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 and
A5: p1 `1 <= q1 `1 and
A6: q1 `1 <= q `1 ; :: thesis: LSeg (p1,q1) c= LSeg (p,q)
A7: p `2 = q `2 by A1, SPPOL_1:15;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (p1,q1) or x in LSeg (p,q) )
assume A8: x in LSeg (p1,q1) ; :: thesis: x in LSeg (p,q)
then reconsider r = x as Point of (TOP-REAL 2) ;
p1 `1 <= r `1 by A5, A8, TOPREAL1:3;
then A9: p `1 <= r `1 by A4, XXREAL_0:2;
r `1 <= q1 `1 by A5, A8, TOPREAL1:3;
then A10: r `1 <= q `1 by A6, XXREAL_0:2;
p1 `2 = r `2 by A2, A8, SPPOL_1:40;
hence x in LSeg (p,q) by A3, A7, A9, A10, Th8; :: thesis: verum