A: TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by Def8;
( x is Real & y is Real ) by XREAL_0:def 1;
hence |[x,y]| is Point of (TOP-REAL 2) by FINSEQ_2:121, A; :: thesis: verum