let p, q, p1, q1 be Point of (TOP-REAL 2); :: thesis: ( LSeg p,q is vertical & LSeg p1,q1 is vertical & p `1 = p1 `1 & p `2 <= p1 `2 & p1 `2 <= q1 `2 & q1 `2 <= q `2 implies LSeg p1,q1 c= LSeg p,q )
assume that
A1: LSeg p,q is vertical and
A2: LSeg p1,q1 is vertical and
A3: p `1 = p1 `1 and
A4: p `2 <= p1 `2 and
A5: p1 `2 <= q1 `2 and
A6: q1 `2 <= q `2 ; :: thesis: LSeg p1,q1 c= LSeg p,q
A7: p `1 = q `1 by A1, SPPOL_1:37;
let x be set ; :: 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 `2 <= r `2 by A5, A8, TOPREAL1:10;
then A9: p `2 <= r `2 by A4, XXREAL_0:2;
r `2 <= q1 `2 by A5, A8, TOPREAL1:10;
then A10: r `2 <= q `2 by A6, XXREAL_0:2;
p1 `1 = r `1 by A2, A8, SPPOL_1:64;
hence x in LSeg p,q by A3, A7, A9, A10, Th8; :: thesis: verum