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