let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (chi ([.a,b.],REAL)) where a, b is Real : a <= b } or x in Membership_Funcs REAL )

assume x in { (chi ([.a,b.],REAL)) where a, b is Real : a <= b } ; :: thesis: x in Membership_Funcs REAL

then ex a, b being Real st

( x = chi ([.a,b.],REAL) & a <= b ) ;

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

assume x in { (chi ([.a,b.],REAL)) where a, b is Real : a <= b } ; :: thesis: x in Membership_Funcs REAL

then ex a, b being Real st

( x = chi ([.a,b.],REAL) & a <= b ) ;

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