let p be Point of (Euclid 2); :: thesis: for q being Point of (TOP-REAL 2) st p = 0. (TOP-REAL 2) & p = q holds
( q = <*0,0*> & q `1 = 0 & q `2 = 0 )
let q be Point of (TOP-REAL 2); :: thesis: ( p = 0. (TOP-REAL 2) & p = q implies ( q = <*0,0*> & q `1 = 0 & q `2 = 0 ) )
assume that
A1: p = 0. (TOP-REAL 2) and
A2: p = q ; :: thesis: ( q = <*0,0*> & q `1 = 0 & q `2 = 0 )
0.REAL 2 = 0. (TOP-REAL 2) by EUCLID:66;
then p = <*0,0*> by A1, FINSEQ_2:61;
hence ( q = <*0,0*> & q `1 = 0 & q `2 = 0 ) by A2, EUCLID:52; :: thesis: verum