let p, q, p1, q1 be Point of (TOP-REAL 2); ( 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
; LSeg (p1,q1) c= LSeg (p,q)
A7:
p `1 = q `1
by A1, SPPOL_1:16;
let x be object ; TARSKI:def 3 ( not x in LSeg (p1,q1) or x in LSeg (p,q) )
assume A8:
x in LSeg (p1,q1)
; 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; verum