let p, p1, q be Point of (TOP-REAL 2); 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; 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); ( 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
; ((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 )
;
suppose A16:
p1 `1 <> p `1
;
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}now ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}per cases
( p1 `1 > p `1 or p1 `1 < p `1 )
by A16, XXREAL_0:1;
suppose A17:
p1 `1 > p `1
;
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}now ( ( 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 ) )per cases
( p `1 > q `1 or p `1 < q `1 )
by A6, XXREAL_0:1;
case A18:
p `1 > q `1
;
((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;
now ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}per cases
( p `2 > q `2 or p `2 < q `2 )
by A7, XXREAL_0:1;
suppose A20:
p `2 > q `2
;
((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}
proof
let x be
object ;
TARSKI:def 3 ( 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))
;
x in {p}
now ( ( 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 ) )per 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;
case A22:
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))
;
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;
verum end; case A23:
x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))
;
contradictionthen
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;
verum end; end; end;
hence
x in {p}
;
verum
end; hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
by A10;
verum end; suppose A25:
p `2 < q `2
;
((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}
proof
let x be
object ;
TARSKI:def 3 ( 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))
;
x in {p}
now ( ( 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 ) )per 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;
case A27:
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))
;
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;
verum end; case A28:
x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))
;
contradictionthen
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;
verum end; end; end;
hence
x in {p}
;
verum
end; hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
by A10;
verum end; end; end; hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
;
verum end; case A30:
p `1 < q `1
;
contradictionnow contradictionper cases
( q `1 > p1 `1 or q `1 = p1 `1 or q `1 < p1 `1 )
by XXREAL_0:1;
suppose A31:
q `1 > p1 `1
;
contradictionthen
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;
verum end; end; end; hence
contradiction
;
verum end; end; end; hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
;
verum end; suppose A32:
p1 `1 < p `1
;
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}now ( ( 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} ) )per cases
( p `1 > q `1 or p `1 < q `1 )
by A6, XXREAL_0:1;
case A33:
p `1 > q `1
;
contradictionnow contradictionper cases
( q `1 > p1 `1 or q `1 = p1 `1 or q `1 < p1 `1 )
by XXREAL_0:1;
suppose A34:
q `1 < p1 `1
;
contradictionthen
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;
verum end; end; end; hence
contradiction
;
verum end; case A35:
p `1 < q `1
;
((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;
now ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}per cases
( p `2 > q `2 or p `2 < q `2 )
by A7, XXREAL_0:1;
suppose A37:
p `2 > q `2
;
((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}
proof
let x be
object ;
TARSKI:def 3 ( 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))
;
x in {p}
now ( ( 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 ) )per 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;
case A39:
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))
;
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;
verum end; case A40:
x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))
;
contradictionthen
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;
verum end; end; end;
hence
x in {p}
;
verum
end; hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
by A10;
verum end; suppose A42:
p `2 < q `2
;
((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}
proof
let x be
object ;
TARSKI:def 3 ( 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))
;
x in {p}
now ( ( 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 ) )per 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;
case A44:
x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))
;
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;
verum end; case A45:
x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))
;
contradictionthen
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;
verum end; end; end;
hence
x in {p}
;
verum
end; hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
by A10;
verum end; end; end; hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
;
verum end; end; end; hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
;
verum end; end; end; hence
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}
;
verum end; end;