let A be Ordinal; :: thesis: ( not A c= 1 or A = {} or A = 1 )
assume A1: ( A c= 1 & A <> {} & A <> 1 ) ; :: thesis: contradiction
then A c< 1 by XBOOLE_0:def 8;
hence contradiction by A1, Th17, ORDINAL1:21; :: thesis: verum