let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Fuzzy_Negation : verum } or x in Funcs ([.0,1.],[.0,1.]) )
assume x in { f where f is Fuzzy_Negation : verum } ; :: thesis: x in Funcs ([.0,1.],[.0,1.])
then consider f being Fuzzy_Negation such that
A1: x = f ;
thus x in Funcs ([.0,1.],[.0,1.]) by A1, FUNCT_2:8; :: thesis: verum