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