let p, q be Point of (TOP-REAL 2); :: thesis: for r being real number st p `1 = q `1 & r in [.(proj2 . p),(proj2 . q).] holds
|[(p `1 ),r]| in LSeg p,q
let r be real number ; :: 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:56;
proj2 . q = q `2 by PSCOMP_1:def 29;
then A4: |[(p `1 ),r]| `2 <= q `2 by A2, A3, XXREAL_1:1;
proj2 . p = p `2 by PSCOMP_1:def 29;
then ( p `1 = |[(p `1 ),r]| `1 & p `2 <= |[(p `1 ),r]| `2 ) by A2, A3, EUCLID:56, XXREAL_1:1;
hence |[(p `1 ),r]| in LSeg p,q by A1, A4, GOBOARD7:8; :: thesis: verum