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

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