theorem Th6: :: MEMBERED:6
for X being set st X is natural-membered holds
X c= NAT by ORDINAL1:def 12;