let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (chi (A,REAL)) where A is Subset of REAL : A c= REAL } or x in Membership_Funcs REAL )

assume x in { (chi (A,REAL)) where A is Subset of REAL : A c= REAL } ; :: thesis: x in Membership_Funcs REAL

then ex A being Subset of REAL st

( x = chi (A,REAL) & A c= REAL ) ;

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

assume x in { (chi (A,REAL)) where A is Subset of REAL : A c= REAL } ; :: thesis: x in Membership_Funcs REAL

then ex A being Subset of REAL st

( x = chi (A,REAL) & A c= REAL ) ;

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