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

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