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