let X be set ; ex A being Ordinal st
( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )
defpred S1[ 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 & S1[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
; ( 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; for B being Ordinal st not B in X holds
A c= B
let C be Ordinal; ( not C in X implies A c= C )
assume A7:
not C in X
; A c= C
assume A8:
not A c= C
; 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; verum