let a, c, d be real number ; :: 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:17; :: thesis: ( c <= p `2 & p `2 <= d )
A3: |[a,c]| `2 = c by EUCLID:56;
|[a,d]| `2 = d by EUCLID:56;
hence ( c <= p `2 & p `2 <= d ) by A1, A2, A3, TOPREAL1:10; :: thesis: verum