let X be set ; :: thesis: ( X is ext-natural-membered iff X c= ExtNAT )

hereby :: thesis: ( X c= ExtNAT implies X is ext-natural-membered )

assume A1: X is ext-natural-membered ; :: thesis: X c= ExtNAT

now :: thesis: for x being object st x in X holds
x in ExtNAT

let x be object ; :: thesis: ( x in X implies x in ExtNAT )
assume x in X ; :: thesis: x in ExtNAT
then x is ext-natural by A1;
hence x in ExtNAT ; :: thesis: verum

end;

hence X c= ExtNAT by TARSKI:def 3; :: thesis: verum

end;

assume X c= ExtNAT ; :: thesis: X is ext-natural-membered
hence X is ext-natural-membered ; :: thesis: verum