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