let X be ext-natural-membered set ; :: thesis: ( ( for N being ExtNat holds N in X ) implies X = ExtNAT )
assume A1: for N being ExtNat holds N in X ; :: thesis: X = ExtNAT
A2: X c= ExtNAT by ThSubset;
for x being object st x in ExtNAT holds
x in X by A1;
then ExtNAT c= X by TARSKI:def 3;
hence X = ExtNAT by A2, XBOOLE_0:def 10; :: thesis: verum