let X be ordinal-membered set ; :: thesis: X c= sup X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in sup X )
thus ( not x in X or x in sup X ) by ORDINAL2:19; :: thesis: verum