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