take {0} ; :: thesis: ( not {0} is empty & {0} is natural-membered )
thus not {0} is empty ; :: thesis: {0} is natural-membered
let x be object ; :: according to MEMBERED:def 6 :: thesis: ( x in {0} implies x is natural )
assume x in {0} ; :: thesis: x is natural
hence x is natural by TARSKI:def 1; :: thesis: verum