let A, C 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:43;
hence 1 in exp (C,A) by A1, A2, Th24, ORDINAL3:8; :: thesis: verum