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