let D be Ordinal; :: thesis: for X being set st ( for A being Ordinal st A in X holds
A in D ) holds
sup X c= D
let X be set ; :: thesis: ( ( for A being Ordinal st A in X holds
A in D ) implies sup X c= D )
assume A1: for A being Ordinal st A in X holds
A in D ; :: thesis: sup X c= D
On X c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in On X or x in D )
assume A2: x in On X ; :: thesis: x in D
then reconsider A = x as Ordinal by ORDINAL1:def 9;
A in X by A2, ORDINAL1:def 9;
hence x in D by A1; :: thesis: verum

end;

hence sup X c= D by Def3; :: thesis: verum