let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is FuzzySet of REAL : f is triangular } or x in Membership_Funcs REAL )
assume x in { f where f is FuzzySet of REAL : f is triangular } ; :: thesis: x in Membership_Funcs REAL
then ex f being FuzzySet of REAL st
( x = f & f is triangular ) ;
hence x in Membership_Funcs REAL by Def1; :: thesis: verum