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