let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is FuzzySet of REAL : f is trapezoidal } or x in Membership_Funcs REAL )

assume x in { f where f is FuzzySet of REAL : f is trapezoidal } ; :: thesis: x in Membership_Funcs REAL

then ex f being FuzzySet of REAL st

( x = f & f is trapezoidal ) ;

hence x in Membership_Funcs REAL by Def1; :: thesis: verum

assume x in { f where f is FuzzySet of REAL : f is trapezoidal } ; :: thesis: x in Membership_Funcs REAL

then ex f being FuzzySet of REAL st

( x = f & f is trapezoidal ) ;

hence x in Membership_Funcs REAL by Def1; :: thesis: verum