let A, B, C be Ordinal; :: thesis: ( C <> {} & A c= B implies exp (C,A) c= exp (C,B) )
A1: ( A c< B iff ( A c= B & A <> B ) ) ;
assume C <> {} ; :: thesis: ( not A c= B or exp (C,A) c= exp (C,B) )
then {} in C by ORDINAL3:8;
then A2: 1 c= C by Lm3, ORDINAL1:21;
assume A c= B ; :: thesis: exp (C,A) c= exp (C,B)
then A3: ( A in B or A = B ) by A1, ORDINAL1:11;
now :: thesis: exp (C,A) c= exp (C,B)
per cases ( C = 1 or C <> 1 ) ;
suppose A4: C = 1 ; :: thesis: exp (C,A) c= exp (C,B)
then exp (C,A) = 1 by ORDINAL2:46;
hence exp (C,A) c= exp (C,B) by A4, ORDINAL2:46; :: thesis: verum
end;
suppose C <> 1 ; :: thesis: exp (C,A) c= exp (C,B)
then 1 c< C by A2;
then 1 in C by ORDINAL1:11;
then ( exp (C,A) in exp (C,B) or exp (C,A) = exp (C,B) ) by A3, Th24;
hence exp (C,A) c= exp (C,B) by ORDINAL1:def 2; :: thesis: verum
end;
end;
end;
hence exp (C,A) c= exp (C,B) ; :: thesis: verum