let A, B, C be Ordinal; ( C <> {} & A c= B implies exp (C,A) c= exp (C,B) )
A1:
( A c< B iff ( A c= B & A <> B ) )
;
assume
C <> {}
; ( 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
; exp (C,A) c= exp (C,B)
then A3:
( A in B or A = B )
by A1, ORDINAL1:11;
hence
exp (C,A) c= exp (C,B)
; verum