let i be set ; :: according to FRAENKEL:def 1 :: thesis: ( not i in {f} or i is set )
assume i in {f} ; :: thesis: i is set
hence i is Function by TARSKI:def 1; :: thesis: verum