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 p `1 = q `1 ; :: thesis: ( not r in [.(proj2 . p),(proj2 . q).] or |[(p `1 ),r]| in LSeg p,q )
then A1: ( p `1 = |[(p `1 ),r]| `1 & |[(p `1 ),r]| `1 = q `1 ) by EUCLID:56;
assume A2: r in [.(proj2 . p),(proj2 . q).] ; :: thesis: |[(p `1 ),r]| in LSeg p,q
A3: ( proj2 . p = p `2 & proj2 . q = q `2 ) by PSCOMP_1:def 29;
|[(p `1 ),r]| `2 = r by EUCLID:56;
then ( p `2 <= |[(p `1 ),r]| `2 & |[(p `1 ),r]| `2 <= q `2 ) by A2, A3, XXREAL_1:1;
hence |[(p `1 ),r]| in LSeg p,q by A1, GOBOARD7:8; :: thesis: verum