let X be set ; :: thesis: ex A being Ordinal st
( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )
defpred S₁[ object ] means not $1 in X;
consider B being Ordinal such that
A1: not B in X by Th22;
consider Y being set such that
A2: for a being object holds
( a in Y iff ( a in succ B & S₁[a] ) ) from XBOOLE_0:sch 1();
for a being object st a in Y holds
a in succ B by A2;
then A3: Y c= succ B ;
B in succ B by Th2;
then Y <> {} by A1, A2;
then consider A being Ordinal such that
A4: A in Y and
A5: for B being Ordinal st B in Y holds
A c= B by A3, Th16;
A in succ B by A2, A4;
then A6: A c= succ B by Def2;
take A ; :: thesis: ( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )
thus not A in X by A2, A4; :: thesis: for B being Ordinal st not B in X holds
A c= B
let C be Ordinal; :: thesis: ( not C in X implies A c= C )
assume A7: not C in X ; :: thesis: A c= C
assume A8: not A c= C ; :: thesis: contradiction
then not A in C by Def2;
then C in A by A8, Th10;
then C in Y by A2, A7, A6;
hence contradiction by A5, A8; :: thesis: verum