take 1 ; :: thesis: ( not 1 is empty & 1 is natural-membered )
thus not 1 is empty ; :: thesis: 1 is natural-membered
let x be set ; :: according to MEMBERED:def 6 :: thesis: ( x in 1 implies x is natural )
assume x in 1 ; :: thesis: x is natural
hence x is natural by CARD_1:87, TARSKI:def 1; :: thesis: verum