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 ) )
consider B being Ordinal such that
A1: not B in X by Th38;
defpred S₁[ set ] means not $1 in X;
consider Y being set such that
A2: for a being set holds
( a in Y iff ( a in succ B & S₁[a] ) ) from XBOOLE_0:sch 1();
for a being set st a in Y holds
a in succ B by A2;
then A3: Y c= succ B by TARSKI:def 3;
B in succ B by Th10;
then Y <> {} by A1, A2;
then consider A being Ordinal such that
A4: ( A in Y & ( for B being Ordinal st B in Y holds
A c= B ) ) by A3, Th32;
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 A5: not C in X ; :: thesis: A c= C
assume A6: not A c= C ; :: thesis: contradiction
then not A in C by Def2;
then A7: C in A by A6, Th24;
A in succ B by A2, A4;
then A c= succ B by Def2;
then C in Y by A2, A5, A7;
hence contradiction by A4, A6; :: thesis: verum