environ
   1: for p being Person holds Knight[p] implies Wise[p];
   2: for p being Person holds Wise[p] implies Rich[p];
begin

   for p being Person holds Knight[p] implies Rich[p] proof      == UI
      let P be Person;
             == thesis   <=>   Knight[P] implies Rich[P] 
      thus thesis proof                                          == II
                  == thesis   <=>   Knight[P] implies Rich[P] 
              assume a: Knight[P];
                  == thesis   <=>   Rich[P] 
                     b: Wise[P] by 1, a;                         == UE, IE
                     c: Rich[P] by 2, b;                         == UE, IE
              thus thesis by c                                   == RE
                  == thesis   <=>  not contradiction
           end;   == thesis   <=>  not contradiction
   end;
           == The inner proof can be shortened.

   for p being Person holds Knight[p] implies Rich[p] proof      == UI
      let P be Person;
             == thesis   <=>   Knight[P] implies Rich[P] 
      thus thesis proof                                          == II
                  == thesis   <=>   Knight[P] implies Rich[P] 
              assume a: Knight[P];
                  == thesis   <=>   Rich[P] 
                     b: Wise[P] by 1, a;                         == UE, IE
              thus thesis by 2, b;                               == UE, IE
                  == thesis   <=>  not contradiction
           end;   == thesis   <=>  not contradiction
   end;
           == The inner proof can be incorporated entirely.

   for p being Person holds Knight[p] implies Rich[p] proof      == UI
      let P be Person;
             == thesis   <=>   Knight[P] implies Rich[P] 
             == Since the thesis is a conditional we can use
             == hypothetical reasoning to get it.
      assume a: Knight[P];                                       == II
             == thesis   <=>   Rich[P] 
        b: Wise[P] by 1, a;                                      == UE, IE
      thus thesis by 2, b
                  == thesis   <=>  not contradiction
   end;