let p, q be Point of (TOP-REAL 2); for r being Real st p `1 = q `1 & r in [.(proj2 . p),(proj2 . q).] holds
|[(p `1),r]| in LSeg (p,q)
let r be Real; ( p `1 = q `1 & r in [.(proj2 . p),(proj2 . q).] implies |[(p `1),r]| in LSeg (p,q) )
assume A1:
p `1 = q `1
; ( not r in [.(proj2 . p),(proj2 . q).] or |[(p `1),r]| in LSeg (p,q) )
assume A2:
r in [.(proj2 . p),(proj2 . q).]
; |[(p `1),r]| in LSeg (p,q)
A3:
|[(p `1),r]| `2 = r
by EUCLID:52;
proj2 . q = q `2
by PSCOMP_1:def 6;
then A4:
|[(p `1),r]| `2 <= q `2
by A2, A3, XXREAL_1:1;
proj2 . p = p `2
by PSCOMP_1:def 6;
then
( p `1 = |[(p `1),r]| `1 & p `2 <= |[(p `1),r]| `2 )
by A2, A3, EUCLID:52, XXREAL_1:1;
hence
|[(p `1),r]| in LSeg (p,q)
by A1, A4, GOBOARD7:7; verum