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