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