let x be object ; :: according to VALUED_2:def 4,TOPREALC:def 2 :: thesis: ( not x in the carrier of (TOP-REAL n) or x is set )
assume x in the carrier of (TOP-REAL n) ; :: thesis: x is set
then reconsider x = x as Point of (TOP-REAL n) ;
x is real-valued ;
hence x is set ; :: thesis: verum