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