let n be Element of NAT ; :: thesis: n is natural-membered
let x be set ; :: according to MEMBERED:def 6 :: thesis: ( x in n implies x is natural )
n c= omega by ORDINAL1:def 2;
hence ( x in n implies x is natural ) ; :: thesis: verum