let X be set ; :: thesis: ( X is empty implies X is natural-membered )
assume A1: X is empty ; :: thesis: X is natural-membered
let x be set ; :: according to MEMBERED:def 6 :: thesis: ( x in X implies x is natural )
thus ( x in X implies x is natural ) by A1; :: thesis: verum