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