let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) } or x in Membership_Funcs REAL )

assume x in { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) } ; :: thesis: x in Membership_Funcs REAL

then ex a, b, c being Real st

( x = TriangularFS (a,b,c) & a < b & b < c ) ;

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

assume x in { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) } ; :: thesis: x in Membership_Funcs REAL

then ex a, b, c being Real st

( x = TriangularFS (a,b,c) & a < b & b < c ) ;

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