let p, q be Point of (TOP-REAL 2); :: thesis: 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; :: thesis: ( p `1 = q `1 & r in [.(proj2 . p),(proj2 . q).] implies |[(p `1),r]| in LSeg (p,q) )
assume A1: p `1 = q `1 ; :: thesis: ( not r in [.(proj2 . p),(proj2 . q).] or |[(p `1),r]| in LSeg (p,q) )
assume A2: r in [.(proj2 . p),(proj2 . q).] ; :: thesis: |[(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; :: thesis: verum