let C, A, B be Ordinal; :: thesis: ( C <> {} & A c= B implies exp C,A c= exp C,B )
assume C <> {} ; :: thesis: ( not A c= B or exp C,A c= exp C,B )
then {} in C by ORDINAL3:10;
then A1: 1 c= C by Lm3, ORDINAL1:33;
A2: ( A c< B iff ( A c= B & A <> B ) ) by XBOOLE_0:def 8;
assume A c= B ; :: thesis: exp C,A c= exp C,B
then A3: ( A in B or A = B ) by A2, ORDINAL1:21;

now

per cases ( C = 1 or C <> 1 ) ;

suppose C = 1 ; :: thesis: exp C,A c= exp C,B

then ( exp C,A = 1 & exp C,B = 1 ) by ORDINAL2:63;
hence exp C,A c= exp C,B ; :: thesis: verum

end;

suppose C <> 1 ; :: thesis: exp C,A c= exp C,B

then 1 c< C by A1, XBOOLE_0:def 8;
then 1 in C by ORDINAL1:21;
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