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:4;
( p `2 <= p1 `2 & p1 `2 <= p `2 ) by A1, A2, TOPREAL1:4;
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:68;
hence ( LSeg (p,q) is horizontal implies p `2 = q `2 ) ; :: thesis: verum