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;

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)end;

hence
exp (C,A) c= exp (C,B)
; :: thesis: verum