let p1, p2 be Point of (TOP-REAL 2); ( p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[1,0]|,|[1,1]|) 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} ) )
assume that
A1:
p1 <> p2
and
A2:
p2 in R^2-unit_square
and
A3:
p1 in LSeg (|[1,0]|,|[1,1]|)
; 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} )
A4:
( p2 in (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) or p2 in (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) )
by A2, TOPREAL1:def 2, XBOOLE_0:def 3;
A5:
LSeg (p1,|[1,1]|) c= LSeg (|[1,0]|,|[1,1]|)
by A3, Lm27, TOPREAL1:6;
|[1,1]| in LSeg (p1,|[1,1]|)
by RLTOPSP1:68;
then A6:
{} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by Lm26, XBOOLE_0:def 4;
|[1,0]| in LSeg (p1,|[1,0]|)
by RLTOPSP1:68;
then A7:
{} <> (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by Lm24, XBOOLE_0:def 4;
A8:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A3, Lm27, TOPREAL1:6, XBOOLE_1:26;
A9:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A3, Lm25, TOPREAL1:6, XBOOLE_1:26;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
then A10:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by A5, XBOOLE_1:3, XBOOLE_1:26;
A11:
LSeg (p1,|[1,0]|) c= LSeg (|[1,0]|,|[1,1]|)
by A3, Lm25, TOPREAL1:6;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
then A12:
(LSeg (|[1,0]|,p1)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by A11, XBOOLE_1:3, XBOOLE_1:26;
consider p being Point of (TOP-REAL 2) such that
A13:
p = p1
and
A14:
p `1 = 1
and
A15:
p `2 <= 1
and
A16:
p `2 >= 0
by A3, TOPREAL1:13;
per cases
( p2 in LSeg (|[0,0]|,|[0,1]|) or p2 in LSeg (|[0,1]|,|[1,1]|) or p2 in LSeg (|[0,0]|,|[1,0]|) or p2 in LSeg (|[1,0]|,|[1,1]|) )
by A4, XBOOLE_0:def 3;
suppose A17:
p2 in LSeg (
|[0,0]|,
|[0,1]|)
;
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} )
|[0,0]| in LSeg (
|[0,0]|,
p2)
by RLTOPSP1:68;
then A18:
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) <> {}
by Lm21, XBOOLE_0:def 4;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))
by A17, Lm20, TOPREAL1:6, XBOOLE_1:26;
then
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) = {|[0,0]|}
by A18, TOPREAL1:17, ZFMISC_1:33;
then A19:
(LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2)) is_an_arc_of |[1,0]|,
p2
by Lm4, Lm8, TOPREAL1:9, TOPREAL1:10;
A20:
LSeg (
p2,
|[0,0]|)
c= LSeg (
|[0,0]|,
|[0,1]|)
by A17, Lm20, TOPREAL1:6;
then A21:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) = {}
by A11, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A22:
LSeg (
p2,
|[0,1]|)
c= LSeg (
|[0,0]|,
|[0,1]|)
by A17, Lm22, TOPREAL1:6;
then A23:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = {}
by A5, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
then A24:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {}
by A5, A20, XBOOLE_1:3, XBOOLE_1:27;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
then A25:
(LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) = {}
by A11, A22, XBOOLE_1:3, XBOOLE_1:27;
A26:
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,p2)) = {p2}
by A17, TOPREAL1:8;
|[0,1]| in LSeg (
|[0,1]|,
p2)
by RLTOPSP1:68;
then A27:
|[0,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))
by Lm23, XBOOLE_0:def 4;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))
by A17, Lm22, TOPREAL1:6, XBOOLE_1:26;
then
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = {|[0,1]|}
by A27, TOPREAL1:15, ZFMISC_1:33;
then A28:
(LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2)) is_an_arc_of |[1,1]|,
p2
by Lm6, Lm10, TOPREAL1:9, TOPREAL1:10;
take P1 =
((LSeg (p1,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2));
ex 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} )take P2 =
((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2));
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )A29:
(LSeg (p1,|[1,1]|)) \/ (LSeg (p1,|[1,0]|)) = LSeg (
|[1,0]|,
|[1,1]|)
by A3, TOPREAL1:5;
(LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) =
((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))
by XBOOLE_1:23
.=
{|[1,1]|}
by A8, A6, A23, TOPREAL1:18, ZFMISC_1:33
;
then
(LSeg (p1,|[1,1]|)) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) is_an_arc_of p1,
p2
by A28, TOPREAL1:11;
hence
P1 is_an_arc_of p1,
p2
by XBOOLE_1:4;
( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )A30:
ex
q being
Point of
(TOP-REAL 2) st
(
q = p2 &
q `1 = 0 &
q `2 <= 1 &
q `2 >= 0 )
by A17, TOPREAL1:13;
(LSeg (p1,|[1,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2))) =
((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))
by XBOOLE_1:23
.=
{|[1,0]|}
by A9, A7, A21, TOPREAL1:16, ZFMISC_1:33
;
then
(LSeg (p1,|[1,0]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2))) is_an_arc_of p1,
p2
by A19, TOPREAL1:11;
hence
P2 is_an_arc_of p1,
p2
by XBOOLE_1:4;
( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )thus R^2-unit_square =
(((LSeg (|[0,0]|,p2)) \/ (LSeg (|[0,1]|,p2))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))
by A17, TOPREAL1:5, TOPREAL1:def 2
.=
((LSeg (|[0,0]|,p2)) \/ ((LSeg (|[0,1]|,p2)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))
by XBOOLE_1:4
.=
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))
by XBOOLE_1:4
.=
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2))))
by XBOOLE_1:4
.=
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (p1,|[1,1]|)) \/ ((LSeg (p1,|[1,0]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2)))))
by A29, XBOOLE_1:4
.=
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2))))
by XBOOLE_1:4
.=
((LSeg (p1,|[1,1]|)) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))
by XBOOLE_1:4
.=
P1 \/ P2
by XBOOLE_1:4
;
P1 /\ P2 = {p1,p2}A31:
(LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) = {p1}
by A3, TOPREAL1:8;
A32:
P1 /\ P2 =
(((LSeg (p1,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((LSeg (|[0,1]|,p2)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2))))
by XBOOLE_1:23
.=
(((LSeg (p1,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2})
by A26, XBOOLE_1:23
.=
(((LSeg (p1,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2})
by XBOOLE_1:23
.=
(((LSeg (p1,|[1,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by A25, XBOOLE_1:23
.=
(((LSeg (p1,|[1,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,|[1,1]|)) /\ ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by XBOOLE_1:23
.=
(((LSeg (p1,|[1,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by XBOOLE_1:23
.=
((((LSeg (p1,|[1,1]|)) /\ ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by Lm2, XBOOLE_1:23
.=
(({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by A24, A31, XBOOLE_1:23
;
A33:
now P1 /\ P2 = ({p1} \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})per cases
( p1 = |[1,0]| or p1 = |[1,1]| or ( p1 <> |[1,1]| & p1 <> |[1,0]| ) )
;
suppose A34:
p1 = |[1,0]|
;
P1 /\ P2 = ({p1} \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})then
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) = (LSeg (|[0,1]|,|[1,1]|)) /\ {|[1,0]|}
by RLTOPSP1:70;
then
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) = {}
by Lm1, Lm17;
hence
P1 /\ P2 = ({p1} \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by A32, A34, TOPREAL1:16;
verum end; suppose A35:
p1 = |[1,1]|
;
P1 /\ P2 = ({p1} \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})then
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[1,1]|} /\ (LSeg (|[0,0]|,|[1,0]|))
by RLTOPSP1:70;
then
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by Lm1, Lm19;
hence P1 /\ P2 =
(({p1} \/ {p1}) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by A32, A35, TOPREAL1:18, XBOOLE_1:4
.=
({p1} \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
;
verum end; suppose A36:
(
p1 <> |[1,1]| &
p1 <> |[1,0]| )
;
P1 /\ P2 = ({p1} \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})now not |[1,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))assume
|[1,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))
;
contradictionthen A37:
|[1,1]| in LSeg (
|[1,0]|,
p1)
by XBOOLE_0:def 4;
|[1,0]| `2 <= p1 `2
by A13, A16, EUCLID:52;
then
|[1,1]| `2 <= p1 `2
by A37, TOPREAL1:4;
then
1
= p1 `2
by A13, A15, Lm11, XXREAL_0:1;
hence
contradiction
by A13, A14, A36, EUCLID:53;
verum end; then A38:
{|[1,1]|} <> (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))
by ZFMISC_1:31;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) c= {|[1,1]|}
by A3, Lm25, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
then A39:
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) = {}
by A38, ZFMISC_1:33;
now not |[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))assume
|[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
;
contradictionthen A40:
|[1,0]| in LSeg (
p1,
|[1,1]|)
by XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2
by A13, A15, EUCLID:52;
then
p1 `2 = 0
by A13, A16, A40, Lm9, TOPREAL1:4;
hence
contradiction
by A13, A14, A36, EUCLID:53;
verum end; then A41:
{|[1,0]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by ZFMISC_1:31;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A3, Lm27, TOPREAL1:6, XBOOLE_1:26;
then
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by A41, TOPREAL1:16, ZFMISC_1:33;
hence
P1 /\ P2 = ({p1} \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by A32, A39;
verum end; end; end; now P1 /\ P2 = {p1,p2}per cases
( p2 = |[0,0]| or p2 = |[0,1]| or ( p2 <> |[0,1]| & p2 <> |[0,0]| ) )
;
suppose A42:
p2 = |[0,0]|
;
P1 /\ P2 = {p1,p2}then
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = (LSeg (|[0,1]|,|[1,1]|)) /\ {|[0,0]|}
by RLTOPSP1:70;
then
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {}
by Lm1, Lm13;
hence
P1 /\ P2 = {p1,p2}
by A33, A42, ENUMSET1:1, TOPREAL1:17;
verum end; suppose A43:
p2 = |[0,1]|
;
P1 /\ P2 = {p1,p2}then
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[0,1]|} /\ (LSeg (|[0,0]|,|[1,0]|))
by RLTOPSP1:70;
then
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by Lm1, Lm14;
hence P1 /\ P2 =
{p1} \/ ({p2} \/ {p2})
by A33, A43, TOPREAL1:15, XBOOLE_1:4
.=
{p1,p2}
by ENUMSET1:1
;
verum end; suppose A44:
(
p2 <> |[0,1]| &
p2 <> |[0,0]| )
;
P1 /\ P2 = {p1,p2}now not |[0,0]| in (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))assume
|[0,0]| in (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))
;
contradictionthen A45:
|[0,0]| in LSeg (
p2,
|[0,1]|)
by XBOOLE_0:def 4;
p2 `2 <= |[0,1]| `2
by A30, EUCLID:52;
then
0 = p2 `2
by A30, A45, Lm5, TOPREAL1:4;
hence
contradiction
by A30, A44, EUCLID:53;
verum end; then A46:
{|[0,0]|} <> (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))
by ZFMISC_1:31;
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= {|[0,0]|}
by A17, Lm22, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
then A47:
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by A46, ZFMISC_1:33;
now not |[0,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))assume
|[0,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))
;
contradictionthen A48:
|[0,1]| in LSeg (
|[0,0]|,
p2)
by XBOOLE_0:def 4;
|[0,0]| `2 <= p2 `2
by A30, EUCLID:52;
then
|[0,1]| `2 <= p2 `2
by A48, TOPREAL1:4;
then
p2 `2 = 1
by A30, Lm7, XXREAL_0:1;
hence
contradiction
by A30, A44, EUCLID:53;
verum end; then A49:
{|[0,1]|} <> (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))
by ZFMISC_1:31;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))
by A17, Lm20, TOPREAL1:6, XBOOLE_1:26;
then
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {}
by A49, TOPREAL1:15, ZFMISC_1:33;
hence
P1 /\ P2 = {p1,p2}
by A33, A47, ENUMSET1:1;
verum end; end; end; hence
P1 /\ P2 = {p1,p2}
;
verum end; suppose A50:
p2 in LSeg (
|[0,1]|,
|[1,1]|)
;
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} )then A51:
ex
q being
Point of
(TOP-REAL 2) st
(
q = p2 &
q `1 <= 1 &
q `1 >= 0 &
q `2 = 1 )
by TOPREAL1:13;
now not |[1,1]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2))A52:
|[0,1]| `1 <= p2 `1
by A51, EUCLID:52;
assume A53:
|[1,1]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2))
;
contradictionthen A54:
|[1,1]| in LSeg (
|[1,0]|,
p1)
by XBOOLE_0:def 4;
|[1,1]| in LSeg (
|[0,1]|,
p2)
by A53, XBOOLE_0:def 4;
then
|[1,1]| `1 <= p2 `1
by A52, TOPREAL1:3;
then A55:
1
= p2 `1
by A51, Lm10, XXREAL_0:1;
|[1,0]| `2 <= p1 `2
by A13, A16, EUCLID:52;
then
|[1,1]| `2 <= p1 `2
by A54, TOPREAL1:4;
then
1
= p1 `2
by A13, A15, Lm11, XXREAL_0:1;
then p1 =
|[1,1]|
by A13, A14, EUCLID:53
.=
p2
by A51, A55, EUCLID:53
;
hence
contradiction
by A1;
verum end; then A56:
{|[1,1]|} <> (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2))
by ZFMISC_1:31;
A57:
LSeg (
|[0,0]|,
|[0,1]|)
is_an_arc_of |[0,0]|,
|[0,1]|
by Lm5, Lm7, TOPREAL1:9;
LSeg (
|[0,0]|,
|[1,0]|)
is_an_arc_of |[1,0]|,
|[0,0]|
by Lm4, Lm8, TOPREAL1:9;
then A58:
(LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)) is_an_arc_of |[1,0]|,
|[0,1]|
by A57, TOPREAL1:2, TOPREAL1:17;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
then A59:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by A5, XBOOLE_1:3, XBOOLE_1:26;
take P1 =
(LSeg (p1,|[1,1]|)) \/ (LSeg (|[1,1]|,p2));
ex 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} )take P2 =
(LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)));
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )A60:
(LSeg (p1,|[1,1]|)) \/ (LSeg (p1,|[1,0]|)) = LSeg (
|[1,0]|,
|[1,1]|)
by A3, TOPREAL1:5;
|[0,1]| in LSeg (
|[0,1]|,
p2)
by RLTOPSP1:68;
then A61:
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) <> {}
by Lm22, XBOOLE_0:def 4;
A62:
|[1,1]| in LSeg (
|[1,1]|,
p2)
by RLTOPSP1:68;
|[1,1]| in LSeg (
p1,
|[1,1]|)
by RLTOPSP1:68;
then A63:
|[1,1]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,1]|,p2))
by A62, XBOOLE_0:def 4;
A64:
LSeg (
|[1,1]|,
p2)
c= LSeg (
|[0,1]|,
|[1,1]|)
by A50, Lm26, TOPREAL1:6;
then
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A5, XBOOLE_1:27;
then A65:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) = {|[1,1]|}
by A63, TOPREAL1:18, ZFMISC_1:33;
(
p1 <> |[1,1]| or
|[1,1]| <> p2 )
by A1;
hence
P1 is_an_arc_of p1,
p2
by A65, TOPREAL1:12;
( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )A66:
{p1} = (LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))
by A3, TOPREAL1:8;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by TOPREAL1:19, XBOOLE_0:def 7;
then A67:
(LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by A64, XBOOLE_1:3, XBOOLE_1:26;
A68:
LSeg (
p2,
|[0,1]|)
c= LSeg (
|[0,1]|,
|[1,1]|)
by A50, Lm23, TOPREAL1:6;
then A69:
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) c= {|[0,1]|}
by TOPREAL1:15, XBOOLE_1:27;
A70:
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) = {}
by A68, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[0,1]|,p2)) =
((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)))
by XBOOLE_1:23
.=
{|[0,1]|}
by A70, A69, A61, ZFMISC_1:33
;
then A71:
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)) is_an_arc_of |[1,0]|,
p2
by A58, TOPREAL1:10;
A72:
{p2} = (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,1]|,p2))
by A50, TOPREAL1:8;
A73:
(LSeg (|[0,1]|,p2)) \/ (LSeg (|[1,1]|,p2)) = LSeg (
|[0,1]|,
|[1,1]|)
by A50, TOPREAL1:5;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A11, A68, XBOOLE_1:27;
then A74:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) = {}
by A56, TOPREAL1:18, ZFMISC_1:33;
(LSeg (p1,|[1,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) =
((LSeg (p1,|[1,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)))
by XBOOLE_1:23
.=
((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[1,0]|,p1)) /\ (LSeg (|[0,0]|,|[0,1]|)))
by A74, XBOOLE_1:23
.=
{|[1,0]|}
by A9, A7, A12, TOPREAL1:16, ZFMISC_1:33
;
hence
P2 is_an_arc_of p1,
p2
by A71, TOPREAL1:11;
( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )thus P1 \/ P2 =
(LSeg (|[1,1]|,p2)) \/ ((LSeg (p1,|[1,1]|)) \/ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))))
by XBOOLE_1:4
.=
(LSeg (|[1,1]|,p2)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))
by A60, XBOOLE_1:4
.=
(LSeg (|[1,1]|,p2)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ (LSeg (|[0,1]|,p2)))
by XBOOLE_1:4
.=
(LSeg (|[1,1]|,p2)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))
by XBOOLE_1:4
.=
(LSeg (|[1,1]|,p2)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))))
by XBOOLE_1:4
.=
(((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))
by XBOOLE_1:4
.=
R^2-unit_square
by A73, TOPREAL1:def 2, XBOOLE_1:4
;
P1 /\ P2 = {p1,p2}A75:
P1 /\ P2 =
((LSeg (p1,|[1,1]|)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))))
by XBOOLE_1:23
.=
(((LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))))
by XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))))
by A66, XBOOLE_1:23
.=
({p1} \/ ((((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))))
by XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[1,1]|,p2)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))))
by A59, XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ (((LSeg (|[1,1]|,p2)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}))
by A72, XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ ((((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}))
by XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2}))
by A67
;
A76:
now P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})per cases
( p1 = |[1,0]| or p1 = |[1,1]| or ( p1 <> |[1,1]| & p1 <> |[1,0]| ) )
;
suppose A77:
p1 = |[1,0]|
;
P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})then A78:
(LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) = (LSeg (|[1,1]|,p2)) /\ {|[1,0]|}
by RLTOPSP1:70;
not
|[1,0]| in LSeg (
|[1,1]|,
p2)
by A64, Lm7, Lm9, Lm11, TOPREAL1:4;
then A79:
(LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) = {}
by A78, Lm1;
thus P1 /\ P2 =
(({p1} \/ {p1}) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2}))
by A75, A77, TOPREAL1:16, XBOOLE_1:4
.=
({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
by A79
;
verum end; suppose A80:
p1 = |[1,1]|
;
P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
|[1,1]| in LSeg (
|[1,1]|,
p2)
by RLTOPSP1:68;
then A81:
(LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) <> {}
by A80, Lm27, XBOOLE_0:def 4;
(LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) c= {p1}
by A64, A80, TOPREAL1:18, XBOOLE_1:27;
then A82:
(LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) = {p1}
by A81, ZFMISC_1:33;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[1,1]|} /\ (LSeg (|[0,0]|,|[1,0]|))
by A80, RLTOPSP1:70;
then
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by Lm1, Lm19;
hence P1 /\ P2 =
({p1} \/ ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
by A75, A82, XBOOLE_1:4
.=
(({p1} \/ {p1}) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
by XBOOLE_1:4
.=
({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
;
verum end; suppose A83:
(
p1 <> |[1,1]| &
p1 <> |[1,0]| )
;
P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})now not |[1,1]| in (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))assume
|[1,1]| in (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))
;
contradictionthen A84:
|[1,1]| in LSeg (
|[1,0]|,
p1)
by XBOOLE_0:def 4;
|[1,0]| `2 <= p1 `2
by A13, A16, EUCLID:52;
then
|[1,1]| `2 <= p1 `2
by A84, TOPREAL1:4;
then
1
= p1 `2
by A13, A15, Lm11, XXREAL_0:1;
hence
contradiction
by A13, A14, A83, EUCLID:53;
verum end; then A85:
{|[1,1]|} <> (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))
by ZFMISC_1:31;
(LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) c= {|[1,1]|}
by A11, A64, TOPREAL1:18, XBOOLE_1:27;
then A86:
(LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) = {}
by A85, ZFMISC_1:33;
now not |[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))assume
|[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
;
contradictionthen A87:
|[1,0]| in LSeg (
p1,
|[1,1]|)
by XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2
by A13, A15, EUCLID:52;
then
p1 `2 = 0
by A13, A16, A87, Lm9, TOPREAL1:4;
hence
contradiction
by A13, A14, A83, EUCLID:53;
verum end; then A88:
{|[1,0]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by ZFMISC_1:31;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A3, Lm27, TOPREAL1:6, XBOOLE_1:26;
then
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by A88, TOPREAL1:16, ZFMISC_1:33;
hence
P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
by A75, A86;
verum end; end; end; now P1 /\ P2 = {p1,p2}per cases
( p2 = |[0,1]| or p2 = |[1,1]| or ( p2 <> |[1,1]| & p2 <> |[0,1]| ) )
;
suppose A89:
p2 = |[0,1]|
;
P1 /\ P2 = {p1,p2}then A90:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = (LSeg (p1,|[1,1]|)) /\ {|[0,1]|}
by RLTOPSP1:70;
not
|[0,1]| in LSeg (
p1,
|[1,1]|)
by A5, Lm6, Lm8, Lm10, TOPREAL1:3;
then
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = {}
by A90, Lm1;
hence
P1 /\ P2 = {p1,p2}
by A76, A89, ENUMSET1:1, TOPREAL1:15;
verum end; suppose A91:
p2 = |[1,1]|
;
P1 /\ P2 = {p1,p2}
|[1,1]| in LSeg (
p1,
|[1,1]|)
by RLTOPSP1:68;
then A92:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) <> {}
by A91, Lm26, XBOOLE_0:def 4;
(LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {|[1,1]|} /\ (LSeg (|[0,0]|,|[0,1]|))
by A91, RLTOPSP1:70;
then A93:
(LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by Lm1, Lm18;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A5, A68, XBOOLE_1:27;
then
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = {p2}
by A91, A92, TOPREAL1:18, ZFMISC_1:33;
hence P1 /\ P2 =
{p1} \/ ({p2} \/ {p2})
by A76, A93, XBOOLE_1:4
.=
{p1,p2}
by ENUMSET1:1
;
verum end; suppose A94:
(
p2 <> |[1,1]| &
p2 <> |[0,1]| )
;
P1 /\ P2 = {p1,p2}now not |[0,1]| in (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))assume
|[0,1]| in (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))
;
contradictionthen A95:
|[0,1]| in LSeg (
p2,
|[1,1]|)
by XBOOLE_0:def 4;
p2 `1 <= |[1,1]| `1
by A51, EUCLID:52;
then
p2 `1 = 0
by A51, A95, Lm6, TOPREAL1:3;
hence
contradiction
by A51, A94, EUCLID:53;
verum end; then A96:
{|[0,1]|} <> (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))
by ZFMISC_1:31;
(LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))
by A50, Lm26, TOPREAL1:6, XBOOLE_1:26;
then A97:
(LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by A96, TOPREAL1:15, ZFMISC_1:33;
now not |[1,1]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))assume
|[1,1]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))
;
contradictionthen A98:
|[1,1]| in LSeg (
|[0,1]|,
p2)
by XBOOLE_0:def 4;
|[0,1]| `1 <= p2 `1
by A51, EUCLID:52;
then
|[1,1]| `1 <= p2 `1
by A98, TOPREAL1:3;
then
1
= p2 `1
by A51, Lm10, XXREAL_0:1;
hence
contradiction
by A51, A94, EUCLID:53;
verum end; then A99:
{|[1,1]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))
by ZFMISC_1:31;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A5, A68, XBOOLE_1:27;
then
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = {}
by A99, TOPREAL1:18, ZFMISC_1:33;
hence
P1 /\ P2 = {p1,p2}
by A76, A97, ENUMSET1:1;
verum end; end; end; hence
P1 /\ P2 = {p1,p2}
;
verum end; suppose A100:
p2 in LSeg (
|[0,0]|,
|[1,0]|)
;
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} )then A101:
ex
q being
Point of
(TOP-REAL 2) st
(
q = p2 &
q `1 <= 1 &
q `1 >= 0 &
q `2 = 0 )
by TOPREAL1:13;
now not |[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))A102:
|[0,0]| `1 <= p2 `1
by A101, EUCLID:52;
assume A103:
|[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))
;
contradictionthen A104:
|[1,0]| in LSeg (
p1,
|[1,1]|)
by XBOOLE_0:def 4;
|[1,0]| in LSeg (
|[0,0]|,
p2)
by A103, XBOOLE_0:def 4;
then
|[1,0]| `1 <= p2 `1
by A102, TOPREAL1:3;
then A105:
1
= p2 `1
by A101, Lm8, XXREAL_0:1;
p1 `2 <= |[1,1]| `2
by A13, A15, EUCLID:52;
then
0 = p1 `2
by A13, A16, A104, Lm9, TOPREAL1:4;
then
p1 = |[1,0]|
by A13, A14, EUCLID:53;
hence
contradiction
by A1, A101, A105, EUCLID:53;
verum end; then A106:
{|[1,0]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))
by ZFMISC_1:31;
A107:
LSeg (
|[0,0]|,
|[0,1]|)
is_an_arc_of |[0,1]|,
|[0,0]|
by Lm5, Lm7, TOPREAL1:9;
LSeg (
|[0,1]|,
|[1,1]|)
is_an_arc_of |[1,1]|,
|[0,1]|
by Lm6, Lm10, TOPREAL1:9;
then A108:
(LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)) is_an_arc_of |[1,1]|,
|[0,0]|
by A107, TOPREAL1:2, TOPREAL1:15;
take P1 =
(LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,p2));
ex 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} )take P2 =
(LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)));
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )A109:
(LSeg (p1,|[1,0]|)) \/ (LSeg (p1,|[1,1]|)) = LSeg (
|[1,0]|,
|[1,1]|)
by A3, TOPREAL1:5;
|[0,0]| in LSeg (
|[0,0]|,
p2)
by RLTOPSP1:68;
then A110:
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) <> {}
by Lm20, XBOOLE_0:def 4;
A111:
|[1,0]| in LSeg (
|[1,0]|,
p2)
by RLTOPSP1:68;
|[1,0]| in LSeg (
p1,
|[1,0]|)
by RLTOPSP1:68;
then A112:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) <> {}
by A111, XBOOLE_0:def 4;
A113:
LSeg (
p2,
|[1,0]|)
c= LSeg (
|[0,0]|,
|[1,0]|)
by A100, Lm24, TOPREAL1:6;
then
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A11, XBOOLE_1:27;
then A114:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) = {|[1,0]|}
by A112, TOPREAL1:16, ZFMISC_1:33;
(
p1 <> |[1,0]| or
p2 <> |[1,0]| )
by A1;
hence
P1 is_an_arc_of p1,
p2
by A114, TOPREAL1:12;
( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )A115:
(LSeg (p1,|[1,0]|)) /\ (LSeg (p1,|[1,1]|)) = {p1}
by A3, TOPREAL1:8;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by TOPREAL1:19, XBOOLE_0:def 7;
then A116:
(LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by A113, XBOOLE_1:3, XBOOLE_1:26;
A117:
LSeg (
p2,
|[0,0]|)
c= LSeg (
|[0,0]|,
|[1,0]|)
by A100, Lm21, TOPREAL1:6;
then A118:
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) c= {|[0,0]|}
by TOPREAL1:17, XBOOLE_1:27;
A119:
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {}
by A117, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[0,0]|,p2)) =
((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))
by XBOOLE_1:23
.=
{|[0,0]|}
by A119, A118, A110, ZFMISC_1:33
;
then A120:
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)) is_an_arc_of |[1,1]|,
p2
by A108, TOPREAL1:10;
A121:
(LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,p2)) = {p2}
by A100, TOPREAL1:8;
A122:
(LSeg (|[0,0]|,p2)) \/ (LSeg (|[1,0]|,p2)) = LSeg (
|[0,0]|,
|[1,0]|)
by A100, TOPREAL1:5;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A5, A117, XBOOLE_1:27;
then A123:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {}
by A106, TOPREAL1:16, ZFMISC_1:33;
(LSeg (p1,|[1,1]|)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))) =
((LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))
by XBOOLE_1:23
.=
((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))
by A123, XBOOLE_1:23
.=
{|[1,1]|}
by A8, A6, A10, TOPREAL1:18, ZFMISC_1:33
;
hence
P2 is_an_arc_of p1,
p2
by A120, TOPREAL1:11;
( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )thus P1 \/ P2 =
(LSeg (|[1,0]|,p2)) \/ ((LSeg (p1,|[1,0]|)) \/ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2)))))
by XBOOLE_1:4
.=
(LSeg (|[1,0]|,p2)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))
by A109, XBOOLE_1:4
.=
((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))) \/ (LSeg (|[1,0]|,p2))
by XBOOLE_1:4
.=
(((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))
by A122, XBOOLE_1:4
.=
R^2-unit_square
by TOPREAL1:def 2, XBOOLE_1:4
;
P1 /\ P2 = {p1,p2}A124:
P1 /\ P2 =
((LSeg (p1,|[1,0]|)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))))
by XBOOLE_1:23
.=
(((LSeg (p1,|[1,0]|)) /\ (LSeg (p1,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))))
by XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,0]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))))
by A115, XBOOLE_1:23
.=
({p1} \/ ((((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,0]|,p1)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))))
by XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))))
by A12, XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ (((LSeg (|[1,0]|,p2)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}))
by A121, XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ ((((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}))
by XBOOLE_1:23
.=
({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2}))
by A116
;
A125:
now P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})per cases
( p1 = |[1,0]| or p1 = |[1,1]| or ( p1 <> |[1,1]| & p1 <> |[1,0]| ) )
;
suppose A126:
p1 = |[1,0]|
;
P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
|[1,0]| in LSeg (
|[1,0]|,
p2)
by RLTOPSP1:68;
then A127:
(LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|)) <> {}
by A126, Lm25, XBOOLE_0:def 4;
(LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|)) c= {p1}
by A113, A126, TOPREAL1:16, XBOOLE_1:27;
then A128:
(LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|)) = {p1}
by A127, ZFMISC_1:33;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {|[1,0]|} /\ (LSeg (|[0,1]|,|[1,1]|))
by A126, RLTOPSP1:70;
then
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by Lm1, Lm17;
hence P1 /\ P2 =
({p1} \/ ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
by A124, A128, XBOOLE_1:4
.=
(({p1} \/ {p1}) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
by XBOOLE_1:4
.=
({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
;
verum end; suppose A129:
p1 = |[1,1]|
;
P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})then A130:
(LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|)) = (LSeg (|[1,0]|,p2)) /\ {|[1,1]|}
by RLTOPSP1:70;
not
|[1,1]| in LSeg (
|[1,0]|,
p2)
by A113, Lm5, Lm9, Lm11, TOPREAL1:4;
then
(LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|)) = {}
by A130, Lm1;
hence P1 /\ P2 =
(({p1} \/ {p1}) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
by A124, A129, TOPREAL1:18, XBOOLE_1:4
.=
({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
;
verum end; suppose A131:
(
p1 <> |[1,1]| &
p1 <> |[1,0]| )
;
P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})now not |[1,0]| in (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))assume
|[1,0]| in (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))
;
contradictionthen A132:
|[1,0]| in LSeg (
p1,
|[1,1]|)
by XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2
by A13, A15, EUCLID:52;
then
p1 `2 = 0
by A13, A16, A132, Lm9, TOPREAL1:4;
hence
contradiction
by A13, A14, A131, EUCLID:53;
verum end; then A133:
{|[1,0]|} <> (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))
by ZFMISC_1:31;
(LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|)) c= {|[1,0]|}
by A5, A113, TOPREAL1:16, XBOOLE_1:27;
then A134:
(LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|)) = {}
by A133, ZFMISC_1:33;
now not |[1,1]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))assume
|[1,1]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
;
contradictionthen A135:
|[1,1]| in LSeg (
|[1,0]|,
p1)
by XBOOLE_0:def 4;
|[1,0]| `2 <= p1 `2
by A13, A16, EUCLID:52;
then
|[1,1]| `2 <= p1 `2
by A135, TOPREAL1:4;
then
p1 `2 = 1
by A13, A15, Lm11, XXREAL_0:1;
hence
contradiction
by A13, A14, A131, EUCLID:53;
verum end; then A136:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) <> {|[1,1]|}
by ZFMISC_1:31;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A3, Lm25, TOPREAL1:6, XBOOLE_1:26;
then
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by A136, TOPREAL1:18, ZFMISC_1:33;
hence
P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
by A124, A134;
verum end; end; end; now P1 /\ P2 = {p1,p2}per cases
( p2 = |[0,0]| or p2 = |[1,0]| or ( p2 <> |[1,0]| & p2 <> |[0,0]| ) )
;
suppose A137:
p2 = |[0,0]|
;
P1 /\ P2 = {p1,p2}then A138:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) = (LSeg (p1,|[1,0]|)) /\ {|[0,0]|}
by RLTOPSP1:70;
not
|[0,0]| in LSeg (
p1,
|[1,0]|)
by A11, Lm4, Lm8, Lm10, TOPREAL1:3;
then
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) = {}
by A138, Lm1;
hence
P1 /\ P2 = {p1,p2}
by A125, A137, ENUMSET1:1, TOPREAL1:17;
verum end; suppose A139:
p2 = |[1,0]|
;
P1 /\ P2 = {p1,p2}
|[1,0]| in LSeg (
p1,
|[1,0]|)
by RLTOPSP1:68;
then A140:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) <> {}
by A139, Lm24, XBOOLE_0:def 4;
(LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {|[1,0]|} /\ (LSeg (|[0,0]|,|[0,1]|))
by A139, RLTOPSP1:70;
then A141:
(LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by Lm1, Lm16;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A11, A117, XBOOLE_1:27;
then
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) = {p2}
by A139, A140, TOPREAL1:16, ZFMISC_1:33;
hence P1 /\ P2 =
{p1} \/ ({p2} \/ {p2})
by A125, A141, XBOOLE_1:4
.=
{p1,p2}
by ENUMSET1:1
;
verum end; suppose A142:
(
p2 <> |[1,0]| &
p2 <> |[0,0]| )
;
P1 /\ P2 = {p1,p2}now not |[0,0]| in (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))assume
|[0,0]| in (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))
;
contradictionthen A143:
|[0,0]| in LSeg (
p2,
|[1,0]|)
by XBOOLE_0:def 4;
p2 `1 <= |[1,0]| `1
by A101, EUCLID:52;
then
p2 `1 = 0
by A101, A143, Lm4, TOPREAL1:3;
hence
contradiction
by A101, A142, EUCLID:53;
verum end; then A144:
{|[0,0]|} <> (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))
by ZFMISC_1:31;
(LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))
by A100, Lm24, TOPREAL1:6, XBOOLE_1:26;
then A145:
(LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by A144, TOPREAL1:17, ZFMISC_1:33;
now not |[1,0]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))assume
|[1,0]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))
;
contradictionthen A146:
|[1,0]| in LSeg (
|[0,0]|,
p2)
by XBOOLE_0:def 4;
|[0,0]| `1 <= p2 `1
by A101, EUCLID:52;
then
|[1,0]| `1 <= p2 `1
by A146, TOPREAL1:3;
then
p2 `1 = 1
by A101, Lm8, XXREAL_0:1;
hence
contradiction
by A101, A142, EUCLID:53;
verum end; then A147:
{|[1,0]|} <> (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))
by ZFMISC_1:31;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A11, A117, XBOOLE_1:27;
then
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) = {}
by A147, TOPREAL1:16, ZFMISC_1:33;
hence
P1 /\ P2 = {p1,p2}
by A125, A145, ENUMSET1:1;
verum end; end; end; hence
P1 /\ P2 = {p1,p2}
;
verum end; suppose A148:
p2 in LSeg (
|[1,0]|,
|[1,1]|)
;
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} )A149:
p = |[(p `1),(p `2)]|
by EUCLID:53;
A150:
LSeg (
p1,
p2)
c= LSeg (
|[1,0]|,
|[1,1]|)
by A3, A148, TOPREAL1:6;
consider q being
Point of
(TOP-REAL 2) such that A151:
q = p2
and A152:
q `1 = 1
and A153:
q `2 <= 1
and A154:
q `2 >= 0
by A148, TOPREAL1:13;
A155:
q = |[(q `1),(q `2)]|
by EUCLID:53;
now ex P1 being Element of K19( the carrier of (TOP-REAL 2)) ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )per cases
( p `2 < q `2 or q `2 < p `2 )
by A1, A13, A14, A151, A152, A149, A155, XXREAL_0:1;
suppose A156:
p `2 < q `2
;
ex P1 being Element of K19( the carrier of (TOP-REAL 2)) ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )A157:
(LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) c= {p2}
proof
let a be
object ;
TARSKI:def 3 ( not a in (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) or a in {p2} )
assume A158:
a in (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2))
;
a in {p2}
then reconsider p =
a as
Point of
(TOP-REAL 2) ;
A159:
p in LSeg (
p2,
|[1,1]|)
by A158, XBOOLE_0:def 4;
p2 `2 <= |[1,1]| `2
by A151, A153, EUCLID:52;
then A160:
p2 `2 <= p `2
by A159, TOPREAL1:4;
A161:
p in LSeg (
p1,
p2)
by A158, XBOOLE_0:def 4;
then A162:
p1 `1 <= p `1
by A13, A14, A151, A152, TOPREAL1:3;
p `2 <= p2 `2
by A13, A151, A156, A161, TOPREAL1:4;
then A163:
p2 `2 = p `2
by A160, XXREAL_0:1;
p `1 <= p2 `1
by A13, A14, A151, A152, A161, TOPREAL1:3;
then
p `1 = 1
by A13, A14, A151, A152, A162, XXREAL_0:1;
then p =
|[1,(p2 `2)]|
by A163, EUCLID:53
.=
p2
by A151, A152, EUCLID:53
;
hence
a in {p2}
by TARSKI:def 1;
verum
end;
|[1,0]| in LSeg (
p1,
|[1,0]|)
by RLTOPSP1:68;
then A164:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) <> {}
by Lm24, XBOOLE_0:def 4;
A165:
now not (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) <> {} set a = the
Element of
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2));
assume A166:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) <> {}
;
contradictionthen reconsider p = the
Element of
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) as
Point of
(TOP-REAL 2) by TARSKI:def 3;
A167:
p in LSeg (
|[1,0]|,
p1)
by A166, XBOOLE_0:def 4;
A168:
p in LSeg (
p2,
|[1,1]|)
by A166, XBOOLE_0:def 4;
p2 `2 <= |[1,1]| `2
by A151, A153, EUCLID:52;
then A169:
p2 `2 <= p `2
by A168, TOPREAL1:4;
|[1,0]| `2 <= p1 `2
by A13, A16, EUCLID:52;
then
p `2 <= p1 `2
by A167, TOPREAL1:4;
hence
contradiction
by A13, A151, A156, A169, XXREAL_0:2;
verum end; A170:
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[0,1]|,|[1,1]|)) =
((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))
by XBOOLE_1:23
.=
{|[0,1]|}
by Lm2, TOPREAL1:15
;
(LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)) is_an_arc_of |[1,0]|,
|[0,1]|
by Lm4, Lm8, TOPREAL1:9, TOPREAL1:10, TOPREAL1:17;
then A171:
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|)) is_an_arc_of |[1,0]|,
|[1,1]|
by A170, TOPREAL1:10;
now not |[1,1]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))assume
|[1,1]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
;
contradictionthen A172:
|[1,1]| in LSeg (
|[1,0]|,
p1)
by XBOOLE_0:def 4;
|[1,0]| `2 <= p1 `2
by A13, A16, EUCLID:52;
then
|[1,1]| `2 <= p1 `2
by A172, TOPREAL1:4;
hence
contradiction
by A13, A15, A153, A156, Lm11, XXREAL_0:1;
verum end; then A173:
{|[1,1]|} <> (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by ZFMISC_1:31;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A3, Lm25, TOPREAL1:6, XBOOLE_1:26;
then A174:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by A173, TOPREAL1:18, ZFMISC_1:33;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
then A175:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by A11, XBOOLE_1:3, XBOOLE_1:26;
now not |[1,0]| in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))assume
|[1,0]| in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))
;
contradictionthen A176:
|[1,0]| in LSeg (
p2,
|[1,1]|)
by XBOOLE_0:def 4;
p2 `2 <= |[1,1]| `2
by A151, A153, EUCLID:52;
hence
contradiction
by A16, A151, A156, A176, Lm9, TOPREAL1:4;
verum end; then A177:
{|[1,0]|} <> (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))
by ZFMISC_1:31;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[1,0]|}
by A148, Lm27, TOPREAL1:6, TOPREAL1:16, XBOOLE_1:26;
then A178:
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) = {}
by A177, ZFMISC_1:33;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
then A179:
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by A150, XBOOLE_1:3, XBOOLE_1:26;
A180:
(LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) c= {p1}
proof
let a be
object ;
TARSKI:def 3 ( not a in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) or a in {p1} )
assume A181:
a in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|))
;
a in {p1}
then reconsider p =
a as
Point of
(TOP-REAL 2) ;
A182:
p in LSeg (
|[1,0]|,
p1)
by A181, XBOOLE_0:def 4;
|[1,0]| `2 <= p1 `2
by A13, A16, EUCLID:52;
then A183:
p `2 <= p1 `2
by A182, TOPREAL1:4;
A184:
p in LSeg (
p1,
p2)
by A181, XBOOLE_0:def 4;
then A185:
p1 `1 <= p `1
by A13, A14, A151, A152, TOPREAL1:3;
p1 `2 <= p `2
by A13, A151, A156, A184, TOPREAL1:4;
then A186:
p1 `2 = p `2
by A183, XXREAL_0:1;
p `1 <= p2 `1
by A13, A14, A151, A152, A184, TOPREAL1:3;
then
p `1 = 1
by A13, A14, A151, A152, A185, XXREAL_0:1;
then p =
|[1,(p1 `2)]|
by A186, EUCLID:53
.=
p1
by A13, A14, EUCLID:53
;
hence
a in {p1}
by TARSKI:def 1;
verum
end; A187:
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A3, Lm25, TOPREAL1:6, XBOOLE_1:26;
|[1,1]| in LSeg (
|[1,1]|,
p2)
by RLTOPSP1:68;
then A188:
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) <> {}
by Lm26, XBOOLE_0:def 4;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[1,1]|}
by A148, Lm27, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
then A189:
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) = {|[1,1]|}
by A188, ZFMISC_1:33;
take P1 =
LSeg (
p1,
p2);
ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )take P2 =
(LSeg (p1,|[1,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)));
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )A190:
p1 in LSeg (
p1,
|[1,0]|)
by RLTOPSP1:68;
thus
P1 is_an_arc_of p1,
p2
by A1, TOPREAL1:9;
( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )A191:
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) c= (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))
by A148, Lm27, TOPREAL1:6, XBOOLE_1:26;
then A192:
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = {}
by A191, XBOOLE_1:3;
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (LSeg (|[1,1]|,p2)) =
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)))
by XBOOLE_1:23
.=
(((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)))) \/ {|[1,1]|}
by A189, XBOOLE_1:23
.=
{|[1,1]|}
by A178, A192
;
then A193:
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)) is_an_arc_of |[1,0]|,
p2
by A171, TOPREAL1:10;
(LSeg (p1,|[1,0]|)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) =
((LSeg (p1,|[1,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)))
by XBOOLE_1:23
.=
((LSeg (p1,|[1,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))
by A165, XBOOLE_1:23
.=
((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))
by A174, XBOOLE_1:23
.=
{|[1,0]|}
by A187, A164, A175, TOPREAL1:16, ZFMISC_1:33
;
hence
P2 is_an_arc_of p1,
p2
by A193, TOPREAL1:11;
( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )thus P1 \/ P2 =
((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) \/ ((LSeg (p1,|[1,0]|)) \/ (LSeg (p1,p2)))
by XBOOLE_1:4
.=
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (((LSeg (|[1,0]|,p1)) \/ (LSeg (p1,p2))) \/ (LSeg (p2,|[1,1]|)))
by XBOOLE_1:4
.=
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))
by A3, A148, TOPREAL1:7
.=
((LSeg (|[0,0]|,|[1,0]|)) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ (LSeg (|[1,0]|,|[1,1]|))
by XBOOLE_1:4
.=
R^2-unit_square
by TOPREAL1:def 2, XBOOLE_1:4
;
P1 /\ P2 = {p1,p2}A194:
p2 in LSeg (
|[1,1]|,
p2)
by RLTOPSP1:68;
p2 in LSeg (
p1,
p2)
by RLTOPSP1:68;
then
p2 in (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2))
by A194, XBOOLE_0:def 4;
then
{p2} c= (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2))
by ZFMISC_1:31;
then A195:
(LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) = {p2}
by A157, XBOOLE_0:def 10;
p1 in LSeg (
p1,
p2)
by RLTOPSP1:68;
then
p1 in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|))
by A190, XBOOLE_0:def 4;
then
{p1} c= (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|))
by ZFMISC_1:31;
then
(LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) = {p1}
by A180, XBOOLE_0:def 10;
then A196:
P1 /\ P2 =
{p1} \/ ((LSeg (p1,p2)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))
by XBOOLE_1:23
.=
{p1} \/ (((LSeg (p1,p2)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2})
by A195, XBOOLE_1:23
.=
{p1} \/ ((((LSeg (p1,p2)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2})
by XBOOLE_1:23
.=
{p1} \/ (((((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2})
by XBOOLE_1:23
.=
{p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}))
by A179, XBOOLE_1:4
.=
({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})
by XBOOLE_1:4
;
A197:
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A3, A148, TOPREAL1:6, XBOOLE_1:26;
A198:
now P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})per cases
( p1 = |[1,0]| or p1 <> |[1,0]| )
;
suppose A199:
p1 = |[1,0]|
;
P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})then
|[1,0]| in LSeg (
p1,
p2)
by RLTOPSP1:68;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) <> {}
by Lm24, XBOOLE_0:def 4;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {p1}
by A197, A199, TOPREAL1:16, ZFMISC_1:33;
hence
P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})
by A196;
verum end; suppose A200:
p1 <> |[1,0]|
;
P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})now not |[1,0]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))assume
|[1,0]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))
;
contradictionthen
|[1,0]| in LSeg (
p1,
p2)
by XBOOLE_0:def 4;
then
p1 `2 = 0
by A13, A16, A151, A156, Lm9, TOPREAL1:4;
hence
contradiction
by A13, A14, A200, EUCLID:53;
verum end; then
{|[1,0]|} <> (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))
by ZFMISC_1:31;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by A197, TOPREAL1:16, ZFMISC_1:33;
hence
P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})
by A196;
verum end; end; end; A201:
(LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A3, A148, TOPREAL1:6, XBOOLE_1:26;
now P1 /\ P2 = {p1,p2}per cases
( p2 = |[1,1]| or p2 <> |[1,1]| )
;
suppose A202:
p2 = |[1,1]|
;
P1 /\ P2 = {p1,p2}then
|[1,1]| in LSeg (
p1,
p2)
by RLTOPSP1:68;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) <> {}
by Lm26, XBOOLE_0:def 4;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {p2}
by A201, A202, TOPREAL1:18, ZFMISC_1:33;
hence
P1 /\ P2 = {p1,p2}
by A198, ENUMSET1:1;
verum end; suppose A203:
p2 <> |[1,1]|
;
P1 /\ P2 = {p1,p2}now not |[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))assume
|[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))
;
contradictionthen
|[1,1]| in LSeg (
p1,
p2)
by XBOOLE_0:def 4;
then
|[1,1]| `2 <= p2 `2
by A13, A151, A156, TOPREAL1:4;
then
p2 `2 = 1
by A151, A153, Lm11, XXREAL_0:1;
hence
contradiction
by A151, A152, A203, EUCLID:53;
verum end; then
{|[1,1]|} <> (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))
by ZFMISC_1:31;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by A201, TOPREAL1:18, ZFMISC_1:33;
hence
P1 /\ P2 = {p1,p2}
by A198, ENUMSET1:1;
verum end; end; end; hence
P1 /\ P2 = {p1,p2}
;
verum end; suppose A204:
q `2 < p `2
;
ex P1 being Element of K19( the carrier of (TOP-REAL 2)) ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )A205:
(LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) c= {p2}
proof
let a be
object ;
TARSKI:def 3 ( not a in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) or a in {p2} )
assume A206:
a in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2))
;
a in {p2}
then reconsider p =
a as
Point of
(TOP-REAL 2) ;
A207:
p in LSeg (
|[1,0]|,
p2)
by A206, XBOOLE_0:def 4;
|[1,0]| `2 <= p2 `2
by A151, A154, EUCLID:52;
then A208:
p `2 <= p2 `2
by A207, TOPREAL1:4;
A209:
p in LSeg (
p2,
p1)
by A206, XBOOLE_0:def 4;
then A210:
p2 `1 <= p `1
by A13, A14, A151, A152, TOPREAL1:3;
p2 `2 <= p `2
by A13, A151, A204, A209, TOPREAL1:4;
then A211:
p2 `2 = p `2
by A208, XXREAL_0:1;
p `1 <= p1 `1
by A13, A14, A151, A152, A209, TOPREAL1:3;
then
p `1 = 1
by A13, A14, A151, A152, A210, XXREAL_0:1;
then p =
|[1,(p2 `2)]|
by A211, EUCLID:53
.=
p2
by A151, A152, EUCLID:53
;
hence
a in {p2}
by TARSKI:def 1;
verum
end;
|[1,1]| in LSeg (
p1,
|[1,1]|)
by RLTOPSP1:68;
then A212:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) <> {}
by Lm26, XBOOLE_0:def 4;
A213:
now not (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) <> {} set a = the
Element of
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2));
assume A214:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) <> {}
;
contradictionthen reconsider p = the
Element of
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) as
Point of
(TOP-REAL 2) by TARSKI:def 3;
A215:
p in LSeg (
p1,
|[1,1]|)
by A214, XBOOLE_0:def 4;
A216:
p in LSeg (
|[1,0]|,
p2)
by A214, XBOOLE_0:def 4;
|[1,0]| `2 <= p2 `2
by A151, A154, EUCLID:52;
then A217:
p `2 <= p2 `2
by A216, TOPREAL1:4;
p1 `2 <= |[1,1]| `2
by A13, A15, EUCLID:52;
then
p1 `2 <= p `2
by A215, TOPREAL1:4;
hence
contradiction
by A13, A151, A204, A217, XXREAL_0:2;
verum end; A218:
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[0,0]|,|[1,0]|)) =
((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))
by XBOOLE_1:23
.=
{|[0,0]|}
by Lm2, TOPREAL1:17
;
(LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)) is_an_arc_of |[1,1]|,
|[0,0]|
by Lm6, Lm10, TOPREAL1:9, TOPREAL1:10, TOPREAL1:15;
then A219:
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|)) is_an_arc_of |[1,1]|,
|[1,0]|
by A218, TOPREAL1:10;
now not |[1,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))assume
|[1,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))
;
contradictionthen A220:
|[1,1]| in LSeg (
|[1,0]|,
p2)
by XBOOLE_0:def 4;
|[1,0]| `2 <= p2 `2
by A151, A154, EUCLID:52;
then
|[1,1]| `2 <= p2 `2
by A220, TOPREAL1:4;
hence
contradiction
by A15, A151, A153, A204, Lm11, XXREAL_0:1;
verum end; then A221:
{|[1,1]|} <> (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))
by ZFMISC_1:31;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[1,1]|}
by A148, Lm25, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
then A222:
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) = {}
by A221, ZFMISC_1:33;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
then A223:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by A5, XBOOLE_1:3, XBOOLE_1:26;
now not |[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))assume
|[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
;
contradictionthen A224:
|[1,0]| in LSeg (
p1,
|[1,1]|)
by XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2
by A13, A15, EUCLID:52;
hence
contradiction
by A13, A154, A204, A224, Lm9, TOPREAL1:4;
verum end; then A225:
{|[1,0]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by ZFMISC_1:31;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A3, Lm27, TOPREAL1:6, XBOOLE_1:26;
then A226:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by A225, TOPREAL1:16, ZFMISC_1:33;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
then A227:
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {}
by A150, XBOOLE_1:3, XBOOLE_1:26;
A228:
(LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) c= {p1}
proof
let a be
object ;
TARSKI:def 3 ( not a in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) or a in {p1} )
assume A229:
a in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|))
;
a in {p1}
then reconsider p =
a as
Point of
(TOP-REAL 2) ;
A230:
p in LSeg (
p1,
|[1,1]|)
by A229, XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2
by A13, A15, EUCLID:52;
then A231:
p1 `2 <= p `2
by A230, TOPREAL1:4;
A232:
p in LSeg (
p2,
p1)
by A229, XBOOLE_0:def 4;
then A233:
p2 `1 <= p `1
by A13, A14, A151, A152, TOPREAL1:3;
p `2 <= p1 `2
by A13, A151, A204, A232, TOPREAL1:4;
then A234:
p1 `2 = p `2
by A231, XXREAL_0:1;
p `1 <= p1 `1
by A13, A14, A151, A152, A232, TOPREAL1:3;
then
p `1 = 1
by A13, A14, A151, A152, A233, XXREAL_0:1;
then p =
|[1,(p1 `2)]|
by A234, EUCLID:53
.=
p1
by A13, A14, EUCLID:53
;
hence
a in {p1}
by TARSKI:def 1;
verum
end; A235:
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A3, Lm27, TOPREAL1:6, XBOOLE_1:26;
|[1,0]| in LSeg (
|[1,0]|,
p2)
by RLTOPSP1:68;
then A236:
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) <> {}
by Lm24, XBOOLE_0:def 4;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[1,0]|}
by A148, Lm25, TOPREAL1:6, TOPREAL1:16, XBOOLE_1:26;
then A237:
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) = {|[1,0]|}
by A236, ZFMISC_1:33;
take P1 =
LSeg (
p1,
p2);
ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )take P2 =
(LSeg (p1,|[1,1]|)) \/ ((((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2)));
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )A238:
p1 in LSeg (
p1,
|[1,1]|)
by RLTOPSP1:68;
thus
P1 is_an_arc_of p1,
p2
by A1, TOPREAL1:9;
( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )A239:
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {}
by TOPREAL1:20, XBOOLE_0:def 7;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) c= (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))
by A148, Lm25, TOPREAL1:6, XBOOLE_1:26;
then A240:
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) = {}
by A239, XBOOLE_1:3;
(((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) /\ (LSeg (|[1,0]|,p2)) =
(((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)))
by XBOOLE_1:23
.=
(((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)))) \/ {|[1,0]|}
by A237, XBOOLE_1:23
.=
{|[1,0]|}
by A222, A240
;
then A241:
(((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2)) is_an_arc_of |[1,1]|,
p2
by A219, TOPREAL1:10;
(LSeg (p1,|[1,1]|)) /\ ((((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))) =
((LSeg (p1,|[1,1]|)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)))
by XBOOLE_1:23
.=
((LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))
by A213, XBOOLE_1:23
.=
((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))
by A226, XBOOLE_1:23
.=
{|[1,1]|}
by A235, A212, A223, TOPREAL1:18, ZFMISC_1:33
;
hence
P2 is_an_arc_of p1,
p2
by A241, TOPREAL1:11;
( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )thus P1 \/ P2 =
((((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))) \/ ((LSeg (p1,|[1,1]|)) \/ (LSeg (p1,p2)))
by XBOOLE_1:4
.=
(((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[1,0]|,p2)) \/ ((LSeg (p1,p2)) \/ (LSeg (p1,|[1,1]|))))
by XBOOLE_1:4
.=
(((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|))
by A3, A148, TOPREAL1:7
.=
R^2-unit_square
by TOPREAL1:def 2, XBOOLE_1:4
;
P1 /\ P2 = {p1,p2}A242:
p2 in LSeg (
|[1,0]|,
p2)
by RLTOPSP1:68;
p2 in LSeg (
p1,
p2)
by RLTOPSP1:68;
then
p2 in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2))
by A242, XBOOLE_0:def 4;
then
{p2} c= (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2))
by ZFMISC_1:31;
then A243:
(LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) = {p2}
by A205, XBOOLE_0:def 10;
p1 in LSeg (
p1,
p2)
by RLTOPSP1:68;
then
p1 in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|))
by A238, XBOOLE_0:def 4;
then
{p1} c= (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|))
by ZFMISC_1:31;
then
(LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) = {p1}
by A228, XBOOLE_0:def 10;
then A244:
P1 /\ P2 =
{p1} \/ ((LSeg (p1,p2)) /\ ((((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))))
by XBOOLE_1:23
.=
{p1} \/ (((LSeg (p1,p2)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2})
by A243, XBOOLE_1:23
.=
{p1} \/ ((((LSeg (p1,p2)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2})
by XBOOLE_1:23
.=
{p1} \/ (((((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2})
by XBOOLE_1:23
.=
{p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}))
by A227, XBOOLE_1:4
.=
({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by XBOOLE_1:4
;
A245:
(LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))
by A3, A148, TOPREAL1:6, XBOOLE_1:26;
A246:
now P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})per cases
( p1 = |[1,1]| or p1 <> |[1,1]| )
;
suppose A247:
p1 = |[1,1]|
;
P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})then
|[1,1]| in LSeg (
p1,
p2)
by RLTOPSP1:68;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) <> {}
by Lm26, XBOOLE_0:def 4;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {p1}
by A245, A247, TOPREAL1:18, ZFMISC_1:33;
hence
P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by A244;
verum end; suppose A248:
p1 <> |[1,1]|
;
P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})now not |[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))assume
|[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))
;
contradictionthen
|[1,1]| in LSeg (
p2,
p1)
by XBOOLE_0:def 4;
then
|[1,1]| `2 <= p1 `2
by A13, A151, A204, TOPREAL1:4;
then
p1 `2 = 1
by A13, A15, Lm11, XXREAL_0:1;
hence
contradiction
by A13, A14, A248, EUCLID:53;
verum end; then
{|[1,1]|} <> (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))
by ZFMISC_1:31;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {}
by A245, TOPREAL1:18, ZFMISC_1:33;
hence
P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
by A244;
verum end; end; end; A249:
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))
by A3, A148, TOPREAL1:6, XBOOLE_1:26;
now P1 /\ P2 = {p1,p2}per cases
( p2 = |[1,0]| or p2 <> |[1,0]| )
;
suppose A250:
p2 = |[1,0]|
;
P1 /\ P2 = {p1,p2}then
|[1,0]| in LSeg (
p1,
p2)
by RLTOPSP1:68;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) <> {}
by Lm24, XBOOLE_0:def 4;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {p2}
by A249, A250, TOPREAL1:16, ZFMISC_1:33;
hence
P1 /\ P2 = {p1,p2}
by A246, ENUMSET1:1;
verum end; suppose A251:
p2 <> |[1,0]|
;
P1 /\ P2 = {p1,p2}now not |[1,0]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))assume
|[1,0]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))
;
contradictionthen
|[1,0]| in LSeg (
p2,
p1)
by XBOOLE_0:def 4;
then
p2 `2 = 0
by A13, A151, A154, A204, Lm9, TOPREAL1:4;
hence
contradiction
by A151, A152, A251, EUCLID:53;
verum end; then
{|[1,0]|} <> (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))
by ZFMISC_1:31;
then
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {}
by A249, TOPREAL1:16, ZFMISC_1:33;
hence
P1 /\ P2 = {p1,p2}
by A246, ENUMSET1:1;
verum end; end; end; hence
P1 /\ P2 = {p1,p2}
;
verum end; end; 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} )
;
verum end; end;