let a, b, d be real number ; :: 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 A1: ( a <= b & p in LSeg |[a,d]|,|[b,d]| ) ; :: thesis: ( p `2 = d & a <= p `1 & p `1 <= b )
thus p `2 = d by A1, TOPREAL3:18; :: thesis: ( a <= p `1 & p `1 <= b )
A2: |[a,d]| `1 = a by EUCLID:56;
|[b,d]| `1 = b by EUCLID:56;
hence ( a <= p `1 & p `1 <= b ) by A1, A2, TOPREAL1:9; :: thesis: verum