let n be Nat; :: thesis: n is natural-membered
for x being set st x in n holds
x is natural by Th1;
hence n is natural-membered by MEMBERED:def 6; :: thesis: verum