let X be set ; :: thesis: for A being Ordinal st X c= A & X <> {} holds
ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
let A be Ordinal; :: thesis: ( X c= A & X <> {} implies ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) ) )
set a = the Element of X;
assume that
A1: X c= A and
A2: X <> {} ; :: thesis: ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
the Element of X in X by A2;
then consider Y being set such that
A3: Y in X and
A4: for a being object holds
( not a in X or not a in Y ) by TARSKI:3;
Y is Ordinal by A1, A3, Th9;
then consider C being Ordinal such that
A5: C = Y ;
take C ; :: thesis: ( C in X & ( for B being Ordinal st B in X holds
C c= B ) )
thus C in X by A3, A5; :: thesis: for B being Ordinal st B in X holds
C c= B
let B be Ordinal; :: thesis: ( B in X implies C c= B )
assume B in X ; :: thesis: C c= B
then not B in C by A4, A5;
then ( B = C or C in B ) by Th10;
hence C c= B by Def2; :: thesis: verum