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