let D be Ordinal; :: thesis: for X being set st On X <> 0 & ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X
let X be set ; :: thesis: ( On X <> 0 & ( for A being Ordinal st A in X holds
D c= A ) implies D c= inf X )
assume that
A1: On X <> 0 and
A2: for A being Ordinal st A in X holds
D c= A ; :: thesis: D c= inf X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in inf X )
assume A3: x in D ; :: thesis: x in inf X
for Y being set st Y in On X holds
x in Y

proof

let Y be set ; :: thesis: ( Y in On X implies x in Y )
assume A4: Y in On X ; :: thesis: x in Y
then reconsider A = Y as Ordinal by ORDINAL1:def 9;
A in X by A4, ORDINAL1:def 9;
then D c= A by A2;
hence x in Y by A3; :: thesis: verum

end;

hence x in inf X by A1, SETFAM_1:def 1; :: thesis: verum