let A be Ordinal; :: thesis: for X being set st A in X holds
inf X in X
let X be set ; :: thesis: ( A in X implies inf X in X )
defpred S₁[ Ordinal] means $1 in X;
assume A in X ; :: thesis: inf X in X
then A1: ex A being Ordinal st S₁[A] ;
consider A being Ordinal such that
A2: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A1);
A3: A in On X by A2, ORDINAL1:def 9;

A4: now

let x be set ; :: thesis: ( ( x in A implies for Y being set st Y in On X holds
x in Y ) & ( ( for Y being set st Y in On X holds
x in Y ) implies x in A ) )
thus ( x in A implies for Y being set st Y in On X holds
x in Y ) :: thesis: ( ( for Y being set st Y in On X holds
x in Y ) implies x in A )

proof

assume A5: x in A ; :: thesis: for Y being set st Y in On X holds
x in Y
let Y be set ; :: thesis: ( Y in On X implies x in Y )
assume A6: Y in On X ; :: thesis: x in Y
then reconsider B = Y as Ordinal by ORDINAL1:def 9;
Y in X by A6, ORDINAL1:def 9;
then A c= B by A2;
hence x in Y by A5; :: thesis: verum

end;

assume for Y being set st Y in On X holds
x in Y ; :: thesis: x in A
hence x in A by A3; :: thesis: verum

end;

On X <> {} by A2, ORDINAL1:def 9;
hence inf X in X by A2, A4, SETFAM_1:def 1; :: thesis: verum