let X be set ; :: thesis: ( X is empty implies X is natural-functions-membered )
assume A1: X is empty ; :: thesis: X is natural-functions-membered
let x be set ; :: according to VALUED_2:def 7 :: thesis: ( x in X implies x is natural-valued Function )
thus ( x in X implies x is natural-valued Function ) by A1; :: thesis: verum