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