let X be set ; :: thesis: ( X is natural implies X is natural-membered )
assume X is natural ; :: thesis: X is natural-membered
then reconsider X = X as Nat ;
let x be object ; :: according to MEMBERED:def 6 :: thesis: ( not x in X or x is natural )
X c= omega ;
hence ( not x in X or x is natural ) ; :: thesis: verum