let p, q be Point of (TOP-REAL 2); :: thesis: ( p `2 = q `2 iff LSeg p,q is horizontal )
set P = LSeg p,q;
thus ( p `2 = q `2 implies LSeg p,q is horizontal ) :: thesis: ( LSeg p,q is horizontal implies p `2 = q `2 )

proof

assume A1: p `2 = q `2 ; :: thesis: LSeg p,q is horizontal
let p1 be Point of (TOP-REAL 2); :: according to SPPOL_1:def 2 :: thesis: for q being Point of (TOP-REAL 2) st p1 in LSeg p,q & q in LSeg p,q holds
p1 `2 = q `2
let p2 be Point of (TOP-REAL 2); :: thesis: ( p1 in LSeg p,q & p2 in LSeg p,q implies p1 `2 = p2 `2 )
assume A2: p1 in LSeg p,q ; :: thesis: ( not p2 in LSeg p,q or p1 `2 = p2 `2 )
assume p2 in LSeg p,q ; :: thesis: p1 `2 = p2 `2
then A3: ( p `2 <= p2 `2 & p2 `2 <= p `2 ) by A1, TOPREAL1:10;
( p `2 <= p1 `2 & p1 `2 <= p `2 ) by A1, A2, TOPREAL1:10;
then p `2 = p1 `2 by XXREAL_0:1;
hence p1 `2 = p2 `2 by A3, XXREAL_0:1; :: thesis: verum

end;

( p in LSeg p,q & q in LSeg p,q ) by RLTOPSP1:69;
hence ( LSeg p,q is horizontal implies p `2 = q `2 ) by Def2; :: thesis: verum