let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A holds X c= sup X
let X be Subset of A; :: thesis: X c= sup X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in sup X )
assume x in X ; :: thesis: x in sup X
hence x in sup X by ORDINAL2:19; :: thesis: verum