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

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

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

assume that

A1: a <= b and

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

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

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

|[b,d]| `1 = b by EUCLID:52;

hence ( a <= p `1 & p `1 <= b ) by A1, A2, A3, TOPREAL1:3; :: thesis: verum

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

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

assume that

A1: a <= b and

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

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

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

|[b,d]| `1 = b by EUCLID:52;

hence ( a <= p `1 & p `1 <= b ) by A1, A2, A3, TOPREAL1:3; :: thesis: verum