let p, q, p1, q1 be Point of (TOP-REAL 2); :: thesis: ( LSeg p,q is horizontal & LSeg p1,q1 is horizontal & p `2 = p1 `2 & p `1 <= p1 `1 & p1 `1 <= q1 `1 & q1 `1 <= q `1 implies LSeg p1,q1 c= LSeg p,q )
assume that
A1: LSeg p,q is horizontal and
A2: LSeg p1,q1 is horizontal and
A3: p `2 = p1 `2 and
A4: ( p `1 <= p1 `1 & p1 `1 <= q1 `1 & q1 `1 <= q `1 ) ; :: thesis: LSeg p1,q1 c= LSeg p,q
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg p1,q1 or x in LSeg p,q )
assume A5: x in LSeg p1,q1 ; :: thesis: x in LSeg p,q
then reconsider r = x as Point of (TOP-REAL 2) ;
A6: p1 `2 = r `2 by A2, A5, SPPOL_1:63;
A7: p `2 = q `2 by A1, SPPOL_1:36;
( p1 `1 <= r `1 & r `1 <= q1 `1 ) by A4, A5, TOPREAL1:9;
then ( p `1 <= r `1 & r `1 <= q `1 ) by A4, XXREAL_0:2;
hence x in LSeg p,q by A3, A6, A7, Th9; :: thesis: verum