Copyright (c) 1991 Association of Mizar Users
environ
vocabulary PRE_TOPC, EUCLID, FINSEQ_1, TOPREAL1, MCART_1, BOOLE, COMPTS_1,
BORSUK_1, RELAT_1, TOPS_2, ORDINAL2, SUBSET_1, FUNCT_1, RCOMP_1,
PCOMPS_1, FUNCT_4, TOPREAL2, FINSEQ_4;
notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_4, STRUCT_0, GRCAT_1, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1,
FINSEQ_1, FINSEQ_4, PCOMPS_1, EUCLID, TOPMETR, TOPREAL1;
constructors TOPS_2, COMPTS_1, RCOMP_1, TOPMETR, TOPREAL1, FINSEQ_4, GRCAT_1,
XCMPLX_0, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, PRE_TOPC, RELSET_1, STRUCT_0, EUCLID, BORSUK_1,
TOPREAL1, XREAL_0, XBOOLE_0, MEMBERED, ZFMISC_1;
requirements NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI, PRE_TOPC, TOPS_2;
theorems AXIOMS, BORSUK_1, COMPTS_1, ENUMSET1, EUCLID, FUNCT_1, FUNCT_2,
HEINE, PCOMPS_1, PRE_TOPC, RCOMP_1, REAL_1, TARSKI, TOPMETR, TOPMETR2,
TOPS_2, ZFMISC_1, TOPREAL1, RELAT_1, RELSET_1, GRCAT_1, XBOOLE_0,
XBOOLE_1;
begin
reserve a for set;
reserve p,p1,p2,q,q1,q2 for Point of TOP-REAL 2;
reserve h1,h2 for FinSequence of TOP-REAL 2;
Lm1:
now let x,X be set; assume not x in X;
then {x} misses X by ZFMISC_1:56;
hence {x} /\ X = {} by XBOOLE_0:def 7;
end;
Lm2:
LSeg(|[0,0]|,|[1,0]|) /\ LSeg(|[0,1]|,|[1,1]|) = {}
by TOPREAL1:25,XBOOLE_0:def 7;
Lm3:
LSeg(|[0,0]|,|[0,1]|) /\ LSeg(|[1,0]|,|[1,1]|) = {}
by TOPREAL1:26,XBOOLE_0:def 7;
set p00 = |[ 0,0 ]|, p01 = |[ 0,1 ]|, p10 = |[ 1,0 ]|, p11 = |[ 1,1 ]|,
L1 = LSeg(p00,p01),L2 = LSeg(p01,p11),L3 = LSeg(p00,p10),L4 = LSeg(p10,p11);
Lm4: p00`1 = 0 & p00`2 = 0 & p01`1 = 0 & p01`2 = 1 & p10`1 = 1 & p10`2 = 0 &
p11`1 = 1 & p11`2 = 1 by EUCLID:56;
then Lm5: not p00 in L4 by TOPREAL1:9;
Lm6: not p00 in L2 by Lm4,TOPREAL1:10;
Lm7: not p01 in L3 by Lm4,TOPREAL1:10;
Lm8: not p01 in L4 by Lm4,TOPREAL1:9;
Lm9: not p10 in L1 by Lm4,TOPREAL1:9;
Lm10: not p10 in L2 by Lm4,TOPREAL1:10;
Lm11: not p11 in L1 by Lm4,TOPREAL1:9;
Lm12: not p11 in L3 by Lm4,TOPREAL1:10;
Lm13: p00 in L1 by TOPREAL1:6;
Lm14: p00 in L3 by TOPREAL1:6;
Lm15: p01 in L1 by TOPREAL1:6;
Lm16: p01 in L2 by TOPREAL1:6;
Lm17: p10 in L3 by TOPREAL1:6;
Lm18: p10 in L4 by TOPREAL1:6;
Lm19: p11 in L2 by TOPREAL1:6;
Lm20: p11 in L4 by TOPREAL1:6;
set L = { p : p`1 = 0 & p`2 <= 1 & p`2 >= 0 or
p`1 <= 1 & p`1 >= 0 & p`2 = 1 or
p`1 <= 1 & p`1 >= 0 & p`2 = 0 or
p`1 = 1 & p`2 <= 1 & p`2 >= 0 };
Lm21:p00 in L by Lm4;
Lm22:p11 in L by Lm4;
Lm23:
p1 <> p2 & p2 in R^2-unit_square &
p1 in LSeg(p00, p01) implies
ex P1,P2 being non empty Subset of TOP-REAL 2
st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 &
R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2}
proof assume that
A1: p1 <> p2 and
A2: p2 in R^2-unit_square and
A3: p1 in LSeg(p00, p01);
A4: p2 in L1 \/ L2 or p2 in L3 \/ L4 by A2,TOPREAL1:20,XBOOLE_0:def 2;
consider p such that
A5: p = p1 and A6: p`1 = 0 & p`2 <= 1 & p`2 >= 0 by A3,TOPREAL1:19;
A7: LSeg(p00,p1) c= L1 by A3,Lm13,TOPREAL1:12;
A8: LSeg(p1,p01) c= L1 by A3,Lm15,TOPREAL1:12;
A9: L1 /\ L4 = {} by TOPREAL1:26,XBOOLE_0:def 7;
LSeg(p1,p00) /\ L4 c= L1 /\ L4 by A7,XBOOLE_1:26;
then A10: LSeg(p1,p00) /\ L4 = {} by A9,XBOOLE_1:3;
p00 in LSeg(p1,p00) by TOPREAL1:6;
then p00 in LSeg(p1,p00) /\ L3 by Lm14,XBOOLE_0:def 3;
then A11: {p00} c= LSeg(p1,p00) /\ L3 by ZFMISC_1:37;
A12: LSeg(p1,p00) /\ L3 c= L1 /\ L3 & L1 /\ L3 = {p00}
by A7,TOPREAL1:23,XBOOLE_1:26;
then A13: LSeg(p1,p00) /\ L3 = {p00} by A11,XBOOLE_0:def 10;
LSeg(p01,p1) /\ L4 c= L1 /\ L4 by A8,XBOOLE_1:26;
then A14: LSeg(p01,p1) /\ L4 = {} by A9,XBOOLE_1:3;
p01 in LSeg(p01,p1) by TOPREAL1:6;
then p01 in LSeg(p01,p1) /\ L2 by Lm16,XBOOLE_0:def 3;
then A15: {p01} c= LSeg(p01,p1) /\ L2 by ZFMISC_1:37;
A16: LSeg(p01,p1) /\ L2 c= {p01} by A8,TOPREAL1:21,XBOOLE_1:26;
per cases by A4,XBOOLE_0:def 2;
suppose A17: p2 in L1;
then consider q such that
A18: q = p2 and A19: q`1 = 0 & q`2 <= 1 & q`2 >= 0 by TOPREAL1:19;
A20: LSeg(p2,p1) c= L1 by A3,A17,TOPREAL1:12;
A21: p = |[p`1,p`2]| & q = |[q`1,q`2]| by EUCLID:57;
now per cases by A1,A5,A6,A18,A19,A21,REAL_1:def 5;
case A22: p`2 < q`2;
A23: LSeg(p01,p2) c= L1 by A17,Lm15,TOPREAL1:12;
then A24: LSeg(p01,p2) /\ L3 c= {p00} by TOPREAL1:23,XBOOLE_1:26;
set P1 = LSeg(p1,p2),
P2 = LSeg(p1,p00) \/ (L3 \/ L4 \/ LSeg(p11,p01) \/ LSeg(p01,p2));
now assume p00 in LSeg(p01,p2) /\ L3;
then p00 in
LSeg(p2,p01) & p2`2 <= p01`2 by A18,A19,EUCLID:56,XBOOLE_0:def 3;
hence contradiction by A6,A18,A22,Lm4,TOPREAL1:10;
end;
then {p00} <> LSeg(p01,p2) /\ L3 by ZFMISC_1:37;
then A25: LSeg(p01,p2) /\ L3 = {} by A24,ZFMISC_1:39;
A26: LSeg(p01,p2) /\ L4 c= L1 /\ L4 by A23,XBOOLE_1:26;
A27: now assume
A28: LSeg(p1,p00) /\ LSeg(p01,p2) <> {};
consider a being Element of LSeg(p1,p00) /\ LSeg(p01,p2);
reconsider p = a as Point of TOP-REAL 2 by A28,TARSKI:def 3;
p in LSeg(p00,p1) & p in LSeg(p2,p01) & p00`2 <= p1`2 &
p2`2 <= p01`2 by A5,A6,A18,A19,A28,EUCLID:56,XBOOLE_0:def 3;
then p`2 <= p1`2 & p2`2 <= p`2 by TOPREAL1:10;
hence contradiction by A5,A18,A22,AXIOMS:22;
end;
p01 in LSeg(p01,p2) by TOPREAL1:6;
then p01 in LSeg(p01,p2) /\ L2 by Lm16,XBOOLE_0:def 3;
then A29: {p01} c= LSeg(p01,p2) /\ L2 by ZFMISC_1:37;
A30: LSeg(p01,p2) /\ L2 c= L1 /\ L2 & L1 /\ L2 = {p01}
by A23,TOPREAL1:21,XBOOLE_1:26;
A31: LSeg(p1,p00) /\ L2 c= {p01} by A7,TOPREAL1:21,XBOOLE_1:26;
now assume p01 in LSeg(p1,p00) /\ L2;
then p01 in LSeg(p00,p1) & p00`2 <=
p1`2 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p01`2 <= p1`2 by TOPREAL1:10;
hence contradiction by A5,A6,A19,A22,Lm4,AXIOMS:21;
end;
then A32: {p01} <> LSeg(p1,p00) /\ L2 by ZFMISC_1:37;
A33: LSeg(p01,p2) \/ LSeg(p2,p1) \/
LSeg(p1,p00) = L1 by A3,A17,TOPREAL1:13;
A34: LSeg(p1,p2) c= L1 by A3,A17,TOPREAL1:12;
then A35: LSeg(p1,p2) /\ L4 c= L1 /\ L4 by XBOOLE_1:26;
p1 in LSeg(p1,p2) & p1 in LSeg(p1,p00) by TOPREAL1:6;
then p1 in LSeg(p1,p2) /\ LSeg(p1,p00) by XBOOLE_0:def 3;
then A36: {p1} c= LSeg(p1,p2) /\ LSeg(p1,p00) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p1,p00) c= {p1}
proof
let a; assume A37: a in LSeg(p1,p2) /\ LSeg(p1,p00);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p1,p2) & p in LSeg(p00,p1) & p1`2 <= p2`2 & p1`1 <= p2`1
& p00`2 <= p1`2 by A5,A6,A18,A19,A22,A37,EUCLID:56,XBOOLE_0:def 3;
then p1`1 <= p`1 & p`1 <= p2`1 & p1`2 <= p`2 & p`2 <= p1`2
by TOPREAL1:9,10;
then p1`2 = p`2 & p`1 = 0 by A5,A6,A18,A19,AXIOMS:21;
then p = |[ 0, p1`2]| by EUCLID:57 .= p1 by A5,A6,EUCLID:57;
hence a in {p1} by TARSKI:def 1;
end;
then A38: LSeg(p1,p2) /\ LSeg(p1,p00) = {p1} by A36,XBOOLE_0:def 10;
p2 in LSeg(p1,p2) & p2 in LSeg(p01,p2) by TOPREAL1:6;
then p2 in LSeg(p1,p2) /\ LSeg(p01,p2) by XBOOLE_0:def 3;
then A39: {p2} c= LSeg(p1,p2) /\ LSeg(p01,p2) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p01,p2) c= {p2}
proof
let a; assume A40: a in LSeg(p1,p2) /\ LSeg(p01,p2);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p1,p2) & p in LSeg(p2,p01) & p1`2 <= p2`2 & p1`1 <= p2`1
& p2`2 <= p01`2 by A5,A6,A18,A19,A22,A40,EUCLID:56,XBOOLE_0:def 3;
then p1`1 <= p`1 & p`1 <= p2`1 & p2`2 <= p`2 & p`2 <= p2`2
by TOPREAL1:9,10;
then p2`2 = p`2 & p`1 = 0 by A5,A6,A18,A19,AXIOMS:21;
then p = |[0,p2`2]| by EUCLID:57 .= p2 by A18,A19,EUCLID:57;
hence a in {p2} by TARSKI:def 1;
end;
then A41: LSeg(p1,p2) /\ LSeg(p01,p2) = {p2} by A39,XBOOLE_0:def 10;
thus P1 is_an_arc_of p1,p2 by A1,TOPREAL1:15;
A42: L3 \/ L4 is_an_arc_of p00,p11 by Lm4,TOPREAL1:18,22;
(L3 \/ L4) /\ LSeg(p11,p01)
= {} \/ {p11} by Lm2,TOPREAL1:24,XBOOLE_1:23 .= {p11};
then A43: L3 \/ L4 \/ LSeg(p11,p01) is_an_arc_of p00,p01 by A42,TOPREAL1:
16;
(L3 \/ L4 \/ LSeg(p11,p01)) /\ LSeg(p01,p2)
= LSeg(p01,p2) /\ (L3 \/ L4) \/ (LSeg(p01,p2) /\
LSeg(p11,p01)) by XBOOLE_1:23
.= {}
\/ (LSeg(p01,p2) /\ L4) \/ (LSeg(p01,p2) /\ LSeg(p11,p01)) by A25,XBOOLE_1:23
.= {} \/ (LSeg(p01,p2) /\ LSeg(p11,p01)) by A26,Lm3,XBOOLE_1:3
.= {p01} by A29,A30,XBOOLE_0:def 10;
then A44: L3 \/ L4 \/ LSeg(p11,p01) \/ LSeg(p01,p2) is_an_arc_of p00,p2
by A43,TOPREAL1:16;
LSeg(p1,p00) /\ (L3 \/ L4 \/ LSeg(p11,p01) \/ LSeg(p01,p2))
= LSeg(p1,p00) /\ (L3 \/ L4 \/ LSeg(p11,p01))
\/ LSeg(p1,p00) /\ LSeg(p01,p2) by XBOOLE_1:23
.= LSeg(p1,p00) /\ (L3 \/ L4)
\/ LSeg(p1,p00) /\ LSeg(p11,p01)
\/ LSeg(p1,p00) /\ LSeg(p01,p2) by XBOOLE_1:23
.= (LSeg(p1,p00) /\ L3) \/ (LSeg(p1,p00) /\ L4)
\/ (LSeg(p1,p00) /\ LSeg(p11,p01))
\/ (LSeg(p1,p00) /\ LSeg(p01,p2)) by XBOOLE_1:23
.= {p00} by A10,A13,A27,A31,A32,ZFMISC_1:39;
hence LSeg(p1,p00) \/ (L3 \/ L4 \/ LSeg(p11,p01) \/ LSeg(p01,p2))
is_an_arc_of p1,p2 by A44,TOPREAL1:17;
thus R^2-unit_square =
LSeg(p1,p2) \/ LSeg(p01,p2) \/ LSeg(p1,p00) \/ (L3 \/ L4 \/
LSeg(p11,p01)) by A33,TOPREAL1:20,XBOOLE_1:4
.= LSeg(p1,p2) \/ (LSeg(p1,p00) \/ LSeg(p01,p2))
\/ (L3 \/ L4 \/ LSeg(p11,p01)) by XBOOLE_1:4
.= LSeg(p1,p2) \/ ((LSeg(p1,p00) \/ LSeg(p01,p2))
\/ (L3 \/ L4 \/ LSeg(p11,p01))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4;
A45: P1 /\ P2
= (LSeg(p1,p2) /\ LSeg(p1,p00))
\/ LSeg(p1,p2) /\ (L3 \/ L4 \/ LSeg(p11,p01) \/
LSeg(p01,p2)) by XBOOLE_1:23
.= (LSeg(p1,p2) /\ LSeg(p1,p00))
\/ ((LSeg(p1,p2) /\ (L3 \/ L4 \/ LSeg(p11,p01)))
\/ (LSeg(p1,p2) /\ LSeg(p01,p2))) by XBOOLE_1:23
.= (LSeg(p1,p2) /\ LSeg(p1,p00)) \/ ((LSeg(p1,p2) /\ (L3 \/ L4))
\/ (LSeg(p1,p2) /\ LSeg(p11,p01))
\/ (LSeg(p1,p2) /\ LSeg(p01,p2))) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ L3) \/ (LSeg(p1,p2) /\ L4)
\/ (LSeg(p1,p2) /\ LSeg(p11,p01))
\/ (LSeg(p1,p2) /\ LSeg(p01,p2))) by A38,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ L3) \/ {} \/ (LSeg(p1,p2) /\ LSeg(p11,p01))
\/ (LSeg(p1,p2) /\ LSeg(p01,p2))) by A35,Lm3,XBOOLE_1:3
.= {p1} \/ ((LSeg(p1,p2) /\ L3) \/ ((LSeg(p1,p2) /\ L2) \/ {p2})) by A41,
XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p2) /\ L3) \/ ((LSeg(p1,p2) /\ L2) \/
{p2}) by XBOOLE_1:4;
A46: LSeg(p1,p2) /\ L3 c= {p00} by A34,TOPREAL1:23,XBOOLE_1:26;
A47: now per cases;
suppose A48: p1 = p00;
then p00 in LSeg(p1,p2) by TOPREAL1:6;
then LSeg(p1,p2) /\ L3 <> {} by Lm14,XBOOLE_0:def 3;
then LSeg(p1,p2) /\ L3 = {p1} by A46,A48,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ((LSeg(p1,p2) /\ L2) \/ {p2}) by A45;
suppose A49: p1 <> p00;
now assume p00 in LSeg(p1,p2) /\ L3;
then p00 in LSeg(p1,p2) & p1`2 <= p2`2 & p00`2 <= p01`2
by A5,A18,A22,Lm4,XBOOLE_0:def 3;
then p00`2 <= p1`2 & p1`2 <= p00`2 by A3,TOPREAL1:10;
then p00`2 = p1`2 by AXIOMS:21;
hence contradiction by A5,A6,A49,Lm4,EUCLID:57;
end;
then LSeg(p1,p2) /\ L3 <> {p00} by ZFMISC_1:37;
then LSeg(p1,p2) /\ L3 = {} by A46,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ((LSeg(p1,p2) /\ L2) \/ {p2}) by A45;
end;
A50: LSeg(p1,p2) /\ L2 c= {p01} by A34,TOPREAL1:21,XBOOLE_1:26;
now per cases;
suppose A51: p2 <> p01;
now assume p01 in LSeg(p1,p2) /\ L2;
then p01 in LSeg(p1,p2) & p1`2 <= p2`2 & p00`2 <= p01`2
by A5,A18,A22,Lm4,XBOOLE_0:def 3;
then p01`2 <= p2`2 & p2`2 <= p01`2 by A17,TOPREAL1:10;
then A52: p01`2 = p2`2 by AXIOMS:21;
p2 = |[p2`1,p2`2]| by EUCLID:57 .= |[0,1]| by A18,A19,A52,EUCLID:56;
hence contradiction by A51;
end;
then LSeg(p1,p2) /\ L2 <> {p01} by ZFMISC_1:37;
then LSeg(p1,p2) /\ L2 = {} by A50,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A47,ENUMSET1:41;
suppose A53: p2 = p01;
then p01 in LSeg(p1,p2) by TOPREAL1:6;
then LSeg(p1,p2) /\ L2 <> {} by Lm16,XBOOLE_0:def 3;
then LSeg(p1,p2) /\ L2 = {p2} by A50,A53,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A47,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
case A54: p`2 > q`2;
take P1 = LSeg(p2,p1),P2
= LSeg(p2,p00) \/ (L3 \/ L4 \/ LSeg(p11,p01) \/ LSeg(p01,p1));
A55: LSeg(p01,p1) /\ L3 c= {p00} by A8,TOPREAL1:23,XBOOLE_1:26;
now assume p00 in LSeg(p01,p1) /\ L3;
then p00 in LSeg(p1,p01) & p1`2 <=
p01`2 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
hence contradiction by A5,A19,A54,Lm4,TOPREAL1:10;
end;
then A56: {p00} <> LSeg(p01,p1) /\ L3 by ZFMISC_1:37;
A57: LSeg(p2,p00) c= L1 by A17,Lm13,TOPREAL1:12;
then A58: LSeg(p2,p00) /\ L4 c= L1 /\ L4 by XBOOLE_1:26;
A59: now assume
A60: LSeg(p2,p00) /\ LSeg(p01,p1) <> {};
consider a being Element of LSeg(p2,p00) /\ LSeg(p01,p1);
reconsider p = a as Point of TOP-REAL 2 by A60,TARSKI:def 3;
p in LSeg(p00,p2) & p in LSeg(p1,p01) & p00`2 <= p2`2 &
p1`2 <= p01`2 by A5,A6,A18,A19,A60,EUCLID:56,XBOOLE_0:def 3;
then p`2 <= p2`2 & p1`2 <= p`2 by TOPREAL1:10;
hence contradiction by A5,A18,A54,AXIOMS:22;
end;
p00 in LSeg(p2,p00) by TOPREAL1:6;
then p00 in LSeg(p2,p00) /\ L3 by Lm14,XBOOLE_0:def 3;
then A61: {p00} c= LSeg(p2,p00) /\ L3 by ZFMISC_1:37;
A62: LSeg(p2,p00) /\ L3 c= {p00} by A57,TOPREAL1:23,XBOOLE_1:26;
A63: LSeg(p2,p00) /\ L2 c= {p01} by A57,TOPREAL1:21,XBOOLE_1:26;
now assume p01 in LSeg(p2,p00) /\ L2;
then p01 in
LSeg(p00,p2) & p00`2 <= p2`2 by A18,A19,EUCLID:56,XBOOLE_0:def 3;
then p01`2 <= p2`2 by TOPREAL1:10;
hence contradiction by A6,A18,A19,A54,Lm4,AXIOMS:21;
end;
then A64: {p01} <> LSeg(p2,p00) /\ L2 by ZFMISC_1:37;
A65: LSeg(p01,p1) \/ LSeg(p1,p2) \/
LSeg(p2,p00) = L1 by A3,A17,TOPREAL1:13;
A66: LSeg(p2,p1) /\ L4 c= L1 /\ L4 by A20,XBOOLE_1:26;
p2 in LSeg(p2,p1) & p2 in LSeg(p2,p00) by TOPREAL1:6;
then p2 in LSeg(p2,p1) /\ LSeg(p2,p00) by XBOOLE_0:def 3;
then A67: {p2} c= LSeg(p2,p1) /\ LSeg(p2,p00) by ZFMISC_1:37;
A68: LSeg(p2,p1) /\ LSeg(p2,p00) c= {p2}
proof
let a; assume A69: a in LSeg(p2,p1) /\ LSeg(p2,p00);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p2,p1) & p in LSeg(p00,p2) & p2`2 <= p1`2 & p2`1 <= p1`1
& p00`2 <= p2`2 by A5,A6,A18,A19,A54,A69,EUCLID:56,XBOOLE_0:def 3;
then p2`1 <= p`1 & p`1 <= p1`1 & p2`2 <= p`2 & p`2 <= p2`2
by TOPREAL1:9,10;
then p2`2 = p`2 & p`1 = 0 by A5,A6,A18,A19,AXIOMS:21;
then p = |[ 0, p2`2]| by EUCLID:57 .= p2 by A18,A19,EUCLID:57;
hence a in {p2} by TARSKI:def 1;
end;
p1 in LSeg(p2,p1) & p1 in LSeg(p01,p1) by TOPREAL1:6;
then p1 in LSeg(p2,p1) /\ LSeg(p01,p1) by XBOOLE_0:def 3;
then A70: {p1} c= LSeg(p2,p1) /\ LSeg(p01,p1) by ZFMISC_1:37;
A71: LSeg(p2,p1) /\ LSeg(p01,p1) c= {p1}
proof
let a; assume A72: a in LSeg(p2,p1) /\ LSeg(p01,p1);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p2,p1) & p in LSeg(p1,p01) & p2`2 <= p1`2 & p2`1 <= p1`1
& p1`2 <= p01`2 by A5,A6,A18,A19,A54,A72,EUCLID:56,XBOOLE_0:def 3;
then p2`1 <= p`1 & p`1 <= p1`1 & p1`2 <= p`2 & p`2 <= p1`2
by TOPREAL1:9,10;
then p1`2 = p`2 & p`1 = 0 by A5,A6,A18,A19,AXIOMS:21;
then p = |[0,p1`2]| by EUCLID:57 .= p1 by A5,A6,EUCLID:57;
hence a in {p1} by TARSKI:def 1;
end;
thus P1 is_an_arc_of p1,p2 by A1,TOPREAL1:15;
A73: L3 \/ L4 is_an_arc_of p11,p00 by Lm4,TOPREAL1:18,22;
L2 /\ (L3 \/ L4)
= {} \/ {p11} by Lm2,TOPREAL1:24,XBOOLE_1:23 .= {p11};
then A74: L3 \/ L4 \/ LSeg(p11,p01) is_an_arc_of p01,p00 by A73,TOPREAL1:
17;
LSeg(p1,p01) /\ (L3 \/ L4 \/ LSeg(p11,p01))
= LSeg(p01,p1) /\ (L3 \/ L4) \/ (LSeg(p01,p1) /\
LSeg(p11,p01)) by XBOOLE_1:23
.= (LSeg(p01,p1) /\ L3) \/ (LSeg(p01,p1) /\ L4)
\/ (LSeg(p01,p1) /\ LSeg(p11,p01)) by XBOOLE_1:23
.= {} \/ (LSeg(p01,p1) /\ L4) \/ (LSeg(p01,p1) /\ LSeg(p11,p01))
by A55,A56,ZFMISC_1:39
.= {p01} by A14,A15,A16,XBOOLE_0:def 10;
then A75: L3 \/ L4 \/ LSeg(p11,p01) \/
LSeg(p01,p1) is_an_arc_of p1,p00 by A74,TOPREAL1:17;
(L3 \/ L4 \/ LSeg(p11,p01) \/ LSeg(p01,p1)) /\ LSeg(p00,p2)
= LSeg(p2,p00) /\ (L3 \/ L4 \/ LSeg(p11,p01))
\/ LSeg(p2,p00) /\ LSeg(p01,p1) by XBOOLE_1:23
.= LSeg(p2,p00) /\ (L3 \/ L4)
\/ LSeg(p2,p00) /\ LSeg(p11,p01)
\/ LSeg(p2,p00) /\ LSeg(p01,p1) by XBOOLE_1:23
.= (LSeg(p2,p00) /\ L3) \/ (LSeg(p2,p00) /\ L4)
\/ (LSeg(p2,p00) /\ LSeg(p11,p01))
\/ (LSeg(p2,p00) /\ LSeg(p01,p1)) by XBOOLE_1:23
.= (LSeg(p2,p00) /\ L3) \/ {} \/ (LSeg(p2,p00) /\ LSeg(p11,p01))
\/ (LSeg(p2,p00) /\ LSeg(p01,p1)) by A58,Lm3,XBOOLE_1:3
.= LSeg(p2,p00) /\ L3 \/ {} by A59,A63,A64,ZFMISC_1:39
.= {p00} by A61,A62,XBOOLE_0:def 10;
hence P2 is_an_arc_of p1,p2 by A75,TOPREAL1:16;
thus R^2-unit_square =
LSeg(p2,p1) \/ LSeg(p01,p1) \/ LSeg(p2,p00) \/ (L3 \/ L4 \/
LSeg(p11,p01)) by A65,TOPREAL1:20,XBOOLE_1:4
.= LSeg(p2,p1) \/ (LSeg(p2,p00) \/ LSeg(p01,p1))
\/ (L3 \/ L4 \/ LSeg(p11,p01)) by XBOOLE_1:4
.= LSeg(p2,p1) \/ ((LSeg(p2,p00) \/ LSeg(p01,p1))
\/ (L3 \/ L4 \/ LSeg(p11,p01))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4;
A76: P1 /\ P2 = (LSeg(p2,p1) /\ LSeg(p2,p00))
\/ LSeg(p2,p1) /\ (L3 \/ L4 \/ LSeg(p11,p01) \/
LSeg(p01,p1)) by XBOOLE_1:23
.= (LSeg(p2,p1) /\ LSeg(p2,p00))
\/ ((LSeg(p2,p1) /\ (L3 \/ L4 \/ LSeg(p11,p01)))
\/ (LSeg(p2,p1) /\ LSeg(p01,p1))) by XBOOLE_1:23
.= (LSeg(p2,p1) /\ LSeg(p2,p00)) \/ ((LSeg(p2,p1) /\ (L3 \/ L4))
\/ (LSeg(p2,p1) /\ LSeg(p11,p01))
\/ (LSeg(p2,p1) /\ LSeg(p01,p1))) by XBOOLE_1:23
.= (LSeg(p2,p1) /\ LSeg(p2,p00))
\/ ((LSeg(p2,p1) /\ L3) \/ (LSeg(p2,p1) /\ L4)
\/ (LSeg(p2,p1) /\ LSeg(p11,p01))
\/ (LSeg(p2,p1) /\ LSeg(p01,p1))) by XBOOLE_1:23
.= {p2} \/ ((LSeg(p2,p1) /\ L3) \/ (LSeg(p2,p1) /\ L4)
\/ (LSeg(p2,p1) /\ LSeg(p11,p01))
\/ (LSeg(p2,p1) /\ LSeg(p01,p1))) by A67,A68,XBOOLE_0:def 10
.= {p2} \/ ((LSeg(p2,p1) /\ L3) \/ {} \/ (LSeg(p2,p1) /\ LSeg(p11,p01))
\/ (LSeg(p2,p1) /\ LSeg(p01,p1))) by A66,Lm3,XBOOLE_1:3
.= {p2} \/ ((LSeg(p2,p1) /\ L3) \/ LSeg(p2,p1) /\ L2 \/
{p1}) by A70,A71,XBOOLE_0:def 10
.= {p2} \/ ((LSeg(p2,p1) /\ L3) \/ ((LSeg(p2,p1) /\ L2) \/
{p1})) by XBOOLE_1:4
.= {p2} \/ (LSeg(p2,p1) /\ L3) \/ ((LSeg(p2,p1) /\ L2) \/
{p1}) by XBOOLE_1:4;
A77: LSeg(p2,p1) /\ L3 c= {p00} by A20,TOPREAL1:23,XBOOLE_1:26;
A78: now per cases;
suppose A79: p2 = p00;
p2 in LSeg(p2,p1) by TOPREAL1:6;
then LSeg(p2,p1) /\ L3 <> {} by A79,Lm14,XBOOLE_0:def 3;
then LSeg(p2,p1) /\ L3 = {p2} by A77,A79,ZFMISC_1:39;
hence P1 /\ P2 = {p2} \/ ((LSeg(p2,p1) /\ L2) \/ {p1}) by A76;
suppose A80: p2 <> p00;
now assume p00 in LSeg(p2,p1) /\ L3;
then p00 in LSeg(p2,p1) & p2`2 <= p1`2 & p00`2 <= p01`2
by A5,A18,A54,Lm4,XBOOLE_0:def 3;
then p00`2 <= p2`2 & p2`2 <= p00`2 by A17,TOPREAL1:10;
then p00`2 = p2`2 by AXIOMS:21;
hence contradiction by A18,A19,A80,Lm4,EUCLID:57;
end;
then LSeg(p2,p1) /\ L3 <> {p00} by ZFMISC_1:37;
then LSeg(p2,p1) /\ L3 = {} by A77,ZFMISC_1:39;
hence P1 /\ P2 = {p2} \/ ((LSeg(p2,p1) /\ L2) \/ {p1}) by A76;
end;
A81: LSeg(p2,p1) /\ L2 c= {p01} by A20,TOPREAL1:21,XBOOLE_1:26;
now per cases;
suppose A82: p1 <> p01;
now assume p01 in LSeg(p2,p1) /\ L2;
then p01 in LSeg(p2,p1) & p2`2 <= p1`2 & p00`2 <= p01`2
by A5,A18,A54,Lm4,XBOOLE_0:def 3;
then p01`2 <= p1`2 & p1`2 <= p01`2 by A3,TOPREAL1:10;
then A83: p01`2 = p1`2 by AXIOMS:21;
p1 = |[p1`1,p1`2]| by EUCLID:57 .= |[0,1]| by A5,A6,A83,EUCLID:56;
hence contradiction by A82;
end;
then LSeg(p2,p1) /\ L2 <> {p01} by ZFMISC_1:37;
then LSeg(p2,p1) /\ L2 = {} by A81,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A78,ENUMSET1:41;
suppose A84: p1 = p01;
then p01 in LSeg(p2,p1) by TOPREAL1:6;
then LSeg(p2,p1) /\ L2 <> {} by Lm16,XBOOLE_0:def 3;
then LSeg(p2,p1) /\ L2 = {p1} by A81,A84,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A78,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
end;
hence ex P1,P2 being non empty Subset of TOP-REAL 2
st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 &
R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2};
suppose A85: p2 in L2;
then A86: ex q st q = p2 & q`1 <= 1 & q`1 >= 0 & q`2 = 1 by TOPREAL1:19;
A87: p1 <> p01 or p2 <> p01 by A1;
take P1 = LSeg(p1,p01) \/ LSeg(p01,p2),P2
= LSeg(p1,p00) \/ (L3 \/ L4 \/ LSeg(p11,p2));
p01 in LSeg(p1,p01) & p01 in LSeg(p01,p2) by TOPREAL1:6;
then LSeg(p1,p01) c= L1 & LSeg(p01,p2) c= L2 &
p01 in LSeg(p1,p01) /\ LSeg(p01,p2) by A3,A85,Lm15,Lm16,TOPREAL1:12,
XBOOLE_0:def 3;
then LSeg(p1,p01) /\ LSeg(p01,p2) c= L1 /\ L2 & L1 /\ L2 = {p01}
& LSeg(p1,p01) /\ LSeg(p01,p2) <> {} by TOPREAL1:21,XBOOLE_1:27;
then LSeg(p1,p01) /\ LSeg(p01,p2) = {p01} by ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by A87,TOPREAL1:18;
L3 is_an_arc_of p00,p10 & L4 is_an_arc_of p10,p11 by Lm4,TOPREAL1:15;
then A88: L3 \/ L4 is_an_arc_of p00,p11 by TOPREAL1:5,22;
A89: LSeg(p11,p2) c= L2 by A85,Lm19,TOPREAL1:12;
then L3 /\ LSeg(p11,p2) c= L3 /\ L2 by XBOOLE_1:26;
then A90: L3 /\ LSeg(p11,p2) = {} by Lm2,XBOOLE_1:3;
p11 in LSeg(p11,p2) by TOPREAL1:6;
then A91: L4 /\ LSeg(p11,p2) c= L4 /\ L2 &
p11 in L4 /\ LSeg(p11,p2) by A89,Lm20,XBOOLE_0:def 3,XBOOLE_1:27;
(L3 \/ L4) /\ LSeg(p11,p2)
= (L3 /\ LSeg(p11,p2)) \/ (L4 /\ LSeg(p11,p2)) by XBOOLE_1:23
.= {p11} by A90,A91,TOPREAL1:24,ZFMISC_1:39;
then A92: L3 \/ L4 \/ LSeg(p11,p2) is_an_arc_of p00,p2 by A88,TOPREAL1:16;
LSeg(p1,p00) /\ LSeg(p11,p2) c= {p01} by A7,A89,TOPREAL1:21,XBOOLE_1:27;
then A93: LSeg(p1,p00) /\ LSeg(p11,p2) = {p01} or
LSeg(p1,p00) /\ LSeg(p11,p2) = {} by ZFMISC_1:39;
A94: now assume p01 in LSeg(p1,p00) /\ LSeg(p11,p2);
then p01 in LSeg(p00,p1) & p01 in LSeg(p2,p11) & p00`2 <= p1`2 &
p2`1 <= p11`1 by A5,A6,A86,EUCLID:56,XBOOLE_0:def 3;
then p01`2 <= p1`2 & p2`1 <= p01`1 by TOPREAL1:9,10;
then A95: p01`2 = p1`2 & p01`2 = p2`2 & p01`1 = p1`1 & p01`1 = p2`1
by A5,A6,A86,Lm4,AXIOMS:21;
then p1 = |[p01`1,p01`2]| by EUCLID:57 .= p2 by A95,EUCLID:57;
hence contradiction by A1;
end;
LSeg(p1,p00) /\ (L3 \/ L4 \/ LSeg(p11,p2))
= (LSeg(p1,p00) /\ (L3 \/ L4)) \/ (LSeg(p1,p00) /\
LSeg(p11,p2)) by XBOOLE_1:23
.= (LSeg(p1,p00) /\ L3) \/ (LSeg(p1,p00) /\ L4) by A93,A94,XBOOLE_1:23,
ZFMISC_1:37
.= {p00} by A10,A11,A12,XBOOLE_0:def 10;
hence P2 is_an_arc_of p1,p2 by A92,TOPREAL1:17;
A96: L1 = LSeg(p1,p01) \/ LSeg(p1,p00) by A3,TOPREAL1:11;
A97: L2 = LSeg(p11,p2) \/ LSeg(p01,p2) by A85,TOPREAL1:11;
thus P1 \/ P2
= LSeg(p01,p2) \/ (LSeg(p1,p01) \/ (LSeg(p1,p00) \/
(L3 \/ L4 \/ LSeg(p11,p2)))) by XBOOLE_1:4
.= L1 \/ (L3 \/ L4 \/ LSeg(p11,p2)) \/ LSeg(p01,p2) by A96,XBOOLE_1:4
.= L1 \/ ((L3 \/ L4 \/ LSeg(p11,p2)) \/ LSeg(p01,p2)) by XBOOLE_1:4
.= L1 \/ (L2 \/ (L3 \/ L4)) by A97,XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:20,XBOOLE_1:4;
A98: LSeg(p01,p2) c= L2 by A85,Lm16,TOPREAL1:12;
A99: {p1} = LSeg(p1,p01) /\ LSeg(p1,p00) by A3,TOPREAL1:14;
A100: LSeg(p01,p2) /\ LSeg(p11,p2) = {p2} by A85,TOPREAL1:14;
LSeg(p01,p2) /\ L3 c= L2 /\ L3 by A98,XBOOLE_1:27;
then A101: LSeg(p01,p2) /\ L3 = {} by Lm2,XBOOLE_1:3;
A102: P1 /\ P2 = (LSeg(p1,p01) /\ (LSeg(p1,p00) \/ (L3 \/ L4 \/
LSeg(p11,p2))))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p00) \/ (L3 \/ L4 \/ LSeg(p11,p2))))
by XBOOLE_1:23
.= (LSeg(p1,p01) /\ LSeg(p1,p00))
\/ (LSeg(p1,p01) /\ (L3 \/ L4 \/ LSeg(p11,p2)))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p00) \/ (L3 \/ L4 \/ LSeg(p11,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ (L3 \/ L4)) \/ (LSeg(p1,p01) /\
LSeg(p11,p2)))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p00) \/ (L3 \/ L4 \/ LSeg(p11,p2))))
by A99,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ L3) \/ (LSeg(p1,p01) /\ L4)
\/ (LSeg(p1,p01) /\ LSeg(p11,p2)))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p00) \/ (L3 \/ L4 \/ LSeg(p11,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ L3) \/ (LSeg(p1,p01) /\ L4)
\/ (LSeg(p1,p01) /\ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ LSeg(p1,p00))
\/ (LSeg(p01,p2) /\ (L3 \/ L4 \/ LSeg(p11,p2)))) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ L3) \/ (LSeg(p1,p01) /\ L4)
\/ (LSeg(p1,p01) /\ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ LSeg(p1,p00))
\/ ((LSeg(p01,p2) /\ (L3 \/ L4)) \/ {p2})) by A100,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ L3) \/ (LSeg(p1,p01) /\ L4)
\/ (LSeg(p1,p01) /\ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ LSeg(p1,p00))
\/ ((LSeg(p01,p2) /\ L3) \/ (LSeg(p01,p2) /\ L4) \/ {p2})) by XBOOLE_1:
23
.= {p1} \/ ((LSeg(p1,p01) /\ L3) \/ (LSeg(p1,p01) /\ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ LSeg(p1,p00)) \/ (LSeg(p01,p2) /\ L4 \/ {p2}))
by A14,A101;
A103: now per cases;
suppose A104: p2 = p11;
then A105: not p2 in LSeg(p1,p01) by A8,Lm4,TOPREAL1:9;
LSeg(p1,p01) /\ LSeg(p11,p2) = LSeg(p1,p01) /\ {p2} by A104,TOPREAL1:7
.= {} by A105,Lm1;
hence P1 /\ P2
= {p1} \/ (LSeg(p1,p01) /\ L3) \/ ((LSeg(p01,p2) /\ LSeg(p1,p00))
\/ {p2}) by A102,A104,TOPREAL1:24;
suppose A106: p2 <> p11 & p2 <> p01;
A107: LSeg(p01,p2) /\ L4 c= {p11} by A98,TOPREAL1:24,XBOOLE_1:27;
now assume p11 in LSeg(p01,p2) /\ L4;
then p11 in
LSeg(p01,p2) & p01`1 <= p2`1 by A86,EUCLID:56,XBOOLE_0:def 3;
then p11`1 <= p2`1 by TOPREAL1:9;
then p2`1 = p11`1 & p2`2 = p11`2 by A86,Lm4,AXIOMS:21;
hence contradiction by A106,Lm4,EUCLID:57;
end;
then {p11} <> LSeg(p01,p2) /\ L4 by ZFMISC_1:37;
then A108: LSeg(p01,p2) /\ L4 = {} by A107,ZFMISC_1:39;
A109: LSeg(p1,p01) /\
LSeg(p11,p2) c= {p01} by A8,A89,TOPREAL1:21,XBOOLE_1:27;
now assume p01 in LSeg(p1,p01) /\ LSeg(p11,p2);
then p01 in LSeg(p2,p11) & p2`1 <= p11`1 by A86,EUCLID:56,XBOOLE_0:def
3;
then p2`1 = 0 & p2`2 = 1 by A86,Lm4,TOPREAL1:9;
hence contradiction by A106,EUCLID:57;
end;
then {p01} <> LSeg(p1,p01) /\ LSeg(p11,p2) by ZFMISC_1:37;
then LSeg(p1,p01) /\ LSeg(p11,p2) = {} by A109,ZFMISC_1:39;
hence P1 /\ P2
= {p1} \/ (LSeg(p1,p01) /\ L3) \/ ((LSeg(p01,p2) /\ LSeg(p1,p00)) \/
{p2}) by A102,A108;
suppose A110: p2 = p01;
then A111: LSeg(p01,p2) /\ L4 = {p01} /\ L4 by TOPREAL1:7
.= {} by Lm1,Lm8;
A112: LSeg(p1,p01) /\
LSeg(p11,p2) c= {p2} by A8,A110,TOPREAL1:21,XBOOLE_1:27;
p2 in LSeg(p1,p01) by A110,TOPREAL1:6;
then LSeg(p1,p01) /\ LSeg(p11,p2) <> {}
by A110,Lm16,XBOOLE_0:def 3;
then LSeg(p1,p01) /\ LSeg(p11,p2) = {p2} by A112,ZFMISC_1:39;
hence P1 /\ P2
= ({p1} \/ (LSeg(p1,p01) /\ L3)) \/ {p2} \/ ((LSeg(p01,p2) /\
LSeg(p1,p00))
\/ {p2}) by A102,A111,XBOOLE_1:4
.= ({p1} \/ (LSeg(p1,p01) /\ L3)) \/ ((LSeg(p01,p2) /\ LSeg(p1,p00))
\/ {p2} \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ (LSeg(p1,p01) /\ L3)) \/ ((LSeg(p01,p2) /\ LSeg(p1,p00))
\/ ({p2} \/ {p2})) by XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p01) /\ L3) \/ ((LSeg(p01,p2) /\ LSeg(p1,p00))
\/ {p2});
end;
now per cases;
suppose A113: p1 = p01;
then A114: LSeg(p1,p01) /\ L3 = {p1} /\ L3 by TOPREAL1:7 .= {}
by A113,Lm1,Lm7;
LSeg(p01,p2) /\ LSeg(p1,p00) c= L2 /\ L1 & p1 in LSeg(p01,p2)
by A98,A113,TOPREAL1:6,XBOOLE_1:27;
then LSeg(p01,p2) /\ LSeg(p1,p00) c= {p1} &
LSeg(p01,p2) /\ LSeg(p1,p00) <> {}
by A113,Lm15,TOPREAL1:21,XBOOLE_0:def 3;
then LSeg(p01,p2) /\ LSeg(p1,p00) = {p1} by ZFMISC_1:39;
hence P1 /\ P2
= {p1} \/ {p1} \/ {p2} by A103,A114,XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41;
suppose A115: p1 = p00;
A116: not p00 in LSeg(p01,p2) by A98,Lm4,TOPREAL1:10;
LSeg(p01,p2) /\ LSeg(p1,p00) = LSeg(p01,p2) /\ {p00}
by A115,TOPREAL1:7
.= {} by A116,Lm1;
hence P1 /\ P2
= {p1,p2} by A103,A115,ENUMSET1:41,TOPREAL1:23;
suppose A117: p1 <> p00 & p1 <> p01;
A118: LSeg(p1,p01) /\ L3 c= {p00} by A8,TOPREAL1:23,XBOOLE_1:27;
now assume p00 in LSeg(p1,p01) /\ L3;
then p00 in LSeg(p1,p01) & p1`2 <= p01`2
by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p1`2 = 0 by A5,A6,Lm4,TOPREAL1:10;
hence contradiction by A5,A6,A117,EUCLID:57;
end;
then {p00} <> LSeg(p1,p01) /\ L3 by ZFMISC_1:37;
then A119: LSeg(p1,p01) /\ L3 = {} by A118,ZFMISC_1:39;
A120: LSeg(p01,p2) /\ LSeg(p1,p00) c= {p01} by A7,A98,TOPREAL1:21,
XBOOLE_1:27;
now assume p01 in LSeg(p01,p2) /\ LSeg(p1,p00);
then p01 in LSeg(p00,p1) & p00`2 <= p1`2
by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p01`2 <= p1`2 by TOPREAL1:10;
then p1`2 = 1 by A5,A6,Lm4,AXIOMS:21;
hence contradiction by A5,A6,A117,EUCLID:57;
end;
then {p01} <> LSeg(p01,p2) /\ LSeg(p1,p00) by ZFMISC_1:37;
then LSeg(p01,p2) /\ LSeg(p1,p00) = {} by A120,ZFMISC_1:39;
hence P1 /\ P2
= {p1,p2} by A103,A119,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
suppose A121: p2 in L3;
then A122: ex q st q = p2 & q`1 <= 1 & q`1 >= 0 & q`2 = 0 by TOPREAL1:19;
take P1 = LSeg(p1,p00) \/ LSeg(p00,p2),P2
= LSeg(p1,p01) \/ (L2 \/ L4 \/ LSeg(p10,p2));
p00 in LSeg(p1,p00) & p00 in LSeg(p00,p2) by TOPREAL1:6;
then LSeg(p1,p00) c= L1 & LSeg(p00,p2) c= L3 &
p00 in LSeg(p1,p00) /\ LSeg(p00,p2) by A3,A121,Lm13,Lm14,TOPREAL1:12,
XBOOLE_0:def 3;
then LSeg(p1,p00) /\ LSeg(p00,p2) c= L1 /\ L3 & L1 /\ L3 = {p00}
& LSeg(p1,p00) /\ LSeg(p00,p2) <> {} by TOPREAL1:23,XBOOLE_1:27;
then LSeg(p1,p00) /\ LSeg(p00,p2) = {p00} & (p1 <> p00 or p00 <> p2)
by A1,ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by TOPREAL1:18;
L2 is_an_arc_of p01,p11 & L4 is_an_arc_of p11,p10
by Lm4,TOPREAL1:15;
then A123: L2 \/ L4 is_an_arc_of p01,p10 by TOPREAL1:5,24;
A124: LSeg(p10,p2) c= L3 by A121,Lm17,TOPREAL1:12;
then L2 /\ LSeg(p10,p2) c= L2 /\ L3 by XBOOLE_1:26;
then A125: L2 /\ LSeg(p10,p2) = {} by Lm2,XBOOLE_1:3;
p10 in LSeg(p10,p2) by TOPREAL1:6;
then A126: L4 /\ LSeg(p10,p2) c= L4 /\ L3 & p10 in L4 /\ LSeg(p10,p2)
by A124,Lm18,XBOOLE_0:def 3,XBOOLE_1:27;
(L2 \/ L4) /\ LSeg(p10,p2)
= (L2 /\ LSeg(p10,p2)) \/ (L4 /\ LSeg(p10,p2)) by XBOOLE_1:23
.= {p10} by A125,A126,TOPREAL1:22,ZFMISC_1:39;
then A127: L2 \/ L4 \/
LSeg(p10,p2) is_an_arc_of p01,p2 by A123,TOPREAL1:16;
LSeg(p1,p01) /\ LSeg(p10,p2) c= {p00} by A8,A124,TOPREAL1:23,XBOOLE_1:27;
then A128: LSeg(p1,p01) /\ LSeg(p10,p2) = {p00} or
LSeg(p1,p01) /\ LSeg(p10,p2) = {} by ZFMISC_1:39;
A129: now assume p00 in LSeg(p1,p01) /\ LSeg(p10,p2);
then p00 in LSeg(p1,p01) & p00 in LSeg(p2,p10) & p1`2 <= p01`2 &
p2`1 <= p10`1 by A5,A6,A122,EUCLID:56,XBOOLE_0:def 3;
then A130: p00`2 = p1`2 & p00`2 = p2`2 & p00`1 = p1`1 & p00`1 = p2`1
by A5,A6,A122,Lm4,TOPREAL1:9,10;
then p1 = |[p00`1,p00`2]| by EUCLID:57 .= p2 by A130,EUCLID:57;
hence contradiction by A1;
end;
LSeg(p1,p01) /\ (L2 \/ L4 \/ LSeg(p10,p2))
= (LSeg(p1,p01) /\ (L2 \/ L4)) \/ (LSeg(p1,p01) /\
LSeg(p10,p2)) by XBOOLE_1:23
.= (LSeg(p1,p01) /\ L2) \/ (LSeg(p01,p1) /\ L4) by A128,A129,XBOOLE_1:23,
ZFMISC_1:37
.= {p01} by A14,A15,A16,XBOOLE_0:def 10;
hence P2 is_an_arc_of p1,p2 by A127,TOPREAL1:17;
A131: L1 = LSeg(p1,p00) \/ LSeg(p1,p01) by A3,TOPREAL1:11;
A132: L3 = LSeg(p10,p2) \/ LSeg(p00,p2) by A121,TOPREAL1:11;
thus P1 \/ P2
= LSeg(p00,p2) \/ (LSeg(p1,p00) \/ (LSeg(p1,p01) \/
(L2 \/ L4 \/ LSeg(p10,p2)))) by XBOOLE_1:4
.= L1 \/ (L2 \/ L4 \/ LSeg(p10,p2)) \/ LSeg(p00,p2) by A131,XBOOLE_1:4
.= L1 \/ ((L2 \/ L4 \/ LSeg(p10,p2)) \/ LSeg(p00,p2)) by XBOOLE_1:4
.= L1 \/ (L2 \/ L4 \/ (LSeg(p10,p2) \/ LSeg(p00,p2))) by XBOOLE_1:4
.= L1 \/ (L2 \/ (L3 \/ L4)) by A132,XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:20,XBOOLE_1:4;
A133: LSeg(p00,p2) c= L3 by A121,Lm14,TOPREAL1:12;
A134: {p1} = LSeg(p1,p00) /\ LSeg(p1,p01) by A3,TOPREAL1:14;
A135: LSeg(p00,p2) /\ LSeg(p10,p2) = {p2} by A121,TOPREAL1:14;
LSeg(p00,p2) /\ L2 c= L3 /\ L2 by A133,XBOOLE_1:27;
then A136: LSeg(p00,p2) /\ L2 = {} by Lm2,XBOOLE_1:3;
A137: P1 /\ P2 = (LSeg(p1,p00) /\ (LSeg(p1,p01) \/ (L2 \/ L4 \/
LSeg(p10,p2))))
\/ (LSeg(p00,p2) /\ (LSeg(p1,p01) \/ (L2 \/ L4 \/ LSeg(p10,p2))))
by XBOOLE_1:23
.= (LSeg(p1,p00) /\ LSeg(p1,p01))
\/ (LSeg(p1,p00) /\ (L2 \/ L4 \/ LSeg(p10,p2)))
\/ (LSeg(p00,p2) /\ (LSeg(p1,p01) \/ (L2 \/ L4 \/ LSeg(p10,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ (L2 \/ L4)) \/ (LSeg(p1,p00) /\
LSeg(p10,p2)))
\/ (LSeg(p00,p2) /\ (LSeg(p1,p01) \/ (L2 \/ L4 \/ LSeg(p10,p2))))
by A134,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ L2) \/ (LSeg(p1,p00) /\ L4)
\/ (LSeg(p1,p00) /\ LSeg(p10,p2)))
\/ (LSeg(p00,p2) /\ (LSeg(p1,p01) \/ (L2 \/ L4 \/ LSeg(p10,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ L2) \/ (LSeg(p1,p00) /\ L4)
\/ (LSeg(p1,p00) /\ LSeg(p10,p2)))
\/ ((LSeg(p00,p2) /\ LSeg(p1,p01))
\/ (LSeg(p00,p2) /\ (L2 \/ L4 \/ LSeg(p10,p2)))) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ L2) \/ (LSeg(p1,p00) /\ L4)
\/ (LSeg(p1,p00) /\ LSeg(p10,p2)))
\/ ((LSeg(p00,p2) /\ LSeg(p1,p01))
\/ ((LSeg(p00,p2) /\ (L2 \/ L4)) \/ {p2})) by A135,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ L2) \/ (LSeg(p1,p00) /\ L4)
\/ (LSeg(p1,p00) /\ LSeg(p10,p2)))
\/ ((LSeg(p00,p2) /\ LSeg(p1,p01))
\/ ((LSeg(p00,p2) /\ L2) \/ (LSeg(p00,p2) /\ L4) \/ {p2})) by XBOOLE_1:
23
.= {p1} \/ ((LSeg(p1,p00) /\ L2) \/ (LSeg(p1,p00) /\ LSeg(p10,p2)))
\/ ((LSeg(p00,p2) /\ LSeg(p1,p01)) \/ (LSeg(p00,p2) /\ L4 \/ {p2}))
by A10,A136;
A138: now per cases;
suppose A139: p2 = p10;
then not p2 in LSeg(p1,p00) by A7,Lm4,TOPREAL1:9;
then A140: LSeg(p1,p00) misses {p2} by ZFMISC_1:56;
LSeg(p1,p00) /\ LSeg(p10,p2) = LSeg(p1,p00) /\ {p2} by A139,TOPREAL1:7
.= {} by A140,XBOOLE_0:def 7;
hence P1 /\ P2
= {p1} \/ (LSeg(p1,p00) /\ L2) \/ ((LSeg(p00,p2) /\ LSeg(p1,p01))
\/ {p2}) by A137,A139,TOPREAL1:22;
suppose A141: p2 <> p10 & p2 <> p00;
A142: LSeg(p00,p2) /\ L4 c= {p10} by A133,TOPREAL1:22,XBOOLE_1:27;
now assume p10 in LSeg(p00,p2) /\ L4;
then p10 in LSeg(p00,p2) & p00`1 <=
p2`1 by A122,EUCLID:56,XBOOLE_0:def 3;
then p10`1 <= p2`1 by TOPREAL1:9;
then p2`1 = p10`1 & p2`2 = p10`2 by A122,Lm4,AXIOMS:21;
hence contradiction by A141,Lm4,EUCLID:57;
end;
then {p10} <> LSeg(p00,p2) /\ L4 by ZFMISC_1:37;
then A143: LSeg(p00,p2) /\ L4 = {} by A142,ZFMISC_1:39;
A144: LSeg(p1,p00) /\ LSeg(p10,p2) c= {p00} by A7,A124,TOPREAL1:23,
XBOOLE_1:27;
now assume p00 in LSeg(p1,p00) /\ LSeg(p10,p2);
then p00 in
LSeg(p2,p10) & p2`1 <= p10`1 by A122,EUCLID:56,XBOOLE_0:def 3;
then p2`1 = 0 & p2`2 = 0 by A122,Lm4,TOPREAL1:9;
hence contradiction by A141,EUCLID:57;
end;
then {p00} <> LSeg(p1,p00) /\ LSeg(p10,p2) by ZFMISC_1:37;
then LSeg(p1,p00) /\ LSeg(p10,p2) = {} by A144,ZFMISC_1:39;
hence P1 /\ P2
= {p1} \/ (LSeg(p1,p00) /\ L2) \/ ((LSeg(p00,p2) /\ LSeg(p1,p01)) \/
{p2})
by A137,A143;
suppose A145: p2 = p00;
then A146: LSeg(p00,p2) /\ L4 = {p00} /\ L4 by TOPREAL1:7
.= {} by Lm1,Lm5;
A147: LSeg(p1,p00) /\
LSeg(p10,p2) c= {p2} by A7,A145,TOPREAL1:23,XBOOLE_1:27;
p2 in LSeg(p1,p00) by A145,TOPREAL1:6;
then LSeg(p1,p00) /\ LSeg(p10,p2) <> {}
by A145,Lm14,XBOOLE_0:def 3;
then LSeg(p1,p00) /\ LSeg(p10,p2) = {p2} by A147,ZFMISC_1:39;
hence P1 /\ P2
= ({p1} \/ (LSeg(p1,p00) /\ L2)) \/ {p2} \/ ((LSeg(p00,p2) /\
LSeg(p1,p01))
\/ {p2}) by A137,A146,XBOOLE_1:4
.= ({p1} \/ (LSeg(p1,p00) /\ L2)) \/ ((LSeg(p00,p2) /\ LSeg(p1,p01))
\/ {p2} \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ (LSeg(p1,p00) /\ L2)) \/ ((LSeg(p00,p2) /\ LSeg(p1,p01))
\/ ({p2} \/ {p2})) by XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p00) /\ L2) \/ ((LSeg(p00,p2) /\ LSeg(p1,p01)) \/
{p2});
end;
now per cases;
suppose A148: p1 = p01;
then A149: LSeg(p00,p2) /\ LSeg(p1,p01) = LSeg(p00,p2) /\ {p1} by
TOPREAL1:7;
not p1 in LSeg(p00,p2) by A133,A148,Lm4,TOPREAL1:10;
then LSeg(p00,p2) /\ LSeg(p1,p01) = {} by A149,Lm1;
hence P1 /\ P2
= {p1,p2} by A138,A148,ENUMSET1:41,TOPREAL1:21;
suppose A150: p1 = p00;
then LSeg(p1,p00) /\ L2 = {p1} /\ L2 by TOPREAL1:7;
then A151:LSeg(p1,p00) /\ L2 = {} by A150,Lm1,Lm6;
A152: LSeg(p00,p2) /\ LSeg(p1,p01) c= L3 /\ L1 by A133,A150,XBOOLE_1:26;
p00 in LSeg(p00,p2) by TOPREAL1:6;
then LSeg(p00,p2) /\ LSeg(p1,p01) <> {} by A150,Lm13,XBOOLE_0:def
3
;
then LSeg(p00,p2) /\ LSeg(p1,p01) = {p1} by A150,A152,TOPREAL1:23,
ZFMISC_1:39;
hence P1 /\ P2
= {p1} \/ {p1} \/ {p2} by A138,A151,XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41;
suppose A153: p1 <> p00 & p1 <> p01;
A154: LSeg(p1,p00) /\ L2 c= {p01} by A7,TOPREAL1:21,XBOOLE_1:27;
now assume p01 in LSeg(p1,p00) /\ L2;
then p01 in LSeg(p00,p1) & p00`2 <= p1`2
by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p01`2 <= p1`2 by TOPREAL1:10;
then p1`2 = 1 by A5,A6,Lm4,AXIOMS:21;
hence contradiction by A5,A6,A153,EUCLID:57;
end;
then {p01} <> LSeg(p1,p00) /\ L2 by ZFMISC_1:37;
then A155: LSeg(p1,p00) /\ L2 = {} by A154,ZFMISC_1:39;
A156: LSeg(p00,p2) /\ LSeg(p1,p01) c= L3 /\ L1 by A8,A133,XBOOLE_1:27;
now assume p00 in LSeg(p00,p2) /\ LSeg(p1,p01);
then p00 in LSeg(p1,p01) & p1`2 <= p01`2
by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p1`2 = 0 by A5,A6,Lm4,TOPREAL1:10;
hence contradiction by A5,A6,A153,EUCLID:57;
end;
then {p00} <> LSeg(p00,p2) /\ LSeg(p1,p01) by ZFMISC_1:37;
then LSeg(p00,p2) /\ LSeg(p1,p01) = {}
by A156,TOPREAL1:23,ZFMISC_1:39;
hence P1 /\ P2
= {p1,p2} by A138,A155,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
suppose A157: p2 in L4;
then A158: ex q st q = p2 & q`1 = 1 & q`2 <= 1 & q`2 >= 0 by TOPREAL1:19;
take P1 = LSeg(p1,p00) \/ L3 \/ LSeg(p10,p2),P2
= LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2);
LSeg(p10,p2) c= L4 & p10 in L3 & p10 in LSeg(p10,p2)
by A157,Lm18,TOPREAL1:6,12;
then L3 /\ LSeg(p10,p2) c= {p10} & L3 /\ LSeg(p10,p2) <> {}
by TOPREAL1:22,XBOOLE_0:def 3,XBOOLE_1:27;
then L3 /\ LSeg(p10,p2) = {p10} by ZFMISC_1:39;
then A159: L3 \/ LSeg(p10,p2) is_an_arc_of p00,p2 by Lm4,TOPREAL1:18;
LSeg(p10,p2) c= L4 by A157,Lm18,TOPREAL1:12;
then LSeg(p1,p00) /\ LSeg(p10,p2) c= L1 /\ L4 by A7,XBOOLE_1:27;
then A160: LSeg(p1,p00) /\ LSeg(p10,p2) = {} by Lm3,XBOOLE_1:3;
LSeg(p1,p00) /\ (L3 \/ LSeg(p10,p2))
= (LSeg(p1,p00) /\ L3) \/ (LSeg(p1,p00) /\ LSeg(p10,p2)) by XBOOLE_1:23
.= {p00} by A11,A12,A160,XBOOLE_0:def 10;
then LSeg(p1,p00) \/ (L3 \/ LSeg(p10,p2)) is_an_arc_of p1,p2
by A159,TOPREAL1:17;
hence P1 is_an_arc_of p1,p2 by XBOOLE_1:4;
A161: LSeg(p11,p2) c= L4 by A157,Lm20,TOPREAL1:12;
then L2 /\ LSeg(p11,p2) c= L2 /\ L4 & p11 in LSeg(p11,p2)
by TOPREAL1:6,XBOOLE_1:27;
then L2 /\ LSeg(p11,p2) c= {p11} & L2 /\ LSeg(p11,p2) <> {}
by Lm19,TOPREAL1:24,XBOOLE_0:def 3;
then L2 /\ LSeg(p11,p2) = {p11} by ZFMISC_1:39;
then A162: L2 \/ LSeg(p11,p2) is_an_arc_of p01,p2 by Lm4,TOPREAL1:18;
LSeg(p1,p01) /\ LSeg(p11,p2) c= L1 /\ L4 by A8,A161,XBOOLE_1:27;
then A163: LSeg(p1,p01) /\ LSeg(p11,p2) = {} by Lm3,XBOOLE_1:3;
LSeg(p1,p01) /\ (L2 \/ LSeg(p11,p2))
= (LSeg(p1,p01) /\ L2) \/ (LSeg(p1,p01) /\ LSeg(p11,p2)) by XBOOLE_1:23
.= {p01} by A15,A16,A163,XBOOLE_0:def 10;
then LSeg(p1,p01) \/ (L2 \/ LSeg(p11,p2)) is_an_arc_of p1,p2
by A162,TOPREAL1:17;
hence P2 is_an_arc_of p1,p2 by XBOOLE_1:4;
thus R^2-unit_square = LSeg(p1,p00) \/ LSeg(p1,p01) \/ L2 \/ (L3 \/
L4) by A3,TOPREAL1:11,20
.= LSeg(p1,p00) \/ (LSeg(p1,p01) \/ L2) \/ (L3 \/ L4) by XBOOLE_1:4
.= LSeg(p1,p00) \/ ((LSeg(p1,p01) \/ L2) \/ (L3 \/ L4)) by XBOOLE_1:4
.= LSeg(p1,p00) \/ (L3 \/ (LSeg(p1,p01) \/ L2 \/ L4)) by XBOOLE_1:4
.= LSeg(p1,p00) \/ L3 \/ (LSeg(p1,p01) \/ L2 \/ L4) by XBOOLE_1:4
.= LSeg(p1,p00) \/ L3 \/ (LSeg(p1,p01) \/ L2
\/ (LSeg(p11,p2) \/ LSeg(p10,p2))) by A157,TOPREAL1:11
.= LSeg(p1,p00) \/ L3 \/ (LSeg(p10,p2)
\/ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4;
p1 in LSeg(p1,p00) & p1 in LSeg(p1,p01) by TOPREAL1:6;
then p1 in LSeg(p1,p00) /\ LSeg(p1,p01) by XBOOLE_0:def 3;
then A164: {p1} c= LSeg(p1,p00) /\ LSeg(p1,p01) by ZFMISC_1:37;
now let a; assume A165: a in LSeg(p1,p00) /\ LSeg(p1,p01);
then A166: a in LSeg(p00,p1) & a in LSeg(p1,p01) by XBOOLE_0:def 3;
reconsider p = a as Point of TOP-REAL 2 by A165;
p`1 <= p1`1 & p1`1 <= p`1 & p`2 <= p1`2 & p1`2 <= p`2
by A5,A6,A166,Lm4,TOPREAL1:9,10;
then p`1 = p1`1 & p`2 = p1`2 by AXIOMS:21;
then a = |[p1`1,p1`2]| by EUCLID:57 .= p1 by EUCLID:57;
hence a in {p1} by TARSKI:def 1;
end;
then LSeg(p1,p00) /\ LSeg(p1,p01) c= {p1} by TARSKI:def 3;
then A167: LSeg(p1,p00) /\ LSeg(p1,p01) = {p1} by A164,XBOOLE_0:def 10;
LSeg(p1,p00) /\ LSeg(p11,p2) c= L1 /\ L4 by A7,A161,XBOOLE_1:27;
then A168: LSeg(p1,p00) /\ LSeg(p11,p2) = {} by Lm3,XBOOLE_1:3;
p2 in LSeg(p10,p2) & p2 in LSeg(p11,p2) by TOPREAL1:6;
then p2 in LSeg(p10,p2) /\ LSeg(p11,p2) by XBOOLE_0:def 3;
then A169: {p2} c= LSeg(p10,p2) /\ LSeg(p11,p2) by ZFMISC_1:37;
now let a; assume A170: a in LSeg(p10,p2) /\ LSeg(p11,p2);
then A171: a in LSeg(p10,p2) & a in LSeg(p2,p11) by XBOOLE_0:def 3;
reconsider p = a as Point of TOP-REAL 2 by A170;
p`2 <= p2`2 & p2`2 <= p`2 & p`1 <= p2`1 & p2`1 <= p`1
by A158,A171,Lm4,TOPREAL1:9,10;
then p`2 = p2`2 & p`1 = p2`1 by AXIOMS:21;
then a = |[p2`1,p2`2]| by EUCLID:57 .= p2 by EUCLID:57;
hence a in {p2} by TARSKI:def 1;
end;
then A172: LSeg(p10,p2) /\ LSeg(p11,p2) c= {p2} by TARSKI:def 3;
A173: LSeg(p10,p2) c= L4 by A157,Lm18,TOPREAL1:12;
then LSeg(p10,p2) /\ LSeg(p1,p01) c= L4 /\ L1 by A8,XBOOLE_1:27;
then A174: LSeg(p10,p2) /\ LSeg(p1,p01) = {} by Lm3,XBOOLE_1:3;
A175: P1 /\ P2
= (LSeg(p1,p00) \/ L3) /\ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2))) by XBOOLE_1:
23
.= (LSeg(p1,p00) /\ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2)))
\/ (L3 /\ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2))) by XBOOLE_1:
23
.= (LSeg(p1,p00) /\ (LSeg(p1,p01) \/ L2))
\/ (LSeg(p1,p00) /\ LSeg(p11,p2))
\/ (L3 /\ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2))) by XBOOLE_1:
23
.= (LSeg(p1,p00) /\ LSeg(p1,p01)) \/ (LSeg(p1,p00) /\ L2)
\/ (L3 /\ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L2 \/
LSeg(p11,p2))) by A168,XBOOLE_1:23
.= {p1} \/ (LSeg(p1,p00) /\ L2)
\/ ((L3 /\ (LSeg(p1,p01) \/ L2)) \/ (L3 /\ LSeg(p11,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L2 \/
LSeg(p11,p2))) by A167,XBOOLE_1:23
.= {p1} \/ (LSeg(p1,p00) /\ L2)
\/ ((L3 /\ LSeg(p1,p01)) \/ (L3 /\ L2) \/ (L3 /\ LSeg(p11,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L2 \/ LSeg(p11,p2))) by XBOOLE_1:
23
.= {p1} \/ (LSeg(p1,p00) /\ L2)
\/ ((L3 /\ LSeg(p1,p01)) \/ (L3 /\ LSeg(p11,p2)))
\/ ((LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L2))
\/ (LSeg(p10,p2) /\ LSeg(p11,p2))) by Lm2,XBOOLE_1:23
.= {p1} \/ (LSeg(p1,p00) /\ L2)
\/ ((L3 /\ LSeg(p1,p01)) \/ (L3 /\ LSeg(p11,p2)))
\/ ((LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L2)) \/
{p2}) by A169,A172,XBOOLE_0:def 10
.= {p1} \/ (LSeg(p1,p00) /\ L2)
\/ ((L3 /\ LSeg(p1,p01)) \/ (L3 /\ LSeg(p11,p2)))
\/ ((LSeg(p10,p2) /\ LSeg(p1,p01)) \/ (LSeg(p10,p2) /\ L2) \/ {p2})
by XBOOLE_1:23
.= {p1} \/ (LSeg(p1,p00) /\ L2)
\/ ((L3 /\ LSeg(p1,p01)) \/ (L3 /\ LSeg(p11,p2)))
\/ ((LSeg(p10,p2) /\ L2) \/ {p2}) by A174;
A176: now per cases;
suppose A177: p2 = p11;
then L3 /\ LSeg(p11,p2) = L3 /\ {p11} by TOPREAL1:7
.= {} by Lm1,Lm12;
hence P1 /\ P2 = {p1} \/ (LSeg(p1,p00) /\ L2) \/ (L3 /\ LSeg(p1,p01)) \/
{p2}
by A175,A177,TOPREAL1:24;
suppose A178: p2 = p10;
then LSeg(p10,p2) /\ L2 = {p10} /\ L2 by TOPREAL1:7
.= {} by Lm1,Lm10;
hence P1 /\ P2 = {p1} \/ (LSeg(p1,p00) /\ L2)
\/ ((L3 /\ LSeg(p1,p01)) \/ {p2} \/
{p2}) by A175,A178,TOPREAL1:22,XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p00) /\ L2)
\/ ((L3 /\ LSeg(p1,p01)) \/ ({p2} \/ {p2})) by XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p00) /\ L2) \/ (L3 /\ LSeg(p1,p01)) \/ {p2}
by XBOOLE_1:4;
suppose A179: p2 <> p10 & p2 <> p11;
A180: L3 /\ LSeg(p11,p2) c= {p10} by A161,TOPREAL1:22,XBOOLE_1:27;
now assume p10 in L3 /\ LSeg(p11,p2);
then p10 in LSeg(p2,p11) & p2`2 <= p11`2 by A158,EUCLID:56,XBOOLE_0:def
3;
then p2`2 = p10`2 & p2`1 = p10`1 by A158,Lm4,TOPREAL1:10;
then p2 = |[p10`1,p10`2]| by EUCLID:57 .= p10 by EUCLID:57;
hence contradiction by A179;
end;
then L3 /\ LSeg(p11,p2) <> {p10} by ZFMISC_1:37;
then A181: L3 /\ LSeg(p11,p2) = {} by A180,ZFMISC_1:39;
A182: LSeg(p10,p2) /\ L2 c= L4 /\ L2 by A173,XBOOLE_1:27;
now assume p11 in LSeg(p10,p2) /\ L2;
then p11 in LSeg(p10,p2) & p10`2 <= p2`2 by A158,EUCLID:56,XBOOLE_0:def
3;
then p11`2 <= p2`2 by TOPREAL1:10;
then p11`2 = p2`2 & p11`1 = p2`1 by A158,Lm4,AXIOMS:21;
then p2 = |[p11`1,p11`2]| by EUCLID:57 .= p11 by EUCLID:57;
hence contradiction by A179;
end;
then {p11} <> LSeg(p10,p2) /\ L2 by ZFMISC_1:37;
then LSeg(p10,p2) /\ L2 = {} by A182,TOPREAL1:24,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (LSeg(p1,p00) /\ L2) \/ (L3 /\ LSeg(p1,p01)) \/
{p2} by A175,A181;
end;
now per cases;
suppose A183: p1 = p01;
then L3 /\ LSeg(p1,p01) = L3 /\ {p01} by TOPREAL1:7
.= {} by Lm1,Lm7;
hence P1 /\ P2 = {p1,p2} by A176,A183,ENUMSET1:41,TOPREAL1:21;
suppose A184: p1 <> p01 & p1 <> p00;
A185:
L3 /\ LSeg(p1,p01) c= L3 /\ L1 by A8,XBOOLE_1:27;
now assume p00 in L3 /\ LSeg(p1,p01);
then p00 in LSeg(p1,p01) by XBOOLE_0:def 3;
then p1`2 = p00`2 & p1`1 = p00`1 by A5,A6,Lm4,TOPREAL1:10;
then p1 = |[p00`1,p00`2]| by EUCLID:57 .= p00 by EUCLID:57;
hence contradiction by A184;
end;
then {p00} <> L3 /\ LSeg(p1,p01) by ZFMISC_1:37;
then A186: L3 /\ LSeg(p1,p01) = {} by A185,TOPREAL1:23,ZFMISC_1:39;
A187: LSeg(p1,p00) /\ L2 c= {p01} by A7,TOPREAL1:21,XBOOLE_1:27;
now assume p01 in LSeg(p1,p00) /\ L2;
then A188: p01 in LSeg(p00,p1) by XBOOLE_0:def 3;
p00`2 <= p1`2 by A5,A6,EUCLID:56;
then p01`2 <= p1`2 by A188,TOPREAL1:10;
then p1`2 = p01`2 & p1`1 = p01`1 by A5,A6,Lm4,AXIOMS:21;
then p1 = |[p01`1,p01`2]| by EUCLID:57 .= p01 by EUCLID:57;
hence contradiction by A184;
end;
then {p01} <> LSeg(p1,p00) /\ L2 by ZFMISC_1:37;
then LSeg(p1,p00) /\ L2 = {} by A187,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A176,A186,ENUMSET1:41;
suppose A189: p1 = p00;
then LSeg(p1,p00) /\ L2 = {p00} /\ L2 by TOPREAL1:7
.= {} by Lm1,Lm6;
hence P1 /\ P2 = {p1,p2} by A176,A189,ENUMSET1:41,TOPREAL1:23;
end;
hence P1 /\ P2 = {p1,p2};
end;
Lm24:
p1 <> p2 & p2 in R^2-unit_square &
p1 in LSeg(p01, p11) implies
ex P1,P2 being non empty Subset of TOP-REAL 2
st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 &
R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2}
proof assume that
A1: p1 <> p2 and
A2: p2 in R^2-unit_square and
A3: p1 in LSeg(p01, p11);
A4: p2 in L1 \/ L2 or p2 in L3 \/ L4 by A2,TOPREAL1:20,XBOOLE_0:def 2;
consider q1 such that
A5: q1 = p1 and A6: q1`1 <= 1 & q1`1 >= 0 & q1`2 = 1 by A3,TOPREAL1:19;
A7: LSeg(p01,p1) c= L2 by A3,Lm16,TOPREAL1:12;
A8: LSeg(p1,p11) c= L2 by A3,Lm19,TOPREAL1:12;
LSeg(p1,p01) /\ L3 c= L2 /\ L3 by A7,XBOOLE_1:26;
then A9: LSeg(p1,p01) /\ L3 = {} by Lm2,XBOOLE_1:3;
p01 in LSeg(p01,p1) by TOPREAL1:6;
then A10: LSeg(p01,p1) /\ L1 <> {} by Lm15,XBOOLE_0:def 3;
A11: LSeg(p01,p1) /\ L1 c= L2 /\ L1 by A7,XBOOLE_1:26;
LSeg(p1,p11) /\ L3 c= L2 /\ L3 by A8,XBOOLE_1:26;
then A12: LSeg(p1,p11) /\ L3 = {} by Lm2,XBOOLE_1:3;
p11 in LSeg(p1,p11) by TOPREAL1:6;
then A13: LSeg(p1,p11) /\ L4 <> {} by Lm20,XBOOLE_0:def 3;
A14: LSeg(p1,p11) /\ L4 c= {p11} by A8,TOPREAL1:24,XBOOLE_1:26;
per cases by A4,XBOOLE_0:def 2;
suppose A15: p2 in L1;
then A16: ex q2 st q2 = p2 & q2`1 = 0 & q2`2 <= 1 & q2`2 >= 0 by TOPREAL1:
19;
A17: p1 <> p01 or p2 <> p01 by A1;
take P1 = LSeg(p1,p01) \/ LSeg(p01,p2),P2
= LSeg(p1,p11) \/ (L3 \/ L4 \/ LSeg(p00,p2));
p01 in LSeg(p1,p01) & p01 in LSeg(p01,p2) by TOPREAL1:6;
then LSeg(p1,p01) c= L2 & LSeg(p01,p2) c= L1 &
p01 in LSeg(p1,p01) /\ LSeg(p01,p2) by A3,A15,Lm15,Lm16,TOPREAL1:12,
XBOOLE_0:def 3;
then LSeg(p1,p01) /\ LSeg(p01,p2) c= L2 /\ L1
& LSeg(p1,p01) /\ LSeg(p01,p2) <> {} by XBOOLE_1:27;
then LSeg(p1,p01) /\ LSeg(p01,p2) = {p01} by TOPREAL1:21,ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by A17,TOPREAL1:18;
L3 is_an_arc_of p10,p00 & L4 is_an_arc_of p11,p10 by Lm4,TOPREAL1:15;
then A18: L3 \/ L4 is_an_arc_of p11,p00 by TOPREAL1:5,22;
A19: LSeg(p00,p2) c= L1 & p00 in LSeg(p00,p2) by A15,Lm13,TOPREAL1:6,12;
then A20: L3 /\ LSeg(p00,p2) c= {p00} & {} <> L3 /\ LSeg(p00,p2)
by Lm14,TOPREAL1:23,XBOOLE_0:def 3,XBOOLE_1:26;
L4 /\ LSeg(p00,p2) c= L4 /\ L1 by A19,XBOOLE_1:27;
then A21: L4 /\ LSeg(p00,p2) = {} by Lm3,XBOOLE_1:3;
A22: LSeg(p2,p01) c= L1 by A15,Lm15,TOPREAL1:12;
(L3 \/ L4) /\ LSeg(p00,p2)
= (L3 /\ LSeg(p00,p2)) \/ (L4 /\ LSeg(p00,p2)) by XBOOLE_1:23
.= {p00} by A20,A21,ZFMISC_1:39;
then A23: L3 \/ L4 \/ LSeg(p00,p2) is_an_arc_of p11,p2 by A18,TOPREAL1:16;
LSeg(p1,p11) /\ LSeg(p00,p2) c= L2 /\ L1 by A8,A19,XBOOLE_1:27;
then A24: LSeg(p1,p11) /\ LSeg(p00,p2) = {p01} or
LSeg(p1,p11) /\ LSeg(p00,p2) = {} by TOPREAL1:21,ZFMISC_1:39;
A25: now assume p01 in LSeg(p1,p11) /\ LSeg(p00,p2);
then p01 in LSeg(p1,p11) & p01 in LSeg(p00,p2) & p1`1 <= p11`1 &
p00`2 <= p2`2 by A5,A6,A16,EUCLID:56,XBOOLE_0:def 3;
then p01`2 <= p2`2 & p1`1 <= p01`1 by TOPREAL1:9,10;
then A26: p01`2 = p1`2 & p01`2 = p2`2 & p01`1 = p1`1 & p01`1 = p2`1
by A5,A6,A16,Lm4,AXIOMS:21;
then p1 = |[p01`1,p01`2]| by EUCLID:57 .= p2 by A26,EUCLID:57;
hence contradiction by A1;
end;
LSeg(p1,p11) /\ (L3 \/ L4 \/ LSeg(p00,p2))
= (LSeg(p1,p11) /\ (L3 \/ L4)) \/ (LSeg(p1,p11) /\
LSeg(p00,p2)) by XBOOLE_1:23
.= (LSeg(p1,p11) /\ L3) \/ (LSeg(p1,p11) /\ L4) by A24,A25,XBOOLE_1:23,
ZFMISC_1:37
.= {p11} by A12,A13,A14,ZFMISC_1:39;
hence P2 is_an_arc_of p1,p2 by A23,TOPREAL1:17;
A27: LSeg(p1,p01) \/ LSeg(p1,p11) = L2 by A3,TOPREAL1:11;
A28: LSeg(p00,p2) \/ LSeg(p01,p2) = L1 by A15,TOPREAL1:11;
thus P1 \/ P2
= LSeg(p01,p2) \/ (LSeg(p1,p01) \/ (LSeg(p1,p11) \/
(L3 \/ L4 \/ LSeg(p00,p2)))) by XBOOLE_1:4
.= LSeg(p01,p2) \/ (L2 \/ (L3 \/ L4 \/ LSeg(p00,p2))) by A27,XBOOLE_1:4
.= LSeg(p01,p2) \/ (L2 \/ (L3 \/ L4) \/ LSeg(p00,p2)) by XBOOLE_1:4
.= LSeg(p00,p2) \/ LSeg(p01,p2) \/ (L2 \/ (L3 \/ L4)) by XBOOLE_1:4
.= R^2-unit_square by A28,TOPREAL1:20,XBOOLE_1:4;
A29: {p1} = LSeg(p1,p01) /\ LSeg(p1,p11) by A3,TOPREAL1:14;
A30: LSeg(p01,p2) /\ LSeg(p00,p2) = {p2} by A15,TOPREAL1:14;
LSeg(p01,p2) /\ L4 c= {} by A22,Lm3,XBOOLE_1:27;
then A31: LSeg(p01,p2) /\ L4 = {} by XBOOLE_1:3;
A32: P1 /\ P2 = (LSeg(p1,p01) /\ (LSeg(p1,p11) \/ (L3 \/ L4 \/
LSeg(p00,p2))))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p11) \/ (L3 \/ L4 \/ LSeg(p00,p2))))
by XBOOLE_1:23
.= (LSeg(p1,p01) /\ LSeg(p1,p11))
\/ (LSeg(p1,p01) /\ (L3 \/ L4 \/ LSeg(p00,p2)))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p11) \/ (L3 \/ L4 \/ LSeg(p00,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ (L3 \/ L4)) \/ (LSeg(p1,p01) /\
LSeg(p00,p2)))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p11) \/ (L3 \/ L4 \/ LSeg(p00,p2))))
by A29,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ L3) \/ (LSeg(p1,p01) /\ L4)
\/ (LSeg(p1,p01) /\ LSeg(p00,p2)))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p11) \/ (L3 \/ L4 \/ LSeg(p00,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ L3) \/ (LSeg(p1,p01) /\ L4)
\/ (LSeg(p1,p01) /\ LSeg(p00,p2)))
\/ ((LSeg(p01,p2) /\ LSeg(p1,p11))
\/ (LSeg(p01,p2) /\ (L3 \/ L4 \/ LSeg(p00,p2)))) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ L4) \/ (LSeg(p1,p01) /\ LSeg(p00,p2)))
\/ ((LSeg(p01,p2) /\ LSeg(p1,p11))
\/ ((LSeg(p01,p2) /\ (L3 \/ L4)) \/ {p2})) by A9,A30,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p01) /\ L4) \/ (LSeg(p1,p01) /\ LSeg(p00,p2)))
\/ ((LSeg(p01,p2) /\ LSeg(p1,p11))
\/ ((LSeg(p01,p2) /\ L3) \/ (LSeg(p01,p2) /\ L4) \/ {p2})) by XBOOLE_1:
23
.= {p1} \/ ((LSeg(p1,p01) /\ L4) \/ (LSeg(p1,p01) /\ LSeg(p00,p2)))
\/ ((LSeg(p01,p2) /\ LSeg(p1,p11))
\/ ((LSeg(p01,p2) /\ L3) \/ {p2})) by A31;
A33: now per cases;
suppose A34: p1 = p01;
then LSeg(p1,p01) /\ L4 = {p1} /\ L4 by TOPREAL1:7;
then A35: LSeg(p1,p01) /\ L4 = {} by A34,Lm1,Lm8;
A36: LSeg(p01,p2) /\ LSeg(p1,p11) c= {p1} by A22,A34,TOPREAL1:21,XBOOLE_1:27;
p1 in LSeg(p01,p2) by A34,TOPREAL1:6;
then LSeg(p01,p2) /\ LSeg(p1,p11) <> {} by A34,Lm16,XBOOLE_0:def 3;
then LSeg(p01,p2) /\ LSeg(p1,p11) = {p1} by A36,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ({p1} \/ (LSeg(p1,p01) /\ LSeg(p00,p2)))
\/ ((LSeg(p01,p2) /\ L3) \/ {p2}) by A32,A35,XBOOLE_1:4
.= {p1} \/ {p1} \/ (LSeg(p1,p01) /\ LSeg(p00,p2))
\/ ((LSeg(p01,p2) /\ L3) \/ {p2}) by XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p01) /\ LSeg(p00,p2))
\/ ((LSeg(p01,p2) /\ L3) \/ {p2});
suppose A37: p1 = p11;
then A38: LSeg(p01,p2) /\ LSeg(p1,p11) = LSeg(p01,p2) /\ {p1} by TOPREAL1:7;
not p1 in LSeg(p01,p2) by A16,A37,Lm4,TOPREAL1:9;
then LSeg(p01,p2) /\ LSeg(p1,p11) = {} by A38,Lm1;
hence P1 /\ P2 = {p1} \/ {p1} \/ (LSeg(p1,p01) /\ LSeg(p00,p2))
\/ ((LSeg(p01,p2) /\ L3) \/ {p2}) by A32,A37,TOPREAL1:24,XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p01) /\ LSeg(p00,p2))
\/ ((LSeg(p01,p2) /\ L3) \/ {p2});
suppose A39: p1 <> p11 & p1 <> p01;
A40: LSeg(p1,p01) /\ L4 c= {p11} by A7,TOPREAL1:24,XBOOLE_1:27;
now assume p11 in LSeg(p1,p01) /\ L4;
then p11 in LSeg(p01,p1) & p01`1 <= p1`1 by A5,A6,EUCLID:56,XBOOLE_0:def
3;
then p11`1 <= p1`1 by TOPREAL1:9;
then p1`1 = 1 by A5,A6,Lm4,AXIOMS:21;
hence contradiction by A5,A6,A39,EUCLID:57;
end;
then {p11} <> LSeg(p1,p01) /\ L4 by ZFMISC_1:37;
then A41: LSeg(p1,p01) /\ L4 = {} by A40,ZFMISC_1:39;
A42: LSeg(p01,p2) /\ LSeg(p1,p11) c= {p01} by A8,A22,TOPREAL1:21,XBOOLE_1:27;
now assume p01 in LSeg(p01,p2) /\ LSeg(p1,p11);
then p01 in LSeg(p1,p11) & p1`1 <= p11`1 by A5,A6,EUCLID:56,XBOOLE_0:def
3;
then p1`1 = 0 by A5,A6,Lm4,TOPREAL1:9;
hence contradiction by A5,A6,A39,EUCLID:57;
end;
then {p01} <> LSeg(p01,p2) /\ LSeg(p1,p11) by ZFMISC_1:37;
then LSeg(p01,p2) /\ LSeg(p1,p11) = {} by A42,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (LSeg(p1,p01) /\ LSeg(p00,p2))
\/ ((LSeg(p01,p2) /\ L3) \/ {p2}) by A32,A41;
end;
now per cases;
suppose A43: p2 <> p00 & p2 <> p01;
A44: LSeg(p1,p01) /\ LSeg(p00,p2) c= L2 /\ L1 by A7,A19,XBOOLE_1:27;
now assume p01 in LSeg(p1,p01) /\ LSeg(p00,p2);
then p01 in LSeg(p00,p2) & p00`2 <= p2`2 by A16,EUCLID:56,XBOOLE_0:def 3
;
then p01`2 <= p2`2 by TOPREAL1:10;
then p2`2 = 1 by A16,Lm4,AXIOMS:21;
hence contradiction by A16,A43,EUCLID:57;
end;
then {p01} <> LSeg(p1,p01) /\ LSeg(p00,p2) by ZFMISC_1:37;
then A45: LSeg(p1,p01) /\ LSeg(p00,p2) = {} by A44,TOPREAL1:21,ZFMISC_1:39;
A46: LSeg(p01,p2) /\ L3 c= {p00} by A22,TOPREAL1:23,XBOOLE_1:27;
now assume p00 in LSeg(p01,p2) /\ L3;
then p00 in LSeg(p2,p01) & p2`2 <= p01`2 by A16,EUCLID:56,XBOOLE_0:def
3;
then 0 = p2`2 by A16,Lm4,TOPREAL1:10;
hence contradiction by A16,A43,EUCLID:57;
end;
then {p00} <> LSeg(p01,p2) /\ L3 by ZFMISC_1:37;
then LSeg(p01,p2) /\ L3 = {} by A46,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A33,A45,ENUMSET1:41;
suppose A47:p2 = p00;
then A48: LSeg(p1,p01) /\ LSeg(p00,p2) = LSeg(p1,p01) /\
{p00} by TOPREAL1:7;
not p00 in LSeg(p1,p01) by A7,Lm4,TOPREAL1:10;
then LSeg(p1,p01) /\ LSeg(p00,p2) = {} by A48,Lm1;
hence P1 /\ P2 = {p1,p2} by A33,A47,ENUMSET1:41,TOPREAL1:23;
suppose A49: p2 = p01;
then LSeg(p01,p2) /\ L3 = {p01} /\ L3 by TOPREAL1:7;
then A50: LSeg(p01,p2) /\ L3 = {} by Lm1,Lm7;
A51: LSeg(p1,p01) /\ LSeg(p00,p2) c= L2 /\ L1 by A7,A19,XBOOLE_1:27;
p2 in LSeg(p1,p01) by A49,TOPREAL1:6;
then {} <> LSeg(p1,p01) /\ LSeg(p00,p2) by A49,Lm15,XBOOLE_0:def 3;
then LSeg(p1,p01) /\ LSeg(p00,p2) = {p2} by A49,A51,TOPREAL1:21,ZFMISC_1:39
;
hence P1 /\ P2
= {p1} \/ ({p2} \/ {p2}) by A33,A50,XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
suppose A52: p2 in L2;
then consider q such that
A53: q = p2 and A54: q`1 <= 1 & q`1 >= 0 & q`2 = 1 by TOPREAL1:19;
A55: q1 = |[q1`1,q1`2]| & q = |[q`1,q`2]| by EUCLID:57;
A56: LSeg(p2,p11) c= L2 by A52,Lm19,TOPREAL1:12;
A57: LSeg(p2,p01) c= L2 by A52,Lm16,TOPREAL1:12;
A58: LSeg(p1,p2) c= L2 by A3,A52,TOPREAL1:12;
now per cases by A1,A5,A6,A53,A54,A55,REAL_1:def 5;
suppose A59: q1`1 < q`1;
take P1 = LSeg(p1,p2),P2 = LSeg(p1,p01) \/ (L1 \/ L3 \/ L4 \/
LSeg(p11,p2));
thus P1 is_an_arc_of p1,p2 by A1,TOPREAL1:15;
A60: now assume
A61: LSeg(p1,p01) /\ LSeg(p11,p2) <> {};
consider a being Element of LSeg(p1,p01) /\ LSeg(p11,p2);
reconsider p = a as Point of TOP-REAL 2 by A61,TARSKI:def 3;
p in LSeg(p01,p1) & p in LSeg(p2,p11) & p01`1 <= p1`1 & p2`1 <= p11
`1
by A5,A6,A53,A54,A61,EUCLID:56,XBOOLE_0:def 3;
then p`1 <= p1`1 & p2`1 <= p`1 by TOPREAL1:9;
hence contradiction by A5,A53,A59,AXIOMS:22;
end;
A62: LSeg(p1,p01) /\ L4 c= {p11} by A7,TOPREAL1:24,XBOOLE_1:26;
now assume p11 in LSeg(p1,p01) /\ L4;
then p11 in LSeg(p01,p1) & p01`1 <=
p1`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p11`1 <= p1`1 by TOPREAL1:9;
hence contradiction by A5,A6,A54,A59,Lm4,AXIOMS:21;
end;
then {p11} <> LSeg(p1,p01) /\ L4 by ZFMISC_1:37;
then A63: LSeg(p1,p01) /\ L4 = {} by A62,ZFMISC_1:39;
LSeg(p1,p01) /\ L3 c= L2 /\ L3 & L3 /\ L2 = {}
by A7,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A64: LSeg(p1,p01) /\ L3 = {} by XBOOLE_1:3;
A65: LSeg(p1,p01) /\ L1 c= L2 /\ L1 by A7,XBOOLE_1:26;
p01 in LSeg(p1,p01) by TOPREAL1:6;
then A66: LSeg(p1,p01) /\ L1 <> {} by Lm15,XBOOLE_0:def 3;
A67: LSeg(p1,p01) /\ (L1 \/ L3 \/ L4 \/ LSeg(p11,p2))
= LSeg(p1,p01) /\ (L1 \/ L3 \/ L4) \/ (LSeg(p1,p01) /\ LSeg(p11,p2))
by XBOOLE_1:23
.= LSeg(p1,p01) /\ (L1 \/ L3) \/ (LSeg(p1,p01) /\ L4) by A60,XBOOLE_1:
23
.= LSeg(p1,p01) /\ L1 \/ (LSeg(p1,p01) /\ L3) by A63,XBOOLE_1:23
.= {p01} by A64,A65,A66,TOPREAL1:21,ZFMISC_1:39;
L1 is_an_arc_of p01,p00 by Lm4,TOPREAL1:15;
then A68: L1 \/ L3 is_an_arc_of p01,p10 by TOPREAL1:16,23;
(L1 \/ L3) /\ L4 = L1 /\ L4 \/ L3 /\ L4 by XBOOLE_1:23
.= {p10} by Lm3,TOPREAL1:22;
then A69: L1 \/ L3 \/ L4 is_an_arc_of p01,p11 by A68,TOPREAL1:16;
A70: L4 /\ LSeg(p11,p2) c= L4 /\ L2 by A56,XBOOLE_1:26;
p11 in LSeg(p11,p2) by TOPREAL1:6;
then L4 /\ LSeg(p11,p2) <> {} by Lm20,XBOOLE_0:def 3;
then A71: L4 /\ LSeg(p11,p2) = {p11} by A70,TOPREAL1:24,ZFMISC_1:39;
A72: L1 /\ LSeg(p11,p2) c= {p01} by A56,TOPREAL1:21,XBOOLE_1:26;
now assume p01 in L1 /\ LSeg(p11,p2);
then p01 in
LSeg(p2,p11) & p2`1 <= p11`1 by A53,A54,EUCLID:56,XBOOLE_0:def 3;
hence contradiction by A6,A53,A59,Lm4,TOPREAL1:9;
end;
then {p01} <> L1 /\ LSeg(p11,p2) by ZFMISC_1:37;
then A73: L1 /\ LSeg(p11,p2) = {} by A72,ZFMISC_1:39;
L3 /\ LSeg(p11,p2) c= L3 /\ L2 & L3 /\ L2 = {}
by A56,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A74: L3 /\ LSeg(p11,p2) = {} by XBOOLE_1:3;
(L1 \/ L3 \/ L4) /\ LSeg(p11,p2)
= (L1 \/ L3) /\ LSeg(p11,p2) \/ L4 /\ LSeg(p11,p2) by XBOOLE_1:23
.= (L1 /\ LSeg(p11,p2)) \/ (L3 /\ LSeg(p11,p2)) \/
{p11} by A71,XBOOLE_1:23
.= {p11} by A73,A74;
then L1 \/ L3 \/ L4 \/
LSeg(p11,p2) is_an_arc_of p01,p2 by A69,TOPREAL1:16;
hence P2 is_an_arc_of p1,p2 by A67,TOPREAL1:17;
thus P1 \/ P2
= LSeg(p01,p1) \/ LSeg(p1,p2) \/ (L1 \/ L3 \/ L4 \/
LSeg(p11,p2)) by XBOOLE_1:4
.= LSeg(p01,p1) \/ LSeg(p1,p2) \/ LSeg(p2,p11) \/ (L1 \/ L3 \/
L4) by XBOOLE_1:4
.= L2 \/ (L1 \/ L3 \/ L4) by A3,A52,TOPREAL1:13
.= L2 \/ (L1 \/ (L3 \/ L4)) by XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:20,XBOOLE_1:4;
p1 in LSeg(p1,p2) & p1 in LSeg(p1,p01) by TOPREAL1:6;
then p1 in LSeg(p1,p2) /\ LSeg(p1,p01) by XBOOLE_0:def 3;
then A75: {p1} c= LSeg(p1,p2) /\ LSeg(p1,p01) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p1,p01) c= {p1}
proof
let a; assume A76: a in LSeg(p1,p2) /\ LSeg(p1,p01);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p1,p2) & p in LSeg(p01,p1) & p1`2 <= p2`2 & p1`1 <= p2`1
& p01`1 <= p1`1 by A5,A6,A53,A54,A59,A76,EUCLID:56,XBOOLE_0:def 3;
then p1`2 <= p`2 & p`2 <= p2`2 & p1`1 <= p`1 & p`1 <= p1`1
by TOPREAL1:9,10;
then p1`1 = p`1 & p`2 = 1 by A5,A6,A53,A54,AXIOMS:21;
then p = |[p1`1, 1]| by EUCLID:57 .= p1 by A5,A6,EUCLID:57;
hence a in {p1} by TARSKI:def 1;
end;
then A77: LSeg(p1,p2) /\ LSeg(p1,p01) = {p1} by A75,XBOOLE_0:def 10;
p2 in LSeg(p1,p2) & p2 in LSeg(p11,p2) by TOPREAL1:6;
then p2 in LSeg(p1,p2) /\ LSeg(p11,p2) by XBOOLE_0:def 3;
then A78: {p2} c= LSeg(p1,p2) /\ LSeg(p11,p2) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p11,p2) c= {p2}
proof
let a; assume A79: a in LSeg(p1,p2) /\ LSeg(p11,p2);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p1,p2) & p in LSeg(p2,p11) & p1`2 <= p2`2 & p1`1 <= p2`1
& p2`1 <= p11`1 by A5,A6,A53,A54,A59,A79,EUCLID:56,XBOOLE_0:def 3;
then p1`2 <= p`2 & p`2 <= p2`2 & p2`1 <= p`1 & p`1 <= p2`1
by TOPREAL1:9,10;
then p2`1 = p`1 & p`2 = 1 by A5,A6,A53,A54,AXIOMS:21;
then p = |[ p2`1, 1]| by EUCLID:57 .= p2 by A53,A54,EUCLID:57;
hence a in {p2} by TARSKI:def 1;
end;
then A80: LSeg(p1,p2) /\ LSeg(p11,p2) = {p2} by A78,XBOOLE_0:def 10;
LSeg(p1,p2) /\ L3 c= L2 /\ L3 & L3 /\ L2 = {}
by A58,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A81: LSeg(p1,p2) /\ L3 = {} by XBOOLE_1:3;
A82: P1 /\ P2
= (LSeg(p1,p2) /\ LSeg(p1,p01))
\/ (LSeg(p1,p2) /\ (L1 \/ L3 \/ L4 \/ LSeg(p11,p2))) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ (L1 \/ L3 \/ L4)) \/
{p2}) by A77,A80,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ (L1 \/ L3)) \/ (LSeg(p1,p2) /\ L4) \/ {p2})
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ L1) \/ (LSeg(p1,p2) /\ L3)
\/ (LSeg(p1,p2) /\ L4) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ L1) \/ ((LSeg(p1,p2) /\ L4) \/ {p2}))
by A81,XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p2) /\ L1) \/ ((LSeg(p1,p2) /\ L4) \/ {p2})
by XBOOLE_1:4;
A83: LSeg(p1,p2) /\ L1 c= L2 /\ L1 by A58,XBOOLE_1:26;
A84: now per cases;
suppose A85: p1 = p01;
p1 in LSeg(p1,p2) by TOPREAL1:6;
then LSeg(p1,p2) /\ L1 <> {} by A85,Lm15,XBOOLE_0:def 3;
then LSeg(p1,p2) /\ L1 = {p1} by A83,A85,TOPREAL1:21,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ((LSeg(p1,p2) /\ L4) \/ {p2}) by A82;
suppose A86: p1 <> p01;
now assume p01 in LSeg(p1,p2) /\ L1;
then p01 in LSeg(p1,p2) & p1`1 <= p2`1
by A5,A53,A59,XBOOLE_0:def 3;
then p1`1 = 0 by A5,A6,Lm4,TOPREAL1:9;
hence contradiction by A5,A6,A86,EUCLID:57;
end;
then {p01} <> LSeg(p1,p2) /\ L1 by ZFMISC_1:37;
then LSeg(p1,p2) /\ L1 = {} by A83,TOPREAL1:21,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ((LSeg(p1,p2) /\ L4) \/ {p2}) by A82;
end;
A87: LSeg(p1,p2) /\ L4 c= {p11} by A58,TOPREAL1:24,XBOOLE_1:26;
now per cases;
suppose A88: p2 = p11;
p2 in LSeg(p1,p2) by TOPREAL1:6;
then LSeg(p1,p2) /\ L4 <> {} by A88,Lm20,XBOOLE_0:def 3;
then LSeg(p1,p2) /\ L4 = {p2} by A87,A88,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A84,ENUMSET1:41;
suppose A89: p2 <> p11;
now assume p11 in LSeg(p1,p2) /\ L4;
then p11 in LSeg(p1,p2) & p1`1 <= p2`1
by A5,A53,A59,XBOOLE_0:def 3;
then p11`1 <= p2`1 by TOPREAL1:9;
then p2`1 = 1 by A53,A54,Lm4,AXIOMS:21;
hence contradiction by A53,A54,A89,EUCLID:57;
end;
then {p11} <> LSeg(p1,p2) /\ L4 by ZFMISC_1:37;
then LSeg(p1,p2) /\ L4 = {} by A87,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A84,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
suppose A90: q`1 < q1`1;
take P1 = LSeg(p1,p2),P2 = LSeg(p1,p11) \/ (L4 \/ L3 \/ L1 \/
LSeg(p01,p2));
thus P1 is_an_arc_of p1,p2 by A1,TOPREAL1:15;
A91: now assume
A92: LSeg(p1,p11) /\ LSeg(p01,p2) <> {};
consider a being Element of LSeg(p1,p11) /\ LSeg(p01,p2);
reconsider p = a as Point of TOP-REAL 2 by A92,TARSKI:def 3;
p in LSeg(p1,p11) & p in LSeg(p01,p2) & p1`1 <= p11`1 & p01`1 <= p2
`1
by A5,A6,A53,A54,A92,EUCLID:56,XBOOLE_0:def 3;
then p1`1 <= p`1 & p`1 <= p2`1 by TOPREAL1:9;
hence contradiction by A5,A53,A90,AXIOMS:22;
end;
A93: LSeg(p1,p11) /\ L1 c= L2 /\ L1 by A8,XBOOLE_1:26;
now assume p01 in LSeg(p1,p11) /\ L1;
then p01 in LSeg(p1,p11) & p1`1 <=
p11`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
hence contradiction by A5,A54,A90,Lm4,TOPREAL1:9;
end;
then {p01} <> LSeg(p1,p11) /\ L1 by ZFMISC_1:37;
then A94: LSeg(p1,p11) /\ L1 = {} by A93,TOPREAL1:21,ZFMISC_1:39;
LSeg(p1,p11) /\ L3 c= L2 /\ L3 & L3 /\ L2 = {}
by A8,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A95: LSeg(p1,p11) /\ L3 = {} by XBOOLE_1:3;
A96: LSeg(p1,p11) /\ L4 c= {p11} by A8,TOPREAL1:24,XBOOLE_1:26;
p11 in LSeg(p1,p11) by TOPREAL1:6;
then A97: LSeg(p1,p11) /\ L4 <> {} by Lm20,XBOOLE_0:def 3;
A98: LSeg(p1,p11) /\ (L4 \/ L3 \/ L1 \/ LSeg(p01,p2))
= LSeg(p1,p11) /\ (L4 \/ L3 \/ L1) \/ (LSeg(p1,p11) /\ LSeg(p01,p2))
by XBOOLE_1:23
.= LSeg(p1,p11) /\ (L4 \/ L3) \/ (LSeg(p1,p11) /\ L1) by A91,XBOOLE_1:
23
.= LSeg(p1,p11) /\ L4 \/ (LSeg(p1,p11) /\ L3) by A94,XBOOLE_1:23
.= {p11} by A95,A96,A97,ZFMISC_1:39;
L4 is_an_arc_of p11,p10 by Lm4,TOPREAL1:15;
then A99: L4 \/ L3 is_an_arc_of p11,p00 by TOPREAL1:16,22;
(L4 \/ L3) /\ L1 = L1 /\ L4 \/ L3 /\ L1 by XBOOLE_1:23
.= {p00} by Lm3,TOPREAL1:23;
then A100: L4 \/ L3 \/ L1 is_an_arc_of p11,p01 by A99,TOPREAL1:16;
A101: L1 /\ LSeg(p01,p2) c= {p01} by A57,TOPREAL1:21,XBOOLE_1:26;
p01 in LSeg(p01,p2) by TOPREAL1:6;
then L1 /\ LSeg(p01,p2) <> {} by Lm15,XBOOLE_0:def 3;
then A102: L1 /\ LSeg(p01,p2) = {p01} by A101,ZFMISC_1:39;
A103:
L4 /\ LSeg(p01,p2) c= L4 /\ L2 by A57,XBOOLE_1:26;
now assume p11 in L4 /\ LSeg(p01,p2);
then p11 in
LSeg(p01,p2) & p01`1 <= p2`1 by A53,A54,EUCLID:56,XBOOLE_0:def 3;
then p11`1 <= p2`1 by TOPREAL1:9;
hence contradiction by A6,A53,A54,A90,Lm4,AXIOMS:21;
end;
then {p11} <> L4 /\ LSeg(p01,p2) by ZFMISC_1:37;
then A104: L4 /\ LSeg(p01,p2) = {} by A103,TOPREAL1:24,ZFMISC_1:39;
L3 /\ LSeg(p01,p2) c= L3 /\ L2 & L3 /\ L2 = {}
by A57,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A105: L3 /\ LSeg(p01,p2) = {} by XBOOLE_1:3;
(L4 \/ L3 \/ L1) /\ LSeg(p01,p2)
= (L4 \/ L3) /\ LSeg(p01,p2) \/ L1 /\ LSeg(p01,p2) by XBOOLE_1:23
.= (L4 /\ LSeg(p01,p2)) \/ (L3 /\ LSeg(p01,p2)) \/
{p01} by A102,XBOOLE_1:23
.= {p01} by A104,A105;
then L4 \/ L3 \/ L1 \/
LSeg(p01,p2) is_an_arc_of p11,p2 by A100,TOPREAL1:16
;
hence P2 is_an_arc_of p1,p2 by A98,TOPREAL1:17;
thus P1 \/ P2
= LSeg(p2,p1) \/ LSeg(p1,p11) \/ (L4 \/ L3 \/ L1 \/
LSeg(p01,p2)) by XBOOLE_1:4
.= LSeg(p01,p2) \/ (LSeg(p2,p1) \/ LSeg(p1,p11)) \/ (L4 \/ L3 \/ L1)
by XBOOLE_1:4
.= L2 \/ (L4 \/ L3 \/ L1) by A3,A52,TOPREAL1:13
.= R^2-unit_square by TOPREAL1:20,XBOOLE_1:4;
p1 in LSeg(p1,p2) & p1 in LSeg(p1,p11) by TOPREAL1:6;
then p1 in LSeg(p1,p2) /\ LSeg(p1,p11) by XBOOLE_0:def 3;
then A106: {p1} c= LSeg(p1,p2) /\ LSeg(p1,p11) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p1,p11) c= {p1}
proof
let a; assume A107: a in LSeg(p1,p2) /\ LSeg(p1,p11);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p2,p1) & p in LSeg(p1,p11) & p2`2 <= p1`2 & p2`1 <= p1`1
& p1`1 <= p11`1 by A5,A6,A53,A54,A90,A107,EUCLID:56,XBOOLE_0:def 3;
then p2`2 <= p`2 & p`2 <= p1`2 & p1`1 <= p`1 & p`1 <= p1`1
by TOPREAL1:9,10;
then p1`1 = p`1 & p`2 = 1 by A5,A6,A53,A54,AXIOMS:21;
then p = |[p1`1, 1]| by EUCLID:57 .= p1 by A5,A6,EUCLID:57;
hence a in {p1} by TARSKI:def 1;
end;
then A108: LSeg(p1,p2) /\ LSeg(p1,p11) = {p1} by A106,XBOOLE_0:def 10;
p2 in LSeg(p1,p2) & p2 in LSeg(p01,p2) by TOPREAL1:6;
then p2 in LSeg(p1,p2) /\ LSeg(p01,p2) by XBOOLE_0:def 3;
then A109: {p2} c= LSeg(p1,p2) /\ LSeg(p01,p2) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p01,p2) c= {p2}
proof
let a; assume A110: a in LSeg(p1,p2) /\ LSeg(p01,p2);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p2,p1) & p in LSeg(p01,p2) & p2`1 <= p1`1 & p2`2 <= p1`2
& p01`1 <= p2`1 by A5,A6,A53,A54,A90,A110,EUCLID:56,XBOOLE_0:def 3;
then p2`2 <= p`2 & p`2 <= p1`2 & p2`1 <= p`1 & p`1 <= p2`1
by TOPREAL1:9,10;
then p2`1 = p`1 & p`2 = 1 by A5,A6,A53,A54,AXIOMS:21;
then p = |[ p2`1, 1]| by EUCLID:57 .= p2 by A53,A54,EUCLID:57;
hence a in {p2} by TARSKI:def 1;
end;
then A111: LSeg(p1,p2) /\ LSeg(p01,p2) = {p2} by A109,XBOOLE_0:def 10;
LSeg(p1,p2) /\ L3 c= L2 /\ L3 & L3 /\ L2 = {}
by A58,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A112: LSeg(p1,p2) /\ L3 = {} by XBOOLE_1:3;
A113: P1 /\ P2
= {p1} \/ LSeg(p1,p2) /\ (L4 \/ L3 \/ L1 \/
LSeg(p01,p2)) by A108,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ (L4 \/ L3 \/ L1)) \/ {p2}) by A111,XBOOLE_1
:23
.= {p1} \/ ((LSeg(p1,p2) /\ (L4 \/ L3)) \/ (LSeg(p1,p2) /\ L1) \/ {p2})
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ L4) \/ (LSeg(p1,p2) /\ L3)
\/ (LSeg(p1,p2) /\ L1) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ L4) \/ ((LSeg(p1,p2) /\ L1) \/ {p2}))
by A112,XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p2) /\ L4) \/ ((LSeg(p1,p2) /\ L1) \/
{p2}) by XBOOLE_1:4;
A114: LSeg(p1,p2) /\ L1 c= L2 /\ L1 by A58,XBOOLE_1:26;
A115: now per cases;
suppose A116: p2 = p01;
p2 in LSeg(p1,p2) by TOPREAL1:6;
then LSeg(p1,p2) /\ L1 <> {} by A116,Lm15,XBOOLE_0:def 3;
then LSeg(p1,p2) /\ L1 = {p2} by A114,A116,TOPREAL1:21,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (LSeg(p1,p2) /\ L4) \/ {p2} by A113;
suppose A117: p2 <> p01;
now assume p01 in LSeg(p1,p2) /\ L1;
then p01 in LSeg(p2,p1) & p2`1 <= p1`1
by A5,A53,A90,XBOOLE_0:def 3;
then p2`1 = 0 by A53,A54,Lm4,TOPREAL1:9;
hence contradiction by A53,A54,A117,EUCLID:57;
end;
then {p01} <> LSeg(p1,p2) /\ L1 by ZFMISC_1:37;
then LSeg(p1,p2) /\ L1 = {} by A114,TOPREAL1:21,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (LSeg(p1,p2) /\ L4) \/ {p2} by A113;
end;
A118: LSeg(p1,p2) /\ L4 c= {p11} by A58,TOPREAL1:24,XBOOLE_1:26;
now per cases;
suppose A119: p1 = p11;
p1 in LSeg(p1,p2) by TOPREAL1:6;
then LSeg(p1,p2) /\ L4 <> {} by A119,Lm20,XBOOLE_0:def 3;
then LSeg(p1,p2) /\ L4 = {p1} by A118,A119,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A115,ENUMSET1:41;
suppose A120: p1 <> p11;
now assume p11 in LSeg(p1,p2) /\ L4;
then p11 in LSeg(p2,p1) & p2`1 <= p1`1
by A5,A53,A90,XBOOLE_0:def 3;
then p11`1 <= p1`1 by TOPREAL1:9;
then p1`1 = 1 by A5,A6,Lm4,AXIOMS:21;
hence contradiction by A5,A6,A120,EUCLID:57;
end;
then {p11} <> LSeg(p1,p2) /\ L4 by ZFMISC_1:37;
then LSeg(p1,p2) /\ L4 = {} by A118,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A115,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
end;
hence ex P1,P2 being non empty Subset of TOP-REAL 2
st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 &
R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2};
suppose A121: p2 in L3;
then A122: ex q2 st q2 = p2 & q2`1 <= 1 & q2`1 >= 0 & q2`2 = 0 by TOPREAL1
:19;
take P1 = LSeg(p1,p11) \/ L4 \/ LSeg(p10,p2),P2
= LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2);
LSeg(p10,p2) c= L3 & p10 in LSeg(p10,p2)
by A121,Lm17,TOPREAL1:6,12;
then LSeg(p11,p10) /\ LSeg(p10,p2) c= L4 /\ L3 &
p10 in LSeg(p11,p10) /\ LSeg(p10,p2) by Lm18,XBOOLE_0:def 3,XBOOLE_1:27;
then LSeg(p11,p10) /\ LSeg(p10,p2) = {p10} by TOPREAL1:22,ZFMISC_1:39;
then A123: L4 \/ LSeg(p10,p2) is_an_arc_of p11,p2 by Lm4,TOPREAL1:18;
A124: LSeg(p2,p10) c= L3 by A121,Lm17,TOPREAL1:12;
then LSeg(p1,p11) /\ LSeg(p10,p2) c= L2 /\ L3 by A8,XBOOLE_1:27;
then A125: LSeg(p1,p11) /\ LSeg(p10,p2) = {} by Lm2,XBOOLE_1:3;
LSeg(p1,p11) /\ (L4 \/ LSeg(p10,p2))
= (LSeg(p1,p11) /\ L4) \/ (LSeg(p1,p11) /\ LSeg(p10,p2)) by XBOOLE_1:23
.= {p11} by A13,A14,A125,ZFMISC_1:39;
then LSeg(p1,p11) \/ (L4 \/ LSeg(p10,p2)) is_an_arc_of p1,p2
by A123,TOPREAL1:17;
hence P1 is_an_arc_of p1,p2 by XBOOLE_1:4;
LSeg(p00,p2) c= L3 & p00 in LSeg(p00,p2)
by A121,Lm14,TOPREAL1:6,12;
then LSeg(p01,p00) /\ LSeg(p00,p2) c= {p00} & LSeg(p01,p00) /\
LSeg(p00,p2) <> {}
by Lm13,TOPREAL1:23,XBOOLE_0:def 3,XBOOLE_1:27;
then LSeg(p01,p00) /\ LSeg(p00,p2) = {p00} by ZFMISC_1:39;
then A126: L1 \/ LSeg(p00,p2) is_an_arc_of p01,p2 by Lm4,TOPREAL1:18;
A127: LSeg(p2,p00) c= L3 by A121,Lm14,TOPREAL1:12;
then LSeg(p1,p01) /\ LSeg(p00,p2) c= L2 /\ L3 by A7,XBOOLE_1:27;
then A128: LSeg(p1,p01) /\ LSeg(p00,p2) = {} by Lm2,XBOOLE_1:3;
LSeg(p1,p01) /\ (L1 \/ LSeg(p00,p2))
= (LSeg(p01,p1) /\ L1) \/ (LSeg(p1,p01) /\ LSeg(p00,p2)) by XBOOLE_1:23
.= {p01} by A10,A11,A128,TOPREAL1:21,ZFMISC_1:39;
then LSeg(p1,p01) \/ (L1 \/ LSeg(p00,p2)) is_an_arc_of p1,p2
by A126,TOPREAL1:17;
hence P2 is_an_arc_of p1,p2 by XBOOLE_1:4;
A129: LSeg(p10,p2) \/ LSeg(p00,p2) = L3 by A121,TOPREAL1:11;
A130: LSeg(p1,p11) \/ LSeg(p1,p01) = L2 by A3,TOPREAL1:11;
thus R^2-unit_square = L2 \/ (L4 \/ (LSeg(p10,p2) \/ LSeg(p00,p2)) \/
L1) by A129,TOPREAL1:20,XBOOLE_1:4
.= L2 \/ (L4 \/ LSeg(p10,p2) \/ LSeg(p00,p2) \/ L1) by XBOOLE_1:4
.= L2 \/ (L4 \/ LSeg(p10,p2) \/ (L1 \/ LSeg(p00,p2))) by XBOOLE_1:4
.= LSeg(p1,p11) \/ ((L4 \/ LSeg(p10,p2) \/ (L1 \/ LSeg(p00,p2)))
\/ LSeg(p1,p01)) by A130,XBOOLE_1:4
.= LSeg(p1,p11) \/ (L4 \/ LSeg(p10,p2) \/ (L1 \/ LSeg(p00,p2)
\/ LSeg(p1,p01))) by XBOOLE_1:4
.= LSeg(p1,p11) \/ (L4 \/ LSeg(p10,p2)) \/ (L1 \/ LSeg(p00,p2)
\/ LSeg(p1,p01)) by XBOOLE_1:4
.= LSeg(p1,p11) \/ L4 \/ LSeg(p10,p2)
\/ (LSeg(p1,p01) \/ (L1 \/ LSeg(p00,p2))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4;
LSeg(p1,p11) /\ LSeg(p00,p2) c= L2 /\ LSeg(p00,p2) &
L2 /\ LSeg(p00,p2) c= L2 /\ L3 by A8,A127,XBOOLE_1:26;
then LSeg(p1,p11) /\ LSeg(p00,p2) c= L3 /\ L2 by XBOOLE_1:1;
then A131: LSeg(p1,p11) /\ LSeg(p00,p2) = {} by Lm2,XBOOLE_1:3;
A132: LSeg(p1,p11) /\ LSeg(p1,p01) = {p1} by A3,TOPREAL1:14;
A133: LSeg(p10,p2) /\ LSeg(p00,p2) = {p2} by A121,TOPREAL1:14;
LSeg(p10,p2) /\ LSeg(p1,p01) c= L3 /\ L2 by A7,A124,XBOOLE_1:27;
then A134: LSeg(p10,p2) /\ LSeg(p1,p01) = {} by Lm2,XBOOLE_1:3;
A135: P1 /\ P2
= (LSeg(p1,p11) \/ L4) /\ (LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2))) by XBOOLE_1:
23
.= (LSeg(p1,p11) /\ (LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2)))
\/ (L4 /\ (LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2))) by XBOOLE_1:
23
.= (LSeg(p1,p11) /\ (LSeg(p1,p01) \/ L1))
\/ (LSeg(p1,p11) /\ LSeg(p00,p2))
\/ (L4 /\ (LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2))) by XBOOLE_1:
23
.= (LSeg(p1,p11) /\ LSeg(p1,p01)) \/ (LSeg(p1,p11) /\ L1)
\/ (L4 /\ (LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L1 \/
LSeg(p00,p2))) by A131,XBOOLE_1:23
.= {p1} \/ (LSeg(p1,p11) /\ L1)
\/ ((L4 /\ (LSeg(p1,p01) \/ L1)) \/ (L4 /\ LSeg(p00,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L1 \/
LSeg(p00,p2))) by A132,XBOOLE_1:23
.= {p1} \/ (LSeg(p1,p11) /\ L1)
\/ ((L4 /\ LSeg(p1,p01)) \/ (L1 /\ L4) \/ (L4 /\ LSeg(p00,p2)))
\/ (LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L1 \/ LSeg(p00,p2))) by XBOOLE_1:
23
.= {p1} \/ (LSeg(p1,p11) /\ L1)
\/ ((L4 /\ LSeg(p1,p01)) \/ (L4 /\ LSeg(p00,p2)))
\/ ((LSeg(p10,p2) /\ (LSeg(p1,p01) \/ L1)) \/ {p2}) by A133,Lm3,
XBOOLE_1:23
.= {p1} \/ (LSeg(p1,p11) /\ L1)
\/ ((L4 /\ LSeg(p1,p01)) \/ (L4 /\ LSeg(p00,p2)))
\/ ((LSeg(p10,p2) /\ LSeg(p1,p01)) \/ (LSeg(p10,p2) /\ L1) \/ {p2})
by XBOOLE_1:23
.= {p1} \/ (LSeg(p1,p11) /\ L1)
\/ ((L4 /\ LSeg(p1,p01)) \/ (L4 /\ LSeg(p00,p2)))
\/ ((LSeg(p10,p2) /\ L1) \/ {p2}) by A134;
A136: now per cases;
suppose A137: p1 = p01;
then L4 /\ LSeg(p1,p01) = L4 /\ {p01} by TOPREAL1:7
.= {} by Lm1,Lm8;
hence P1 /\ P2 =
{p1} \/ (L4 /\ LSeg(p00,p2)) \/ ((LSeg(p10,p2) /\ L1) \/ {p2})
by A135,A137,TOPREAL1:21;
suppose A138: p1 = p11;
then LSeg(p1,p11) /\ L1 = {p11} /\ L1 by TOPREAL1:7
.= {} by Lm1,Lm11;
hence P1 /\ P2
= {p1} \/ {p1} \/ (L4 /\ LSeg(p00,p2))
\/ ((LSeg(p10,p2) /\ L1) \/ {p2}) by A135,A138,TOPREAL1:24,XBOOLE_1:
4
.= {p1} \/ (L4 /\ LSeg(p00,p2)) \/ ((LSeg(p10,p2) /\ L1) \/ {p2});
suppose A139: p1 <> p11 & p1 <> p01;
A140: LSeg(p1,p11) /\ L1 c= L2 /\ L1 by A8,XBOOLE_1:26;
now assume p01 in LSeg(p1,p11) /\ L1;
then p01 in LSeg(p1,p11) & p1`1 <=
p11`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p1`1 = 0 by A5,A6,Lm4,TOPREAL1:9;
hence contradiction by A5,A6,A139,EUCLID:57;
end;
then {p01} <> LSeg(p1,p11) /\ L1 by ZFMISC_1:37;
then A141: LSeg(p1,p11) /\ L1 = {} by A140,TOPREAL1:21,ZFMISC_1:39;
A142: L4 /\ LSeg(p1,p01) c= L4 /\ L2 by A7,XBOOLE_1:26;
now assume p11 in L4 /\ LSeg(p1,p01);
then p11 in LSeg(p01,p1) & p01`1 <=
p1`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then 1 <= p1`1 by Lm4,TOPREAL1:9;
then p1`1 = 1 by A5,A6,AXIOMS:21;
hence contradiction by A5,A6,A139,EUCLID:57;
end;
then {p11} <> L4 /\ LSeg(p1,p01) by ZFMISC_1:37;
then L4 /\ LSeg(p1,p01) = {} by A142,TOPREAL1:24,ZFMISC_1:39;
hence P1 /\ P2 =
{p1} \/ (L4 /\ LSeg(p00,p2)) \/ ((LSeg(p10,p2) /\ L1) \/ {p2})
by A135,A141;
end;
now per cases;
suppose A143: p2 = p00;
then L4 /\ LSeg(p00,p2) = L4 /\ {p00} by TOPREAL1:7
.= {} by Lm1,Lm5;
hence P1 /\ P2 = {p1,p2} by A136,A143,ENUMSET1:41,TOPREAL1:23;
suppose A144: p2 = p10;
then LSeg(p10,p2) /\ L1 = {p10} /\ L1 by TOPREAL1:7
.= {} by Lm1,Lm9;
hence P1 /\ P2 = {p1} \/ ({p2} \/
{p2}) by A136,A144,TOPREAL1:22,XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41;
suppose A145: p2 <> p10 & p2 <> p00;
A146: L4 /\ LSeg(p00,p2) c= L4 /\ L3 by A127,XBOOLE_1:26;
now assume p10 in L4 /\ LSeg(p00,p2);
then p10 in LSeg(p00,p2) & p00`1 <=
p2`1 by A122,EUCLID:56,XBOOLE_0:def 3;
then 1 <= p2`1 by Lm4,TOPREAL1:9;
then p2`1 = 1 by A122,AXIOMS:21;
hence contradiction by A122,A145,EUCLID:57;
end;
then {p10} <> L4 /\ LSeg(p00,p2) by ZFMISC_1:37;
then A147: L4 /\ LSeg(p00,p2) = {} by A146,TOPREAL1:22,ZFMISC_1:39;
A148: LSeg(p10,p2) /\ L1 c= L3 /\ L1 by A124,XBOOLE_1:26;
now assume p00 in LSeg(p10,p2) /\ L1;
then p00 in LSeg(p2,p10) & p2`1 <=
p10`1 by A122,EUCLID:56,XBOOLE_0:def 3;
then p2`1 = 0 by A122,Lm4,TOPREAL1:9;
hence contradiction by A122,A145,EUCLID:57;
end;
then {p00} <> LSeg(p10,p2) /\ L1 by ZFMISC_1:37;
then LSeg(p10,p2) /\ L1 = {} by A148,TOPREAL1:23,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A136,A147,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
suppose A149: p2 in L4;
then A150: ex q st q = p2 & q`1 = 1 & q`2 <= 1 & q`2 >= 0 by TOPREAL1:19;
take P1 = LSeg(p1,p11) \/ LSeg(p11,p2),P2
= LSeg(p1,p01) \/ (L1 \/ L3 \/ LSeg(p10,p2));
p11 in LSeg(p1,p11) & p11 in LSeg(p11,p2) by TOPREAL1:6;
then LSeg(p1,p11) c= L2 & LSeg(p11,p2) c= L4 &
p11 in LSeg(p1,p11) /\ LSeg(p11,p2) by A3,A149,Lm19,Lm20,TOPREAL1:12,
XBOOLE_0:def 3;
then LSeg(p1,p11) /\ LSeg(p11,p2) c= L2 /\ L4 & L2 /\ L4 = {p11}
& LSeg(p1,p11) /\ LSeg(p11,p2) <> {} by TOPREAL1:24,XBOOLE_1:27;
then LSeg(p1,p11) /\ LSeg(p11,p2) = {p11} & (p1 <> p11 or p11 <> p2)
by A1,ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by TOPREAL1:18;
L1 is_an_arc_of p01,p00 & L3 is_an_arc_of p00,p10
by Lm4,TOPREAL1:15;
then A151: L1 \/ L3 is_an_arc_of p01,p10 by TOPREAL1:5,23;
A152: LSeg(p10,p2) c= L4 by A149,Lm18,TOPREAL1:12;
then L1 /\ LSeg(p10,p2) c= L1 /\ L4 by XBOOLE_1:26;
then A153: L1 /\ LSeg(p10,p2) = {} by Lm3,XBOOLE_1:3;
p10 in LSeg(p10,p2) by TOPREAL1:6;
then A154: L3 /\ LSeg(p10,p2) c= {p10} & L3 /\ LSeg(p10,p2) <> {}
by A152,Lm17,TOPREAL1:22,XBOOLE_0:def 3,XBOOLE_1:27;
(L1 \/ L3) /\ LSeg(p10,p2)
= (L1 /\ LSeg(p10,p2)) \/ (L3 /\ LSeg(p10,p2)) by XBOOLE_1:23
.= {p10} by A153,A154,ZFMISC_1:39;
then A155: L1 \/ L3 \/ LSeg(p10,p2) is_an_arc_of p01,p2 by A151,TOPREAL1:16;
A156: LSeg(p1,p01) /\
LSeg(p10,p2) c= {p11} by A7,A152,TOPREAL1:24,XBOOLE_1:27;
now assume p11 in LSeg(p1,p01) /\ LSeg(p10,p2);
then p11 in LSeg(p01,p1) & p11 in LSeg(p10,p2) & p01`1 <= p1`1 &
p10`2 <= p2`2 by A5,A6,A150,EUCLID:56,XBOOLE_0:def 3;
then p11`1 <= p1`1 & p11`2 <= p2`2 by TOPREAL1:9,10;
then A157: p11`2 = p1`2 & p11`2 = p2`2 & p11`1 = p1`1 & p11`1 = p2`1
by A5,A6,A150,Lm4,AXIOMS:21;
then p1 = |[p11`1,p11`2]| by EUCLID:57 .= p2 by A157,EUCLID:57;
hence contradiction by A1;
end;
then {p11} <> LSeg(p1,p01) /\ LSeg(p10,p2) by ZFMISC_1:37;
then A158: LSeg(p1,p01) /\ LSeg(p10,p2) = {} by A156,ZFMISC_1:39;
LSeg(p1,p01) /\ (L1 \/ L3 \/ LSeg(p10,p2))
= (LSeg(p1,p01) /\ (L1 \/ L3)) \/ (LSeg(p1,p01) /\
LSeg(p10,p2)) by XBOOLE_1:23
.= (LSeg(p1,p01) /\ L1) \/ (LSeg(p1,p01) /\ L3) by A158,XBOOLE_1:23
.= {p01} by A9,A10,A11,TOPREAL1:21,ZFMISC_1:39;
hence P2 is_an_arc_of p1,p2 by A155,TOPREAL1:17;
A159: L2 = LSeg(p1,p11) \/ LSeg(p1,p01) by A3,TOPREAL1:11;
A160: L4 = LSeg(p10,p2) \/ LSeg(p11,p2) by A149,TOPREAL1:11;
thus P1 \/ P2
= LSeg(p11,p2) \/ (LSeg(p1,p11) \/ (LSeg(p1,p01) \/
(L1 \/ L3 \/ LSeg(p10,p2)))) by XBOOLE_1:4
.= L2 \/ (L1 \/ L3 \/ LSeg(p10,p2)) \/ LSeg(p11,p2) by A159,XBOOLE_1:4
.= L2 \/ ((L1 \/ L3 \/ LSeg(p10,p2)) \/ LSeg(p11,p2)) by XBOOLE_1:4
.= L2 \/ (L1 \/ L3 \/ (LSeg(p10,p2) \/ LSeg(p11,p2))) by XBOOLE_1:4
.= L2 \/ (L1 \/ (L3 \/ L4)) by A160,XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:20,XBOOLE_1:4;
A161: LSeg(p2,p11) c= L4 by A149,Lm20,TOPREAL1:12;
A162: {p1} = LSeg(p1,p11) /\ LSeg(p1,p01) by A3,TOPREAL1:14;
A163: LSeg(p11,p2) /\ LSeg(p10,p2)
= {p2} by A149,TOPREAL1:14;
LSeg(p11,p2) /\ L1 c= L4 /\ L1 by A161,XBOOLE_1:27;
then A164: LSeg(p11,p2) /\ L1 = {} by Lm3,XBOOLE_1:3;
A165: P1 /\ P2 = (LSeg(p1,p11) /\ (LSeg(p1,p01) \/ (L1 \/ L3 \/
LSeg(p10,p2))))
\/ (LSeg(p11,p2) /\ (LSeg(p1,p01) \/ (L1 \/ L3 \/ LSeg(p10,p2))))
by XBOOLE_1:23
.= (LSeg(p1,p11) /\ LSeg(p1,p01))
\/ (LSeg(p1,p11) /\ (L1 \/ L3 \/ LSeg(p10,p2)))
\/ (LSeg(p11,p2) /\ (LSeg(p1,p01) \/ (L1 \/ L3 \/ LSeg(p10,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p11) /\ (L1 \/ L3)) \/ (LSeg(p1,p11) /\
LSeg(p10,p2)))
\/ (LSeg(p11,p2) /\ (LSeg(p1,p01) \/ (L1 \/ L3 \/ LSeg(p10,p2))))
by A162,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p11) /\ L1) \/ (LSeg(p1,p11) /\ L3)
\/ (LSeg(p1,p11) /\ LSeg(p10,p2)))
\/ (LSeg(p11,p2) /\ (LSeg(p1,p01) \/ (L1 \/ L3 \/ LSeg(p10,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p11) /\ L1) \/ (LSeg(p1,p11) /\ L3)
\/ (LSeg(p1,p11) /\ LSeg(p10,p2)))
\/ ((LSeg(p11,p2) /\ LSeg(p1,p01))
\/ (LSeg(p11,p2) /\ (L1 \/ L3 \/ LSeg(p10,p2)))) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p11) /\ L1) \/ (LSeg(p1,p11) /\ L3)
\/ (LSeg(p1,p11) /\ LSeg(p10,p2)))
\/ ((LSeg(p11,p2) /\ LSeg(p1,p01))
\/ ((LSeg(p11,p2) /\ (L1 \/ L3)) \/ {p2})) by A163,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p11) /\ L1) \/ (LSeg(p1,p11) /\ L3)
\/ (LSeg(p1,p11) /\ LSeg(p10,p2)))
\/ ((LSeg(p11,p2) /\ LSeg(p1,p01))
\/ ((LSeg(p11,p2) /\ L1) \/ (LSeg(p11,p2) /\ L3) \/ {p2})) by XBOOLE_1:
23
.= {p1} \/ ((LSeg(p1,p11) /\ L1) \/ (LSeg(p1,p11) /\ LSeg(p10,p2)))
\/ ((LSeg(p11,p2) /\ LSeg(p1,p01)) \/ (LSeg(p11,p2) /\ L3 \/ {p2}))
by A12,A164;
A166: now per cases;
suppose A167: p2 = p10;
then A168: not p2 in LSeg(p1,p11) by A8,Lm4,TOPREAL1:10;
LSeg(p1,p11) /\ LSeg(p10,p2) = LSeg(p1,p11) /\ {p2} by A167,TOPREAL1:7
.= {} by A168,Lm1;
hence P1 /\ P2
= {p1} \/ (LSeg(p1,p11) /\ L1) \/ ((LSeg(p11,p2) /\ LSeg(p1,p01))
\/ {p2}) by A165,A167,TOPREAL1:22;
suppose A169: p2 = p11;
then A170: LSeg(p11,p2) /\ L3 = {p11} /\ L3 by TOPREAL1:7
.= {} by Lm1,Lm12;
A171: LSeg(p1,p11) /\ LSeg(p10,p2) c= {p2} by A8,A169,TOPREAL1:24,
XBOOLE_1:27;
p2 in LSeg(p1,p11) by A169,TOPREAL1:6;
then LSeg(p1,p11) /\
LSeg(p10,p2) <> {} by A169,Lm20,XBOOLE_0:def 3;
then LSeg(p1,p11) /\ LSeg(p10,p2) = {p2} by A171,ZFMISC_1:39;
hence P1 /\ P2
= ({p1} \/ (LSeg(p1,p11) /\ L1)) \/ {p2} \/ ((LSeg(p11,p2) /\
LSeg(p1,p01))
\/ {p2}) by A165,A170,XBOOLE_1:4
.= ({p1} \/ (LSeg(p1,p11) /\ L1)) \/ ((LSeg(p11,p2) /\ LSeg(p1,p01))
\/ {p2} \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ (LSeg(p1,p11) /\ L1)) \/ ((LSeg(p11,p2) /\ LSeg(p1,p01))
\/ ({p2} \/ {p2})) by XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p11) /\ L1) \/ ((LSeg(p11,p2) /\ LSeg(p1,p01)) \/
{p2});
suppose A172: p2 <> p11 & p2 <> p10;
A173:
LSeg(p11,p2) /\ L3 c= L4 /\ L3 by A161,XBOOLE_1:27;
now assume p10 in LSeg(p11,p2) /\ L3;
then p10 in LSeg(p2,p11) & p2`2 <= p11`2 by A150,EUCLID:56,XBOOLE_0:def
3;
then p2`1 = 1 & p2`2 = 0 by A150,Lm4,TOPREAL1:10;
hence contradiction by A172,EUCLID:57;
end;
then {p10} <> LSeg(p11,p2) /\ L3 by ZFMISC_1:37;
then A174: LSeg(p11,p2) /\ L3 = {} by A173,TOPREAL1:22,ZFMISC_1:39;
A175: LSeg(p1,p11) /\ LSeg(p10,p2) c= {p11} by A8,A152,TOPREAL1:24,
XBOOLE_1:27;
now assume p11 in LSeg(p1,p11) /\ LSeg(p10,p2);
then p11 in
LSeg(p10,p2) & p10`2 <= p2`2 by A150,EUCLID:56,XBOOLE_0:def 3;
then p11`2 <= p2`2 by TOPREAL1:10;
then p2`1 = 1 & p2`2 = 1 by A150,Lm4,AXIOMS:21;
hence contradiction by A172,EUCLID:57;
end;
then {p11} <> LSeg(p1,p11) /\ LSeg(p10,p2) by ZFMISC_1:37;
then LSeg(p1,p11) /\ LSeg(p10,p2) = {} by A175,ZFMISC_1:39;
hence P1 /\ P2
= {p1} \/ (LSeg(p1,p11) /\ L1) \/ ((LSeg(p11,p2) /\ LSeg(p1,p01)) \/
{p2})
by A165,A174;
end;
now per cases;
suppose A176: p1 = p01;
then A177: LSeg(p11,p2) /\ LSeg(p1,p01) = LSeg(p11,p2) /\ {p1} by
TOPREAL1:7;
p1 in LSeg(p11,p2) implies
contradiction by A161,A176,Lm4,TOPREAL1:9;
then LSeg(p11,p2) /\ LSeg(p1,p01) = {} by A177,Lm1;
hence P1 /\ P2
= {p1,p2} by A166,A176,ENUMSET1:41,TOPREAL1:21;
suppose A178: p1 = p11;
then LSeg(p1,p11) /\ L1 = {p1} /\ L1 by TOPREAL1:7;
then A179: LSeg(p1,p11) /\ L1 = {} by A178,Lm1,Lm11;
A180: LSeg(p11,p2) /\ LSeg(p1,p01) c= L4 /\ L2 by A7,A161,XBOOLE_1:
27;
p11 in LSeg(p11,p2) by TOPREAL1:6;
then LSeg(p11,p2) /\ LSeg(p1,p01) <> {} by A178,Lm19,XBOOLE_0:def
3
;
then LSeg(p11,p2) /\ LSeg(p1,p01) = {p1} by A178,A180,TOPREAL1:24,
ZFMISC_1:39;
hence P1 /\ P2
= {p1} \/ {p1} \/ {p2} by A166,A179,XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41;
suppose A181: p1 <> p11 & p1 <> p01;
A182: LSeg(p1,p11) /\ L1 c= L2 /\ L1 by A8,XBOOLE_1:27;
now assume p01 in LSeg(p1,p11) /\ L1;
then p01 in LSeg(p1,p11) & p1`1 <= p11`1
by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p1`1 = 0 by A5,A6,Lm4,TOPREAL1:9;
hence contradiction by A5,A6,A181,EUCLID:57;
end;
then {p01} <> LSeg(p1,p11) /\ L1 by ZFMISC_1:37;
then A183: LSeg(p1,p11) /\ L1 = {} by A182,TOPREAL1:21,ZFMISC_1:39;
A184: LSeg(p11,p2) /\ LSeg(p1,p01) c= L4 /\ L2
by A7,A161,XBOOLE_1:27;
now assume p11 in LSeg(p11,p2) /\ LSeg(p1,p01);
then p11 in LSeg(p01,p1) & p01`1 <= p1`1
by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p11`1 <= p1`1 by TOPREAL1:9;
then p1`1 = 1 by A5,A6,Lm4,AXIOMS:21;
hence contradiction by A5,A6,A181,EUCLID:57;
end;
then {p11} <> LSeg(p11,p2) /\ LSeg(p1,p01) by ZFMISC_1:37;
then LSeg(p11,p2) /\ LSeg(p1,p01) = {}
by A184,TOPREAL1:24,ZFMISC_1:39;
hence P1 /\ P2
= {p1,p2} by A166,A183,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
end;
Lm25:
p1 <> p2 & p2 in R^2-unit_square &
p1 in LSeg(p00, p10) implies
ex P1,P2 being non empty Subset of TOP-REAL 2
st P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 &
R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2}
proof assume that
A1: p1 <> p2 and
A2: p2 in R^2-unit_square and
A3: p1 in LSeg(p00, p10);
A4: p2 in L1 \/ L2 or p2 in L3 \/ L4 by A2,TOPREAL1:20,XBOOLE_0:def 2;
consider p such that
A5: p = p1 and A6: p`1 <= 1 & p`1 >= 0 & p`2 = 0 by A3,TOPREAL1:19;
A7: LSeg(p00,p1) c= L3 by A3,Lm14,TOPREAL1:12;
A8: LSeg(p10,p1) c= L3 by A3,Lm17,TOPREAL1:12;
then LSeg(p10,p1) /\ L2 c= L3 /\ L2 & L3 /\ L2 = {}
by TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A9: LSeg(p10,p1) /\ L2 = {} by XBOOLE_1:3;
p10 in LSeg(p10,p1) by TOPREAL1:6;
then A10: LSeg(p10,p1) /\ L4 c= L3 /\ L4 & LSeg(p10,p1) /\ L4 <> {}
by A8,Lm18,XBOOLE_0:def 3,XBOOLE_1:26;
p00 in LSeg(p1,p00) by TOPREAL1:6;
then A11: LSeg(p1,p00) /\ L1 c= L3 /\ L1 &
p00 in LSeg(p1,p00) /\ L1 by A7,Lm13,XBOOLE_0:def 3,XBOOLE_1:26;
A12: LSeg(p1,p00) /\ LSeg(p1,p10)
= {p1} by A3,TOPREAL1:14;
LSeg(p1,p00) /\ L2 c= L3 /\ L2 & L3 /\ L2 = {}
by A7,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A13: LSeg(p1,p00) /\ L2 = {} by XBOOLE_1:3;
per cases by A4,XBOOLE_0:def 2;
suppose A14: p2 in L1;
then A15: ex q st q = p2 & q`1 = 0 & q`2 <= 1 & q`2 >= 0 by TOPREAL1:19;
A16: LSeg(p00,p2) c= L1 by A14,Lm13,TOPREAL1:12;
A17: LSeg(p2,p01) c= L1 by A14,Lm15,TOPREAL1:12;
take P1 = LSeg(p1,p00) \/ LSeg(p00,p2),P2
= LSeg(p1,p10) \/ (L4 \/ L2 \/ LSeg(p01,p2));
p00 in LSeg(p1,p00) & p00 in LSeg(p00,p2) by TOPREAL1:6;
then LSeg(p1,p00) /\ LSeg(p00,p2) c= L3 /\ L1 &
p00 in LSeg(p1,p00) /\ LSeg(p00,p2) & L1 /\ L3 = {p00}
by A7,A16,TOPREAL1:23,XBOOLE_0:def 3,XBOOLE_1:27;
then LSeg(p1,p00) /\ LSeg(p00,p2) = {p00} & (p1 <> p00 or p00 <> p2)
by A1,ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by TOPREAL1:18;
L4 is_an_arc_of p10,p11 & L2 is_an_arc_of p11,p01
by Lm4,TOPREAL1:15;
then A18: L4 \/ L2 is_an_arc_of p10,p01 by TOPREAL1:5,24;
L4 /\ LSeg(p01,p2) c= L4 /\ L1 by A17,XBOOLE_1:26;
then A19: L4 /\ LSeg(p01,p2) = {} by Lm3,XBOOLE_1:3;
p01 in LSeg(p01,p2) by TOPREAL1:6;
then A20: L2 /\ LSeg(p01,p2) c= L2 /\ L1 & p01 in L2 /\ LSeg(p01,p2)
by A17,Lm16,XBOOLE_0:def 3,XBOOLE_1:27;
(L4 \/ L2) /\ LSeg(p01,p2)
= (L4 /\ LSeg(p01,p2)) \/ (L2 /\ LSeg(p01,p2)) by XBOOLE_1:23
.= {p01} by A19,A20,TOPREAL1:21,ZFMISC_1:39;
then A21: L4 \/ L2 \/ LSeg(p01,p2) is_an_arc_of p10,p2 by A18,TOPREAL1:16;
A22: LSeg(p1,p10) /\ LSeg(p01,p2) c= L3 /\ L1
by A8,A17,XBOOLE_1:27;
now assume p00 in LSeg(p1,p10) /\ LSeg(p01,p2);
then p00 in LSeg(p1,p10) & p00 in LSeg(p2,p01) & p1`1 <= p10`1 &
p2`2 <= p01`2 by A5,A6,A15,EUCLID:56,XBOOLE_0:def 3;
then A23: 0 = p1`2 & 0 = p2`2 & 0 = p1`1 & 0 = p2`1 by A5,A6,A15,Lm4,
TOPREAL1:9,10;
then p1 = p00 by EUCLID:57 .= p2 by A23,EUCLID:57;
hence contradiction by A1;
end;
then {p00} <> LSeg(p1,p10) /\ LSeg(p01,p2) by ZFMISC_1:37;
then A24: LSeg(p1,p10) /\ LSeg(p01,p2) = {} by A22,TOPREAL1:23,ZFMISC_1:39;
LSeg(p1,p10) /\ (L4 \/ L2 \/ LSeg(p01,p2))
= (LSeg(p1,p10) /\ (L4 \/ L2)) \/ (LSeg(p1,p10) /\
LSeg(p01,p2)) by XBOOLE_1:23
.= (LSeg(p1,p10) /\ L4) \/ (LSeg(p10,p1) /\ L2) by A24,XBOOLE_1:23
.= {p10} by A9,A10,TOPREAL1:22,ZFMISC_1:39;
hence P2 is_an_arc_of p1,p2 by A21,TOPREAL1:17;
A25: LSeg(p1,p00) \/ LSeg(p1,p10) = L3 by A3,TOPREAL1:11;
A26: LSeg(p01,p2) \/ LSeg(p00,p2) = L1 by A14,TOPREAL1:11;
thus P1 \/ P2
= LSeg(p00,p2) \/ (LSeg(p1,p00) \/ (LSeg(p1,p10) \/
(L4 \/ L2 \/ LSeg(p01,p2)))) by XBOOLE_1:4
.= LSeg(p00,p2) \/ (L3 \/ (L4 \/ L2 \/ LSeg(p01,p2))) by A25,XBOOLE_1:4
.= LSeg(p00,p2) \/ (L3 \/ (L4 \/ L2) \/ LSeg(p01,p2)) by XBOOLE_1:4
.= LSeg(p00,p2) \/ (L3 \/ L4 \/ L2 \/ LSeg(p01,p2)) by XBOOLE_1:4
.= LSeg(p00,p2) \/ (L3 \/ L4 \/ (L2 \/ LSeg(p01,p2))) by XBOOLE_1:4
.= (L2 \/ LSeg(p01,p2) \/ LSeg(p00,p2)) \/ (L3 \/ L4) by XBOOLE_1:4
.= R^2-unit_square by A26,TOPREAL1:20,XBOOLE_1:4;
A27: {p1} = LSeg(p1,p00) /\ LSeg(p1,p10) by A3,TOPREAL1:14;
LSeg(p1,p00) /\ L2 c= L3 /\ L2 & L3 /\ L2 = {}
by A7,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A28: LSeg(p1,p00) /\ L2 = {} by XBOOLE_1:3;
A29: {p2} = LSeg(p00,p2) /\ LSeg(p01,p2) by A14,TOPREAL1:14;
LSeg(p00,p2) /\ L4 c= L1 /\ L4 & L1 /\ L4 = {} by A16,TOPREAL1:26,
XBOOLE_0:def 7,XBOOLE_1:26
;
then A30: LSeg(p00,p2) /\ L4 = {} by XBOOLE_1:3;
A31: P1 /\ P2 = (LSeg(p1,p00) /\ (LSeg(p1,p10) \/ (L4 \/ L2 \/ LSeg(p01,p2))))
\/ (LSeg(p00,p2) /\ (LSeg(p1,p10) \/ (L4 \/ L2 \/ LSeg(p01,p2))))
by XBOOLE_1:23
.= (LSeg(p1,p00) /\ LSeg(p1,p10))
\/ (LSeg(p1,p00) /\ (L4 \/ L2 \/ LSeg(p01,p2)))
\/ (LSeg(p00,p2) /\ (LSeg(p1,p10) \/ (L4 \/ L2 \/ LSeg(p01,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ (L4 \/ L2)) \/ (LSeg(p1,p00) /\
LSeg(p01,p2)))
\/ (LSeg(p00,p2) /\ (LSeg(p1,p10) \/ (L4 \/ L2 \/ LSeg(p01,p2))))
by A27,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ L4) \/ (LSeg(p1,p00) /\ L2)
\/ (LSeg(p1,p00) /\ LSeg(p01,p2)))
\/ (LSeg(p00,p2) /\ (LSeg(p1,p10) \/ (L4 \/ L2 \/ LSeg(p01,p2))))
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ L4) \/ (LSeg(p1,p00) /\ LSeg(p01,p2)))
\/ ((LSeg(p00,p2) /\ LSeg(p1,p10))
\/ (LSeg(p00,p2) /\ (L4 \/ L2 \/ LSeg(p01,p2)))) by A28,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ L4) \/ (LSeg(p1,p00) /\ LSeg(p01,p2)))
\/ ((LSeg(p00,p2) /\ (LSeg(p1,p10))
\/ ((LSeg(p00,p2) /\ (L4 \/ L2)) \/ {p2}))) by A29,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ L4) \/ (LSeg(p1,p00) /\ LSeg(p01,p2)))
\/ ((LSeg(p00,p2) /\ (LSeg(p1,p10))
\/ (((LSeg(p00,p2) /\ L4) \/ (LSeg(p00,p2) /\ L2)) \/
{p2}))) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p00) /\ L4) \/ (LSeg(p1,p00) /\ LSeg(p01,p2)))
\/ ((LSeg(p00,p2) /\ LSeg(p1,p10))
\/ ((LSeg(p00,p2) /\ L2) \/ {p2})) by A30;
A32: now per cases;
suppose A33: p1 = p00;
then LSeg(p1,p00) /\ L4 = {p00} /\ L4 by TOPREAL1:7;
then A34: LSeg(p1,p00) /\ L4 = {} by Lm1,Lm5;
p1 in LSeg(p00,p2) & p1 in LSeg(p1,p10) by A33,TOPREAL1:6;
then LSeg(p00,p2) /\ LSeg(p1,p10) c= {p1} & LSeg(p00,p2) /\
LSeg(p1,p10) <> {}
by A16,A33,TOPREAL1:23,XBOOLE_0:def 3,XBOOLE_1:26;
then LSeg(p00,p2) /\ LSeg(p1,p10) = {p1} by ZFMISC_1:39;
hence P1 /\ P2
= {p1} \/ ({p1} \/ LSeg(p1,p00) /\ LSeg(p01,p2))
\/ ((LSeg(p00,p2) /\ L2) \/ {p2}) by A31,A34,XBOOLE_1:4
.= {p1} \/ {p1} \/ LSeg(p1,p00) /\ LSeg(p01,p2)
\/ ((LSeg(p00,p2) /\ L2) \/ {p2}) by XBOOLE_1:4
.= {p1} \/ LSeg(p1,p00) /\ LSeg(p01,p2)
\/ ((LSeg(p00,p2) /\ L2) \/ {p2});
suppose A35: p1 = p10;
then A36: LSeg(p00,p2) /\ LSeg(p1,p10) = LSeg(p00,p2) /\
{p10} by TOPREAL1:7;
not p10 in LSeg(p00,p2) by A16,Lm4,TOPREAL1:9;
then LSeg(p00,p2) /\ LSeg(p1,p10) = {} by A36,Lm1;
hence P1 /\ P2 = {p1} \/ {p1} \/ (LSeg(p1,p00) /\ LSeg(p01,p2))
\/ ((LSeg(p00,p2) /\ L2) \/ {p2}) by A31,A35,TOPREAL1:22,XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p00) /\ LSeg(p01,p2))
\/ ((LSeg(p00,p2) /\ L2) \/ {p2});
suppose A37: p1 <> p10 & p1 <> p00;
A38: LSeg(p1,p00) /\ L4 c= {p10} by A7,TOPREAL1:22,XBOOLE_1:26;
now assume p10 in LSeg(p1,p00) /\ L4;
then p10 in LSeg(p00,p1) & p00`1 <=
p1`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p10`1 <= p1`1 by TOPREAL1:9;
then p1`1 = 1 by A5,A6,Lm4,AXIOMS:21;
hence contradiction by A5,A6,A37,EUCLID:57;
end;
then {p10} <> LSeg(p1,p00) /\ L4 by ZFMISC_1:37;
then A39: LSeg(p1,p00) /\ L4 = {} by A38,ZFMISC_1:39;
A40: LSeg(p00,p2) /\ LSeg(p1,p10) c= {p00} by A8,A16,TOPREAL1:23,XBOOLE_1:
27;
now assume p00 in LSeg(p00,p2) /\ LSeg(p1,p10);
then p00 in
LSeg(p1,p10) & p1`1 <= p10`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then 0 = p1`1 by A5,A6,Lm4,TOPREAL1:9;
hence contradiction by A5,A6,A37,EUCLID:57;
end;
then {p00} <> LSeg(p00,p2) /\ LSeg(p1,p10) by ZFMISC_1:37;
then LSeg(p00,p2) /\ LSeg(p1,p10) = {} by A40,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (LSeg(p1,p00) /\ LSeg(p01,p2))
\/ ((LSeg(p00,p2) /\ L2) \/ {p2}) by A31,A39;
end;
now per cases;
suppose A41: p2 = p00;
A42: LSeg(p1,p00) /\ LSeg(p01,p2) c= L3 /\ L1 by A7,A17,XBOOLE_1:27;
p00 in LSeg(p1,p00) by TOPREAL1:6;
then LSeg(p1,p00) /\ LSeg(p01,p2) <> {} by A41,Lm13,XBOOLE_0:def 3
;
then A43: LSeg(p1,p00) /\
LSeg(p01,p2) = {p2} by A41,A42,TOPREAL1:23,ZFMISC_1:39;
LSeg(p00,p2) /\ L2 = {p00} /\ L2 by A41,TOPREAL1:7;
then LSeg(p00,p2) /\ L2 = {} by Lm1,Lm6;
hence P1 /\ P2
= {p1} \/ ({p2} \/ {p2}) by A32,A43,XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41;
hence P1 /\ P2 = {p1,p2};
suppose A44: p2 = p01;
then A45: LSeg(p1,p00) /\ LSeg(p01,p2) = LSeg(p1,p00) /\ {p01} by TOPREAL1
:7;
not p01 in LSeg(p1,p00) by A7,Lm4,TOPREAL1:10;
then A46: LSeg(p1,p00) /\ LSeg(p01,p2) = {} by A45,Lm1;
hence P1 /\ P2 = {p1,p2} by A32,A44,ENUMSET1:41,TOPREAL1:21;
thus P1 /\ P2 = {p1,p2} by A32,A44,A46,ENUMSET1:41,TOPREAL1:21;
suppose A47: p2 <> p01 & p2 <> p00;
A48: LSeg(p1,p00) /\ LSeg(p01,p2) c= L3 /\ L1 by A7,A17,XBOOLE_1:27;
now assume p00 in LSeg(p1,p00) /\ LSeg(p01,p2);
then p00 in
LSeg(p2,p01) & p2`2 <= p01`2 by A15,EUCLID:56,XBOOLE_0:def 3;
then p2`2 = 0 by A15,Lm4,TOPREAL1:10;
hence contradiction by A15,A47,EUCLID:57;
end;
then {p00} <> LSeg(p1,p00) /\ LSeg(p01,p2) by ZFMISC_1:37;
then A49: LSeg(p1,p00) /\ LSeg(p01,p2) = {} by A48,TOPREAL1:23,ZFMISC_1:39;
A50: LSeg(p00,p2) /\ L2 c= {p01} by A16,TOPREAL1:21,XBOOLE_1:26;
now assume p01 in LSeg(p00,p2) /\ L2;
then p01 in
LSeg(p00,p2) & p00`2 <= p2`2 by A15,EUCLID:56,XBOOLE_0:def 3;
then p01`2 <= p2`2 by TOPREAL1:10;
then 1 = p2`2 by A15,Lm4,AXIOMS:21;
hence contradiction by A15,A47,EUCLID:57;
end;
then {p01} <> LSeg(p00,p2) /\ L2 by ZFMISC_1:37;
then A51: LSeg(p00,p2) /\ L2 = {} by A50,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A32,A49,ENUMSET1:41;
thus P1 /\ P2 = {p1,p2} by A32,A49,A51,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
suppose A52: p2 in L2;
then A53: ex q st q = p2 & q`1 <= 1 & q`1 >= 0 & q`2 = 1 by TOPREAL1:19;
take P1 = LSeg(p1,p00) \/ L1 \/ LSeg(p01,p2),P2
= LSeg(p1,p10) \/ L4 \/ LSeg(p11,p2);
A54: LSeg(p2,p01) c= L2 by A52,Lm16,TOPREAL1:12;
A55: LSeg(p2,p11) c= L2 by A52,Lm19,TOPREAL1:12;
p01 in LSeg(p01,p2) by TOPREAL1:6;
then L1 /\ LSeg(p01,p2) c= {p01} & L1 /\ LSeg(p01,p2) <> {}
by A54,Lm15,TOPREAL1:21,XBOOLE_0:def 3,XBOOLE_1:26;
then L1 /\ LSeg(p01,p2) = {p01} by ZFMISC_1:39;
then A56: L1 \/ LSeg(p01,p2) is_an_arc_of p00,p2 by Lm4,TOPREAL1:18;
LSeg(p1,p00) /\ LSeg(p01,p2) c= L3 /\ L2 by A7,A54,XBOOLE_1:27;
then A57: LSeg(p1,p00) /\ LSeg(p01,p2) = {} by Lm2,XBOOLE_1:3;
LSeg(p1,p00) /\ (L1 \/ LSeg(p01,p2))
= (LSeg(p1,p00) /\ L1) \/ (LSeg(p1,p00) /\ LSeg(p01,p2)) by XBOOLE_1:23
.= {p00} by A11,A57,TOPREAL1:23,ZFMISC_1:39;
then LSeg(p1,p00) \/ (L1 \/ LSeg(p01,p2)) is_an_arc_of p1,p2
by A56,TOPREAL1:17;
hence P1 is_an_arc_of p1,p2 by XBOOLE_1:4;
L4 /\ LSeg(p11,p2) c= L4 /\ L2 &
p11 in LSeg(p11,p2) by A55,TOPREAL1:6,XBOOLE_1:26;
then L4 /\ LSeg(p11,p2) c= {p11} & L4 /\ LSeg(p11,p2) <> {}
by Lm20,TOPREAL1:24,XBOOLE_0:def 3;
then L4 /\ LSeg(p11,p2) = {p11} by ZFMISC_1:39;
then A58: L4 \/ LSeg(p11,p2) is_an_arc_of p10,p2 by Lm4,TOPREAL1:18;
LSeg(p1,p10) /\ LSeg(p11,p2) c= L3 /\ L2 by A8,A55,XBOOLE_1:27;
then A59: LSeg(p1,p10) /\ LSeg(p11,p2) = {} by Lm2,XBOOLE_1:3;
LSeg(p1,p10) /\ (L4 \/ LSeg(p11,p2))
= (LSeg(p1,p10) /\ L4) \/ (LSeg(p1,p10) /\ LSeg(p11,p2)) by XBOOLE_1:23
.= {p10} by A10,A59,TOPREAL1:22,ZFMISC_1:39;
then LSeg(p1,p10) \/ (L4 \/ LSeg(p11,p2)) is_an_arc_of p1,p2
by A58,TOPREAL1:17;
hence P2 is_an_arc_of p1,p2 by XBOOLE_1:4;
thus R^2-unit_square = L1 \/ (LSeg(p01,p2) \/ LSeg(p11,p2)) \/ (L3 \/
L4) by A52,TOPREAL1:11,20
.= L1 \/ LSeg(p01,p2) \/ LSeg(p11,p2) \/ (L3 \/ L4) by XBOOLE_1:4
.= L1 \/ LSeg(p01,p2) \/ ((L3 \/ L4) \/ LSeg(p11,p2)) by XBOOLE_1:4
.= L1 \/ LSeg(p01,p2) \/ (L3 \/ (L4 \/ LSeg(p11,p2))) by XBOOLE_1:4
.= L1 \/ LSeg(p01,p2) \/ (LSeg(p1,p00) \/ LSeg(p1,p10)
\/ (L4 \/ LSeg(p11,p2))) by A3,TOPREAL1:11
.= L1 \/ LSeg(p01,p2) \/ (LSeg(p1,p00) \/ (LSeg(p1,p10)
\/ (L4 \/ LSeg(p11,p2)))) by XBOOLE_1:4
.= L1 \/ LSeg(p01,p2) \/ (LSeg(p1,p00) \/ (LSeg(p1,p10)
\/ L4 \/ LSeg(p11,p2))) by XBOOLE_1:4
.= (LSeg(p1,p00) \/ (L1 \/ LSeg(p01,p2))) \/ (LSeg(p1,p10)
\/ L4 \/ LSeg(p11,p2)) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4;
A60: LSeg(p01,p2) /\ LSeg(p11,p2)
= {p2} by A52,TOPREAL1:14;
LSeg(p01,p2) /\ LSeg(p1,p10) c= L2 /\ L3 by A8,A54,XBOOLE_1:27;
then A61: LSeg(p01,p2) /\ LSeg(p1,p10) = {} by Lm2,XBOOLE_1:3;
LSeg(p1,p00) /\ LSeg(p11,p2) c= L3 /\ L2 & L3 /\ L2 = {}
by A7,A55,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:27;
then A62: LSeg(p1,p00) /\ LSeg(p11,p2) = {} by XBOOLE_1:3;
A63: P1 /\ P2
= (LSeg(p1,p00) \/ L1) /\ (LSeg(p1,p10) \/ L4 \/ LSeg(p11,p2))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p10) \/ L4 \/ LSeg(p11,p2))) by XBOOLE_1:
23
.= (LSeg(p1,p00) \/ L1) /\ (LSeg(p1,p10) \/ L4 \/ LSeg(p11,p2))
\/ (LSeg(p01,p2) /\ (LSeg(p1,p10) \/ L4) \/ {p2}) by A60,XBOOLE_1:23
.= (LSeg(p1,p00) \/ L1) /\ (LSeg(p1,p10) \/ L4 \/ LSeg(p11,p2))
\/ ((LSeg(p01,p2) /\ LSeg(p1,p10)) \/ (LSeg(p01,p2) /\ L4) \/ {p2})
by XBOOLE_1:23
.= (LSeg(p1,p00) /\ (LSeg(p1,p10) \/ L4 \/ LSeg(p11,p2)))
\/ (L1 /\ (LSeg(p1,p10) \/ L4 \/ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ L4) \/ {p2}) by A61,XBOOLE_1:23
.= ((LSeg(p1,p00) /\ (LSeg(p1,p10) \/ L4))
\/ (LSeg(p1,p00) /\ LSeg(p11,p2)))
\/ (L1 /\ (LSeg(p1,p10) \/ L4 \/ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ L4) \/ {p2}) by XBOOLE_1:23
.= ({p1} \/ (LSeg(p1,p00) /\ L4))
\/ (L1 /\ (LSeg(p1,p10) \/ L4 \/ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ L4) \/ {p2}) by A12,A62,XBOOLE_1:23
.= ({p1} \/ (LSeg(p1,p00) /\ L4))
\/ ((L1 /\ (LSeg(p1,p10) \/ L4)) \/ (L1 /\ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ L4) \/ {p2}) by XBOOLE_1:23
.= ({p1} \/ (LSeg(p1,p00) /\ L4))
\/ ((L1 /\ LSeg(p1,p10)) \/ (L1 /\ L4) \/ (L1 /\ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ L4) \/ {p2}) by XBOOLE_1:23
.= ({p1} \/ (LSeg(p1,p00) /\ L4))
\/ ((L1 /\ LSeg(p1,p10)) \/ (L1 /\ LSeg(p11,p2)))
\/ ((LSeg(p01,p2) /\ L4) \/ {p2}) by Lm3;
A64: now per cases;
suppose A65: p1 = p00;
then LSeg(p1,p00) /\ L4 = {p00} /\ L4 by TOPREAL1:7;
then LSeg(p1,p00) /\ L4 = {} by Lm1,Lm5;
hence P1 /\ P2 = {p1} \/ {p1} \/ (L1 /\ LSeg(p11,p2))
\/ ((LSeg(p01,p2) /\ L4) \/ {p2}) by A63,A65,TOPREAL1:23,XBOOLE_1:4
.= {p1} \/ (L1 /\ LSeg(p11,p2)) \/ ((LSeg(p01,p2) /\ L4) \/ {p2});
suppose A66: p1 = p10;
then L1 /\ LSeg(p1,p10) = L1 /\ {p10} by TOPREAL1:7;
then L1 /\ LSeg(p1,p10) = {} by Lm1,Lm9;
hence P1 /\ P2 = {p1} \/ (L1 /\ LSeg(p11,p2)) \/ ((LSeg(p01,p2) /\ L4)
\/
{p2})
by A63,A66,TOPREAL1:22;
suppose A67: p1 <> p10 & p1 <> p00;
A68: LSeg(p1,p00) /\ L4 c= {p10} by A7,TOPREAL1:22,XBOOLE_1:26;
now assume p10 in LSeg(p1,p00) /\ L4;
then p10 in
LSeg(p00,p1) & p00`1 <= p1`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p10`1 <= p1`1 by TOPREAL1:9;
then 1 = p1`1 by A5,A6,Lm4,AXIOMS:21;
hence contradiction by A5,A6,A67,EUCLID:57;
end;
then {p10} <> LSeg(p1,p00) /\ L4 by ZFMISC_1:37;
then A69: LSeg(p1,p00) /\ L4 = {} by A68,ZFMISC_1:39;
A70: L1 /\ LSeg(p1,p10) c= {p00} by A8,TOPREAL1:23,XBOOLE_1:26;
now assume p00 in L1 /\ LSeg(p1,p10);
then p00 in
LSeg(p1,p10) & p1`1 <= p10`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then 0 = p1`1 by A5,A6,Lm4,TOPREAL1:9;
hence contradiction by A5,A6,A67,EUCLID:57;
end;
then {p00} <> L1 /\ LSeg(p1,p10) by ZFMISC_1:37;
then L1 /\ LSeg(p1,p10) = {} by A70,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (L1 /\ LSeg(p11,p2)) \/ ((LSeg(p01,p2) /\ L4)
\/
{p2})
by A63,A69;
end;
now per cases;
suppose A71: p2 = p01;
then LSeg(p01,p2) /\ L4 = {p01} /\ L4 by TOPREAL1:7;
then LSeg(p01,p2) /\ L4 = {} by Lm1,Lm8;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A64,A71,TOPREAL1:21,XBOOLE_1
:4
.= {p1,p2} by ENUMSET1:41;
suppose A72: p2 = p11;
then L1 /\ LSeg(p11,p2) = L1 /\ {p11} by TOPREAL1:7;
then L1 /\ LSeg(p11,p2) = {} by Lm1,Lm11;
hence P1 /\ P2 = {p1,p2} by A64,A72,ENUMSET1:41,TOPREAL1:24;
suppose A73: p2 <> p11 & p2 <> p01;
A74: L1 /\ LSeg(p11,p2) c= {p01} by A55,TOPREAL1:21,XBOOLE_1:26;
now assume p01 in L1 /\ LSeg(p11,p2);
then p01 in
LSeg(p2,p11) & p2`1 <= p11`1 by A53,EUCLID:56,XBOOLE_0:def 3;
then p2`1 = 0 by A53,Lm4,TOPREAL1:9;
hence contradiction by A53,A73,EUCLID:57;
end;
then {p01} <> L1 /\ LSeg(p11,p2) by ZFMISC_1:37;
then A75: L1 /\ LSeg(p11,p2) = {} by A74,ZFMISC_1:39;
A76: LSeg(p01,p2) /\ L4 c= {p11} by A54,TOPREAL1:24,XBOOLE_1:26;
now assume p11 in LSeg(p01,p2) /\ L4;
then p11 in
LSeg(p01,p2) & p01`1 <= p2`1 by A53,EUCLID:56,XBOOLE_0:def 3;
then p11`1 <= p2`1 by TOPREAL1:9;
then 1 = p2`1 by A53,Lm4,AXIOMS:21;
hence contradiction by A53,A73,EUCLID:57;
end;
then {p11} <> LSeg(p01,p2) /\ L4 by ZFMISC_1:37;
then LSeg(p01,p2) /\ L4 = {} by A76,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A64,A75,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
suppose A77: p2 in L3;
then consider q such that
A78: q = p2 and A79: q`1 <= 1 & q`1 >= 0 & q`2 = 0 by TOPREAL1:19;
A80: p = |[p`1,p`2]| & q = |[q`1,q`2]| by EUCLID:57;
A81: LSeg(p2,p10) c= L3 by A77,Lm17,TOPREAL1:12;
A82: LSeg(p2,p00) c= L3 by A77,Lm14,TOPREAL1:12;
A83: LSeg(p1,p2) c= L3 by A3,A77,TOPREAL1:12;
now per cases by A1,A5,A6,A78,A79,A80,REAL_1:def 5;
suppose A84: p`1 < q`1;
take P1 = LSeg(p1,p2),P2 = LSeg(p1,p00) \/ (L1 \/ L2 \/ L4 \/
LSeg(p10,p2));
thus P1 is_an_arc_of p1,p2 by A1,TOPREAL1:15;
A85: now assume
A86: LSeg(p1,p00) /\ LSeg(p10,p2) <> {};
consider a being Element of LSeg(p1,p00) /\ LSeg(p10,p2);
reconsider p = a as Point of TOP-REAL 2 by A86,TARSKI:def 3;
p in LSeg(p00,p1) & p in LSeg(p2,p10) & p00`1 <= p1`1 & p2`1 <= p10
`1
by A5,A6,A78,A79,A86,EUCLID:56,XBOOLE_0:def 3;
then p`1 <= p1`1 & p2`1 <= p`1 by TOPREAL1:9;
hence contradiction by A5,A78,A84,AXIOMS:22;
end;
A87: LSeg(p1,p00) /\ L4 c= {p10} by A7,TOPREAL1:22,XBOOLE_1:26;
now assume p10 in LSeg(p1,p00) /\ L4;
then p10 in LSeg(p00,p1) & p00`1 <=
p1`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
then p10`1 <= p1`1 by TOPREAL1:9;
hence contradiction by A5,A6,A79,A84,Lm4,AXIOMS:21;
end;
then {p10} <> LSeg(p1,p00) /\ L4 by ZFMISC_1:37;
then A88: LSeg(p1,p00) /\ L4 = {} by A87,ZFMISC_1:39;
LSeg(p1,p00) /\ L2 c= L3 /\ L2 & L3 /\ L2 = {}
by A7,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A89: LSeg(p1,p00) /\ L2 = {} by XBOOLE_1:3;
A90:
LSeg(p1,p00) /\ L1 c= L3 /\ L1 by A7,XBOOLE_1:26;
p00 in LSeg(p1,p00) by TOPREAL1:6;
then A91: LSeg(p1,p00) /\ L1 <> {} by Lm13,XBOOLE_0:def 3;
A92: LSeg(p1,p00) /\ (L1 \/ L2 \/ L4 \/ LSeg(p10,p2))
= LSeg(p1,p00) /\ (L1 \/ L2 \/ L4) \/ (LSeg(p1,p00) /\ LSeg(p10,p2))
by XBOOLE_1:23
.= LSeg(p1,p00) /\ (L1 \/ L2) \/ (LSeg(p1,p00) /\ L4) by A85,XBOOLE_1:
23
.= LSeg(p1,p00) /\ L1 \/ (LSeg(p1,p00) /\ L2) by A88,XBOOLE_1:23
.= {p00} by A89,A90,A91,TOPREAL1:23,ZFMISC_1:39;
L1 is_an_arc_of p00,p01 by Lm4,TOPREAL1:15;
then A93: L1 \/ L2 is_an_arc_of p00,p11 by TOPREAL1:16,21;
(L1 \/ L2) /\ L4 = L1 /\ L4 \/ L2 /\ L4 by XBOOLE_1:23
.= {p11} by Lm3,TOPREAL1:24;
then A94: L1 \/ L2 \/ L4 is_an_arc_of p00,p10 by A93,TOPREAL1:16;
A95:
L4 /\ LSeg(p10,p2) c= L4 /\ L3 by A81,XBOOLE_1:26;
p10 in LSeg(p10,p2) by TOPREAL1:6;
then L4 /\ LSeg(p10,p2) <> {} by Lm18,XBOOLE_0:def 3;
then A96: L4 /\ LSeg(p10,p2) = {p10} by A95,TOPREAL1:22,ZFMISC_1:39;
A97: L1 /\ LSeg(p10,p2) c= {p00} by A81,TOPREAL1:23,XBOOLE_1:26;
now assume p00 in L1 /\ LSeg(p10,p2);
then p00 in
LSeg(p2,p10) & p2`1 <= p10`1 by A78,A79,EUCLID:56,XBOOLE_0:def 3;
hence contradiction by A6,A78,A84,Lm4,TOPREAL1:9;
end;
then {p00} <> L1 /\ LSeg(p10,p2) by ZFMISC_1:37;
then A98: L1 /\ LSeg(p10,p2) = {} by A97,ZFMISC_1:39;
L2 /\ LSeg(p10,p2) c= L2 /\ L3 & L3 /\ L2 = {}
by A81,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A99: L2 /\ LSeg(p10,p2) = {} by XBOOLE_1:3;
(L1 \/ L2 \/ L4) /\ LSeg(p10,p2)
= (L1 \/ L2) /\ LSeg(p10,p2) \/ L4 /\ LSeg(p10,p2) by XBOOLE_1:23
.= (L1 /\ LSeg(p10,p2)) \/ (L2 /\ LSeg(p10,p2)) \/
{p10} by A96,XBOOLE_1:23
.= {p10} by A98,A99;
then L1 \/ L2 \/ L4 \/
LSeg(p10,p2) is_an_arc_of p00,p2 by A94,TOPREAL1:16;
hence P2 is_an_arc_of p1,p2 by A92,TOPREAL1:17;
thus P1 \/ P2
= LSeg(p00,p1) \/ LSeg(p1,p2) \/ (L1 \/ L2 \/ L4 \/
LSeg(p10,p2)) by XBOOLE_1:4
.= LSeg(p00,p1) \/ LSeg(p1,p2) \/ LSeg(p2,p10) \/ (L1 \/ L2 \/
L4) by XBOOLE_1:4
.= (L1 \/ L2 \/ L4) \/ L3 by A3,A77,TOPREAL1:13
.= R^2-unit_square by TOPREAL1:20,XBOOLE_1:4;
p1 in LSeg(p1,p2) & p1 in LSeg(p1,p00) by TOPREAL1:6;
then p1 in LSeg(p1,p2) /\ LSeg(p1,p00) by XBOOLE_0:def 3;
then A100: {p1} c= LSeg(p1,p2) /\ LSeg(p1,p00) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p1,p00) c= {p1}
proof
let a; assume A101: a in LSeg(p1,p2) /\ LSeg(p1,p00);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p1,p2) & p in LSeg(p00,p1) & p1`2 <= p2`2 & p1`1 <= p2`1
& p00`1 <= p1`1 by A5,A6,A78,A79,A84,A101,EUCLID:56,XBOOLE_0:def 3;
then p1`2 <= p`2 & p`2 <= p2`2 & p1`1 <= p`1 & p`1 <= p1`1
by TOPREAL1:9,10;
then p1`1 = p`1 & p`2 = 0 by A5,A6,A78,A79,AXIOMS:21;
then p = |[p1`1, 0]| by EUCLID:57 .= p1 by A5,A6,EUCLID:57;
hence a in {p1} by TARSKI:def 1;
end;
then A102: LSeg(p1,p2) /\ LSeg(p1,p00) = {p1} by A100,XBOOLE_0:def 10;
p2 in LSeg(p1,p2) & p2 in LSeg(p10,p2) by TOPREAL1:6;
then p2 in LSeg(p1,p2) /\ LSeg(p10,p2) by XBOOLE_0:def 3;
then A103: {p2} c= LSeg(p1,p2) /\ LSeg(p10,p2) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p10,p2) c= {p2}
proof
let a; assume A104: a in LSeg(p1,p2) /\ LSeg(p10,p2);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p1,p2) & p in LSeg(p2,p10) & p1`2 <= p2`2 & p1`1 <= p2`1
& p2`1 <= p10`1 by A5,A6,A78,A79,A84,A104,EUCLID:56,XBOOLE_0:def 3;
then p1`2 <= p`2 & p`2 <= p2`2 & p2`1 <= p`1 & p`1 <= p2`1
by TOPREAL1:9,10;
then p2`1 = p`1 & p`2 = 0 by A5,A6,A78,A79,AXIOMS:21;
then p = |[ p2`1, 0]| by EUCLID:57 .= p2 by A78,A79,EUCLID:57;
hence a in {p2} by TARSKI:def 1;
end;
then A105: LSeg(p1,p2) /\ LSeg(p10,p2) = {p2} by A103,XBOOLE_0:def 10;
LSeg(p1,p2) /\ L2 c= L3 /\ L2 & L3 /\ L2 = {}
by A83,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A106: LSeg(p1,p2) /\ L2 = {} by XBOOLE_1:3;
A107: P1 /\ P2
= (LSeg(p1,p2) /\ LSeg(p1,p00))
\/ (LSeg(p1,p2) /\ (L1 \/ L2 \/ L4 \/ LSeg(p10,p2))) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ (L1 \/ L2 \/ L4)) \/
{p2}) by A102,A105,XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ (L1 \/ L2)) \/ (LSeg(p1,p2) /\ L4) \/ {p2})
by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ L1) \/ (LSeg(p1,p2) /\ L2)
\/ (LSeg(p1,p2) /\ L4) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ ((LSeg(p1,p2) /\ L1) \/ ((LSeg(p1,p2) /\ L4) \/ {p2}))
by A106,XBOOLE_1:4
.= {p1} \/ (LSeg(p1,p2) /\ L1) \/ ((LSeg(p1,p2) /\ L4) \/ {p2})
by XBOOLE_1:4;
A108: now per cases;
suppose A109: p1 = p00;
A110: LSeg(p1,p2) /\ L1 c= L3 /\ L1 by A83,XBOOLE_1:26;
p1 in LSeg(p1,p2) by TOPREAL1:6;
then LSeg(p1,p2) /\ L1 <> {} by A109,Lm13,XBOOLE_0:def 3;
then LSeg(p1,p2) /\ L1 = {p1} by A109,A110,TOPREAL1:23,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ((LSeg(p1,p2) /\ L4) \/ {p2}) by A107;
suppose A111: p1 <> p00;
A112: LSeg(p1,p2) /\ L1 c= L3 /\ L1 by A83,XBOOLE_1:26;
now assume p00 in LSeg(p1,p2) /\ L1;
then p00 in LSeg(p1,p2) & p1`1 <= p2`1
by A5,A78,A84,XBOOLE_0:def 3;
then p1`1 = 0 by A5,A6,Lm4,TOPREAL1:9;
hence contradiction by A5,A6,A111,EUCLID:57;
end;
then {p00} <> LSeg(p1,p2) /\ L1 by ZFMISC_1:37;
then LSeg(p1,p2) /\ L1 = {} by A112,TOPREAL1:23,ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ((LSeg(p1,p2) /\ L4) \/ {p2}) by A107;
end;
now per cases;
suppose A113: p2 = p10;
then A114: LSeg(p1,p2) /\ L4 c= {p2} by A83,TOPREAL1:22,XBOOLE_1:26;
p2 in LSeg(p1,p2) by TOPREAL1:6;
then LSeg(p1,p2) /\ L4 <> {} by A113,Lm18,XBOOLE_0:def 3;
then LSeg(p1,p2) /\ L4 = {p2} by A114,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A108,ENUMSET1:41;
suppose A115: p2 <> p10;
A116: LSeg(p1,p2) /\ L4 c= {p10} by A83,TOPREAL1:22,XBOOLE_1:26;
now assume p10 in LSeg(p1,p2) /\ L4;
then p10 in LSeg(p1,p2) & p1`1 <= p2`1
by A5,A78,A84,XBOOLE_0:def 3;
then p10`1 <= p2`1 by TOPREAL1:9;
then p2`1 = 1 by A78,A79,Lm4,AXIOMS:21;
hence contradiction by A78,A79,A115,EUCLID:57;
end;
then {p10} <> LSeg(p1,p2) /\ L4 by ZFMISC_1:37;
then LSeg(p1,p2) /\ L4 = {} by A116,ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A108,ENUMSET1:41;
end;
hence P1 /\ P2 = {p1,p2};
suppose A117: q`1 < p`1;
take P1 = LSeg(p1,p2),P2 = LSeg(p1,p10) \/ (L4 \/ L2 \/ L1 \/
LSeg(p00,p2));
thus P1 is_an_arc_of p1,p2 by A1,TOPREAL1:15;
A118: now assume
A119: LSeg(p1,p10) /\ LSeg(p00,p2) <> {};
consider a being Element of LSeg(p1,p10) /\ LSeg(p00,p2);
reconsider p = a as Point of TOP-REAL 2 by A119,TARSKI:def 3;
p in LSeg(p1,p10) & p in LSeg(p00,p2) & p1`1 <= p10`1 & p00`1 <= p2
`1
by A5,A6,A78,A79,A119,EUCLID:56,XBOOLE_0:def 3;
then p1`1 <= p`1 & p`1 <= p2`1 by TOPREAL1:9;
hence contradiction by A5,A78,A117,AXIOMS:22;
end;
A120:
LSeg(p1,p10) /\ L1 c= L3 /\ L1 by A8,XBOOLE_1:26;
now assume p00 in LSeg(p1,p10) /\ L1;
then p00 in LSeg(p1,p10) & p1`1 <=
p10`1 by A5,A6,EUCLID:56,XBOOLE_0:def 3;
hence contradiction by A5,A79,A117,Lm4,TOPREAL1:9;
end;
then {p00} <> LSeg(p1,p10) /\ L1 by ZFMISC_1:37;
then A121: LSeg(p1,p10) /\ L1 = {} by A120,TOPREAL1:23,ZFMISC_1:39;
LSeg(p1,p10) /\ L2 c= L3 /\ L2 & L3 /\ L2 = {}
by A8,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A122: LSeg(p1,p10) /\ L2 = {} by XBOOLE_1:3;
A123: LSeg(p1,p10) /\ L4 c= {p10} by A8,TOPREAL1:22,XBOOLE_1:26;
p10 in LSeg(p1,p10) by TOPREAL1:6;
then A124: LSeg(p1,p10) /\ L4 <> {} by Lm18,XBOOLE_0:def 3;
A125: LSeg(p1,p10) /\ (L4 \/ L2 \/ L1 \/ LSeg(p00,p2))
= LSeg(p1,p10) /\ (L4 \/ L2 \/ L1) \/ (LSeg(p1,p10) /\ LSeg(p00,p2))
by XBOOLE_1:23
.= LSeg(p1,p10) /\ (L4 \/ L2) \/ (LSeg(p1,p10) /\ L1) by A118,XBOOLE_1:
23
.= LSeg(p1,p10) /\ L4 \/ (LSeg(p1,p10) /\ L2) by A121,XBOOLE_1:23
.= {p10} by A122,A123,A124,ZFMISC_1:39;
L4 is_an_arc_of p10,p11 by Lm4,TOPREAL1:15;
then A126: L4 \/ L2 is_an_arc_of p10,p01 by TOPREAL1:16,24;
(L4 \/ L2) /\ L1 = L1 /\ L4 \/ L2 /\ L1 by XBOOLE_1:23
.= {p01} by Lm3,TOPREAL1:21;
then A127: L4 \/ L2 \/ L1 is_an_arc_of p10,p00 by A126,TOPREAL1:16;
A128: L1 /\ LSeg(p00,p2) c= {p00} by A82,TOPREAL1:23,XBOOLE_1:26;
p00 in LSeg(p00,p2) by TOPREAL1:6;
then L1 /\ LSeg(p00,p2) <> {} by Lm13,XBOOLE_0:def 3;
then A129: L1 /\ LSeg(p00,p2) = {p00} by A128,ZFMISC_1:39;
A130:
L4 /\ LSeg(p00,p2) c= L4 /\ L3 by A82,XBOOLE_1:26;
now assume p10 in L4 /\ LSeg(p00,p2);
then p10 in
LSeg(p00,p2) & p00`1 <= p2`1 by A78,A79,EUCLID:56,XBOOLE_0:def 3;
then p10`1 <= p2`1 by TOPREAL1:9;
hence contradiction by A6,A78,A79,A117,Lm4,AXIOMS:21;
end;
then {p10} <> L4 /\ LSeg(p00,p2) by ZFMISC_1:37;
then A131: L4 /\ LSeg(p00,p2) = {} by A130,TOPREAL1:22,ZFMISC_1:39;
L2 /\ LSeg(p00,p2) c= L2 /\ L3 & L3 /\ L2 = {}
by A82,TOPREAL1:25,XBOOLE_0:def 7,XBOOLE_1:26;
then A132: L2 /\ LSeg(p00,p2) = {} by XBOOLE_1:3;
(L4 \/ L2 \/ L1) /\ LSeg(p00,p2)
= (L4 \/ L2) /\ LSeg(p00,p2) \/ L1 /\ LSeg(p00,p2) by XBOOLE_1:23
.= (L4 /\ LSeg(p00,p2)) \/ (L2 /\ LSeg(p00,p2)) \/
{p00} by A129,XBOOLE_1:23
.= {p00} by A131,A132;
then L4 \/ L2 \/ L1 \/
LSeg(p00,p2) is_an_arc_of p10,p2 by A127,TOPREAL1:16
;
hence P2 is_an_arc_of p1,p2 by A125,TOPREAL1:17;
thus P1 \/ P2
= LSeg(p2,p1) \/ LSeg(p1,p10) \/ (L4 \/ L2 \/ L1 \/
LSeg(p00,p2)) by XBOOLE_1:4
.= LSeg(p00,p2) \/ (LSeg(p2,p1) \/ LSeg(p1,p10)) \/ (L4 \/ L2 \/ L1)
by XBOOLE_1:4
.= L3 \/ (L4 \/ L2 \/ L1) by A3,A77,TOPREAL1:13
.= L3 \/ (L4 \/ (L1 \/ L2)) by XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:20,XBOOLE_1:4;
p1 in LSeg(p1,p2) & p1 in LSeg(p1,p10) by TOPREAL1:6;
then p1 in LSeg(p1,p2) /\ LSeg(p1,p10) by XBOOLE_0:def 3;
then A133: {p1} c= LSeg(p1,p2) /\ LSeg(p1,p10) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p1,p10) c= {p1}
proof
let a; assume A134: a in LSeg(p1,p2) /\ LSeg(p1,p10);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p2,p1) & p in LSeg(p1,p10) & p2`2 <= p1`2 & p2`1 <= p1`1
& p1`1 <= p10`1 by A5,A6,A78,A79,A117,A134,EUCLID:56,XBOOLE_0:def 3;
then p2`2 <= p`2 & p`2 <= p1`2 & p1`1 <= p`1 & p`1 <= p1`1
by TOPREAL1:9,10;
then p1`1 = p`1 & p`2 = 0 by A5,A6,A78,A79,AXIOMS:21;
then p = |[p1`1, 0]| by EUCLID:57 .= p1 by A5,A6,EUCLID:57;
hence a in {p1} by TARSKI:def 1;
end;
then A135: LSeg(p1,p2) /\ LSeg(p1,p10) = {p1} by A133,XBOOLE_0:def 10;
p2 in LSeg(p1,p2) & p2 in LSeg(p00,p2) by TOPREAL1:6;
then p2 in LSeg(p1,p2) /\ LSeg(p00,p2) by XBOOLE_0:def 3;
then A136: {p2} c= LSeg(p1,p2) /\ LSeg(p00,p2) by ZFMISC_1:37;
LSeg(p1,p2) /\ LSeg(p00,p2) c= {p2}
proof
let a; assume A137: a in LSeg(p1,p2) /\ LSeg(p00,p2);
then reconsider p = a as Point of TOP-REAL 2;
p in LSeg(p2,p1) & p in LSeg(p00,p2) & p2`1 <= p1`1 & p2`2 <= p1`2
& p00`1 <= p2`1 by A5,A6,A78,A79,A117,A137,EUCLID:56,XBOOLE_0:def 3;
then p2`2 <= p`2 & p`2 <= p1`2 & p2`1 <= p`1 & p`1 <= p2`1
by TOPREAL1:9,10;
then p2`1 = p`1 & p`2 = 0 by A5,A6,A78,A79,AXIOMS:21;
then p = |[ p2`1, 0]| by EUCLID:57 .= p2 by A78,A79,EUCLID:57;
hence a in {p2} by TARSKI:def 1;
end;
then A138: LSeg(p1,p2) /\ LSeg(p00,p2) = {p2} by A136,XBOOLE_0:def 10;
LSeg(p1,p2) /\ L2 c= L3 /\ L2 & L3 /\ L2 = {}