let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (TrapezoidalFS (a,b,c,d)) where a, b, c, d is Real : ( a < b & b < c & c < d ) } or x in Membership_Funcs REAL )
assume x in { (TrapezoidalFS (a,b,c,d)) where a, b, c, d is Real : ( a < b & b < c & c < d ) } ; :: thesis: x in Membership_Funcs REAL
then ex a, b, c, d being Real st
( x = TrapezoidalFS (a,b,c,d) & a < b & b < c & c < d ) ;
hence x in Membership_Funcs REAL by Def1; :: thesis: verum