let X be set ; :: thesis: ( X is natural-membered implies X c= NAT )
assume A1: X is natural-membered ; :: thesis: X c= NAT
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in NAT )
assume x in X ; :: thesis: x in NAT
then x is natural by A1, Def6;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum