let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is FuzzySet of REAL : ex A being Subset of REAL st f = chi (A,REAL) } or x in Membership_Funcs REAL )
assume x in { f where f is FuzzySet of REAL : ex A being Subset of REAL st f = chi (A,REAL) } ; :: thesis: x in Membership_Funcs REAL
then consider f0 being FuzzySet of REAL such that
A1: x = f0 and
ex A being Subset of REAL st f0 = chi (A,REAL) ;
thus x in Membership_Funcs REAL by Def1, A1; :: thesis: verum