let C, A be Ordinal; :: thesis: ( 1 in C & A <> {} implies 1 in exp C,A )
assume A1: ( 1 in C & A <> {} ) ; :: thesis: 1 in exp C,A
then ( {} in A & exp C,{} = 1 ) by ORDINAL2:60, ORDINAL3:10;
hence 1 in exp C,A by A1, Th24; :: thesis: verum