take {ff} ; :: thesis: ( {ff} is natural-functions-membered & not {ff} is empty )
thus for x being set st x in {ff} holds
x is natural-valued Function by TARSKI:def 1; :: according to VALUED_2:def 7 :: thesis: not {ff} is empty
thus not {ff} is empty ; :: thesis: verum