let p, p1, q be Point of (TOP-REAL 2); :: thesis: for r being Real

for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 holds

((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

let r be Real; :: thesis: for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 holds

((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

let u be Point of (Euclid 2); :: thesis: ( not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 implies ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} )

set v = |[(q `1),(p `2)]|;

assume that

A1: not p1 in Ball (u,r) and

A2: p in Ball (u,r) and

A3: |[(q `1),(p `2)]| in Ball (u,r) and

A4: not |[(q `1),(p `2)]| in LSeg (p1,p) and

A5: p1 `2 = p `2 and

A6: p `1 <> q `1 and

A7: p `2 <> q `2 ; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

A8: LSeg (p,|[(q `1),(p `2)]|) c= Ball (u,r) by A2, A3, Th21;

A9: p1 = |[(p1 `1),(p `2)]| by A5, EUCLID:53;

p in LSeg (p,|[(q `1),(p `2)]|) by RLTOPSP1:68;

then ( p in LSeg (p1,p) & p in (LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q)) ) by RLTOPSP1:68, XBOOLE_0:def 3;

then p in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) by XBOOLE_0:def 4;

then A10: {p} c= ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) by ZFMISC_1:31;

A11: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = ((LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))) \/ ((LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))) by XBOOLE_1:23;

A12: q = |[(q `1),(q `2)]| by EUCLID:53;

A13: p = |[(p `1),(p `2)]| by EUCLID:53;

A14: |[(q `1),(p `2)]| `2 = p `2 by EUCLID:52;

A15: |[(q `1),(p `2)]| `1 = q `1 by EUCLID:52;

for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 holds

((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

let r be Real; :: thesis: for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 holds

((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

let u be Point of (Euclid 2); :: thesis: ( not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 implies ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} )

set v = |[(q `1),(p `2)]|;

assume that

A1: not p1 in Ball (u,r) and

A2: p in Ball (u,r) and

A3: |[(q `1),(p `2)]| in Ball (u,r) and

A4: not |[(q `1),(p `2)]| in LSeg (p1,p) and

A5: p1 `2 = p `2 and

A6: p `1 <> q `1 and

A7: p `2 <> q `2 ; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

A8: LSeg (p,|[(q `1),(p `2)]|) c= Ball (u,r) by A2, A3, Th21;

A9: p1 = |[(p1 `1),(p `2)]| by A5, EUCLID:53;

p in LSeg (p,|[(q `1),(p `2)]|) by RLTOPSP1:68;

then ( p in LSeg (p1,p) & p in (LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q)) ) by RLTOPSP1:68, XBOOLE_0:def 3;

then p in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) by XBOOLE_0:def 4;

then A10: {p} c= ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) by ZFMISC_1:31;

A11: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = ((LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))) \/ ((LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))) by XBOOLE_1:23;

A12: q = |[(q `1),(q `2)]| by EUCLID:53;

A13: p = |[(p `1),(p `2)]| by EUCLID:53;

A14: |[(q `1),(p `2)]| `2 = p `2 by EUCLID:52;

A15: |[(q `1),(p `2)]| `1 = q `1 by EUCLID:52;

per cases
( p1 `1 = p `1 or p1 `1 <> p `1 )
;

end;

suppose
p1 `1 = p `1
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
by A1, A2, A5, Th6; :: thesis: verum

end;suppose A16:
p1 `1 <> p `1
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

end;

now :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}end;

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
; :: thesis: verumper cases
( p1 `1 > p `1 or p1 `1 < p `1 )
by A16, XXREAL_0:1;

end;

suppose A17:
p1 `1 > p `1
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

end;

now :: thesis: ( ( p `1 > q `1 & ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ) or ( p `1 < q `1 & contradiction ) )end;

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
; :: thesis: verumper cases
( p `1 > q `1 or p `1 < q `1 )
by A6, XXREAL_0:1;

end;

case A18:
p `1 > q `1
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

then A19:
p `1 >= |[(q `1),(p `2)]| `1
by EUCLID:52;

end;now :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}end;

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
; :: thesis: verumper cases
( p `2 > q `2 or p `2 < q `2 )
by A7, XXREAL_0:1;

end;

suppose A20:
p `2 > q `2
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) c= {p}

end;proof

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
by A10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} )

assume A21: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis: x in {p}

end;assume A21: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis: x in {p}

now :: thesis: ( ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) & x in {p} ) or ( x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) & contradiction ) )end;

hence
x in {p}
; :: thesis: verumper cases
( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) )
by A11, A21, XBOOLE_0:def 3;

end;

case A22:
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))
; :: thesis: x in {p}

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & |[(q `1),(p `2)]| `1 <= q1 `1 & q1 `1 <= p1 `1 ) }
by A17, A19;

then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A17, A18, Th10, XXREAL_0:2;

hence x in {p} by A22, TOPREAL1:8; :: thesis: verum

end;then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A17, A18, Th10, XXREAL_0:2;

hence x in {p} by A22, TOPREAL1:8; :: thesis: verum

case A23:
x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))
; :: thesis: contradiction

then
x in LSeg (q,|[(q `1),(p `2)]|)
by XBOOLE_0:def 4;

then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) } by A12, A20, Th9;

then A24: ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) ;

x in LSeg (p,p1) by A23, XBOOLE_0:def 4;

then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) } by A9, A13, A17, Th10;

then ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) ;

hence contradiction by A18, A24; :: thesis: verum

end;then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) } by A12, A20, Th9;

then A24: ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) ;

x in LSeg (p,p1) by A23, XBOOLE_0:def 4;

then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) } by A9, A13, A17, Th10;

then ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) ;

hence contradiction by A18, A24; :: thesis: verum

suppose A25:
p `2 < q `2
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) c= {p}

end;proof

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
by A10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} )

assume A26: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis: x in {p}

end;assume A26: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis: x in {p}

now :: thesis: ( ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) & x in {p} ) or ( x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) & contradiction ) )end;

hence
x in {p}
; :: thesis: verumper cases
( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) )
by A11, A26, XBOOLE_0:def 3;

end;

case A27:
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))
; :: thesis: x in {p}

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & |[(q `1),(p `2)]| `1 <= q1 `1 & q1 `1 <= p1 `1 ) }
by A17, A19;

then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A17, A18, Th10, XXREAL_0:2;

hence x in {p} by A27, TOPREAL1:8; :: thesis: verum

end;then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A17, A18, Th10, XXREAL_0:2;

hence x in {p} by A27, TOPREAL1:8; :: thesis: verum

case A28:
x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))
; :: thesis: contradiction

then
x in LSeg (p1,p)
by XBOOLE_0:def 4;

then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) } by A9, A13, A17, Th10;

then A29: ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) ;

x in LSeg (|[(q `1),(p `2)]|,q) by A28, XBOOLE_0:def 4;

then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A25, Th9;

then ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) ;

hence contradiction by A18, A29; :: thesis: verum

end;then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) } by A9, A13, A17, Th10;

then A29: ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) ;

x in LSeg (|[(q `1),(p `2)]|,q) by A28, XBOOLE_0:def 4;

then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A25, Th9;

then ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) ;

hence contradiction by A18, A29; :: thesis: verum

case A30:
p `1 < q `1
; :: thesis: contradiction

end;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( q `1 > p1 `1 or q `1 = p1 `1 or q `1 < p1 `1 )
by XXREAL_0:1;

end;

suppose A31:
q `1 > p1 `1
; :: thesis: contradiction

then
p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= |[(q `1),(p `2)]| `1 ) }
by A5, A15, A17;

then p1 in LSeg (p,|[(q `1),(p `2)]|) by A13, A15, A17, A31, Th10, XXREAL_0:2;

hence contradiction by A1, A8; :: thesis: verum

end;then p1 in LSeg (p,|[(q `1),(p `2)]|) by A13, A15, A17, A31, Th10, XXREAL_0:2;

hence contradiction by A1, A8; :: thesis: verum

suppose A32:
p1 `1 < p `1
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

end;

now :: thesis: ( ( p `1 > q `1 & contradiction ) or ( p `1 < q `1 & ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ) )end;

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
; :: thesis: verumper cases
( p `1 > q `1 or p `1 < q `1 )
by A6, XXREAL_0:1;

end;

case A33:
p `1 > q `1
; :: thesis: contradiction

end;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( q `1 > p1 `1 or q `1 = p1 `1 or q `1 < p1 `1 )
by XXREAL_0:1;

end;

suppose
q `1 > p1 `1
; :: thesis: contradiction

then
|[(q `1),(p `2)]| in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) }
by A15, A14, A33;

hence contradiction by A4, A9, A13, A32, Th10; :: thesis: verum

end;hence contradiction by A4, A9, A13, A32, Th10; :: thesis: verum

suppose A34:
q `1 < p1 `1
; :: thesis: contradiction

then
p1 in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & |[(q `1),(p `2)]| `1 <= p2 `1 & p2 `1 <= p `1 ) }
by A5, A15, A32;

then p1 in LSeg (p,|[(q `1),(p `2)]|) by A13, A15, A32, A34, Th10, XXREAL_0:2;

hence contradiction by A1, A8; :: thesis: verum

end;then p1 in LSeg (p,|[(q `1),(p `2)]|) by A13, A15, A32, A34, Th10, XXREAL_0:2;

hence contradiction by A1, A8; :: thesis: verum

case A35:
p `1 < q `1
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

then A36:
p `1 <= |[(q `1),(p `2)]| `1
by EUCLID:52;

end;now :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}end;

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
; :: thesis: verumper cases
( p `2 > q `2 or p `2 < q `2 )
by A7, XXREAL_0:1;

end;

suppose A37:
p `2 > q `2
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) c= {p}

end;proof

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
by A10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} )

assume A38: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis: x in {p}

end;assume A38: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis: x in {p}

now :: thesis: ( ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) & x in {p} ) or ( x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) & contradiction ) )end;

hence
x in {p}
; :: thesis: verumper cases
( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) )
by A11, A38, XBOOLE_0:def 3;

end;

case A39:
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))
; :: thesis: x in {p}

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & p1 `1 <= q1 `1 & q1 `1 <= |[(q `1),(p `2)]| `1 ) }
by A32, A36;

then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A32, A35, Th10, XXREAL_0:2;

hence x in {p} by A39, TOPREAL1:8; :: thesis: verum

end;then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A32, A35, Th10, XXREAL_0:2;

hence x in {p} by A39, TOPREAL1:8; :: thesis: verum

case A40:
x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))
; :: thesis: contradiction

then
x in LSeg (|[(q `1),(p `2)]|,q)
by XBOOLE_0:def 4;

then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) } by A12, A37, Th9;

then A41: ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) ;

x in LSeg (p1,p) by A40, XBOOLE_0:def 4;

then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A9, A13, A32, Th10;

then ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) ;

hence contradiction by A35, A41; :: thesis: verum

end;then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) } by A12, A37, Th9;

then A41: ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) ;

x in LSeg (p1,p) by A40, XBOOLE_0:def 4;

then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A9, A13, A32, Th10;

then ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) ;

hence contradiction by A35, A41; :: thesis: verum

suppose A42:
p `2 < q `2
; :: thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}

((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) c= {p}

end;proof

hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
by A10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} )

assume A43: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis: x in {p}

end;assume A43: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; :: thesis: x in {p}

now :: thesis: ( ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) & x in {p} ) or ( x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) & contradiction ) )end;

hence
x in {p}
; :: thesis: verumper cases
( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) )
by A11, A43, XBOOLE_0:def 3;

end;

case A44:
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))
; :: thesis: x in {p}

p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & p1 `1 <= q1 `1 & q1 `1 <= |[(q `1),(p `2)]| `1 ) }
by A32, A36;

then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A32, A35, Th10, XXREAL_0:2;

hence x in {p} by A44, TOPREAL1:8; :: thesis: verum

end;then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A32, A35, Th10, XXREAL_0:2;

hence x in {p} by A44, TOPREAL1:8; :: thesis: verum

case A45:
x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))
; :: thesis: contradiction

then
x in LSeg (p1,p)
by XBOOLE_0:def 4;

then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A9, A13, A32, Th10;

then A46: ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) ;

x in LSeg (|[(q `1),(p `2)]|,q) by A45, XBOOLE_0:def 4;

then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A42, Th9;

then ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) ;

hence contradiction by A35, A46; :: thesis: verum

end;then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A9, A13, A32, Th10;

then A46: ex q2 being Point of (TOP-REAL 2) st

( q2 = x & q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) ;

x in LSeg (|[(q `1),(p `2)]|,q) by A45, XBOOLE_0:def 4;

then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A42, Th9;

then ex p2 being Point of (TOP-REAL 2) st

( p2 = x & p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) ;

hence contradiction by A35, A46; :: thesis: verum