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:16;

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 `2 <= r `2 by A5, A8, TOPREAL1:4;

then A9: p `2 <= r `2 by A4, XXREAL_0:2;

r `2 <= q1 `2 by A5, A8, TOPREAL1:4;

then A10: r `2 <= q `2 by A6, XXREAL_0:2;

p1 `1 = r `1 by A2, A8, SPPOL_1:41;

hence x in LSeg (p,q) by A3, A7, A9, A10, Th7; :: thesis: verum

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:16;

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 `2 <= r `2 by A5, A8, TOPREAL1:4;

then A9: p `2 <= r `2 by A4, XXREAL_0:2;

r `2 <= q1 `2 by A5, A8, TOPREAL1:4;

then A10: r `2 <= q `2 by A6, XXREAL_0:2;

p1 `1 = r `1 by A2, A8, SPPOL_1:41;

hence x in LSeg (p,q) by A3, A7, A9, A10, Th7; :: thesis: verum