let a, c, d be Real; :: thesis: for p being Point of (TOP-REAL 2) st c <= d & p in LSeg (|[a,c]|,|[a,d]|) holds

( p `1 = a & c <= p `2 & p `2 <= d )

let p be Point of (TOP-REAL 2); :: thesis: ( c <= d & p in LSeg (|[a,c]|,|[a,d]|) implies ( p `1 = a & c <= p `2 & p `2 <= d ) )

assume that

A1: c <= d and

A2: p in LSeg (|[a,c]|,|[a,d]|) ; :: thesis: ( p `1 = a & c <= p `2 & p `2 <= d )

thus p `1 = a by A2, TOPREAL3:11; :: thesis: ( c <= p `2 & p `2 <= d )

A3: |[a,c]| `2 = c by EUCLID:52;

|[a,d]| `2 = d by EUCLID:52;

hence ( c <= p `2 & p `2 <= d ) by A1, A2, A3, TOPREAL1:4; :: thesis: verum

( p `1 = a & c <= p `2 & p `2 <= d )

let p be Point of (TOP-REAL 2); :: thesis: ( c <= d & p in LSeg (|[a,c]|,|[a,d]|) implies ( p `1 = a & c <= p `2 & p `2 <= d ) )

assume that

A1: c <= d and

A2: p in LSeg (|[a,c]|,|[a,d]|) ; :: thesis: ( p `1 = a & c <= p `2 & p `2 <= d )

thus p `1 = a by A2, TOPREAL3:11; :: thesis: ( c <= p `2 & p `2 <= d )

A3: |[a,c]| `2 = c by EUCLID:52;

|[a,d]| `2 = d by EUCLID:52;

hence ( c <= p `2 & p `2 <= d ) by A1, A2, A3, TOPREAL1:4; :: thesis: verum