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 A1: ( c <= d & p in LSeg |[a,c]|,|[a,d]| ) ; :: thesis: ( p `1 = a & c <= p `2 & p `2 <= d )
thus p `1 = a by A1, TOPREAL3:17; :: thesis: ( c <= p `2 & p `2 <= d )
A2: |[a,c]| `2 = c by EUCLID:56;
|[a,d]| `2 = d by EUCLID:56;
hence ( c <= p `2 & p `2 <= d ) by A1, A2, TOPREAL1:10; :: thesis: verum