theorem :: ORDINAL4:27

for A, B, C being Ordinal st C <> {} & A c= B holds
exp (C,A) c= exp (C,B)