let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( 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 ]|
; :: thesis: 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 4, XBOOLE_0:def 3;
consider p being Point of (TOP-REAL 2) such that
A5:
p = p1
and
A6:
( p `1 <= 1 & p `1 >= 0 & p `2 = 0 )
by A3, TOPREAL1:19;
A7:
LSeg |[0 ,0 ]|,p1 c= LSeg |[0 ,0 ]|,|[1,0 ]|
by A3, Lm14, TOPREAL1:12;
A8:
LSeg |[1,0 ]|,p1 c= LSeg |[0 ,0 ]|,|[1,0 ]|
by A3, Lm17, TOPREAL1:12;
then
( (LSeg |[1,0 ]|,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A9:
(LSeg |[1,0 ]|,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by XBOOLE_1:3;
|[1,0 ]| in LSeg |[1,0 ]|,p1
by RLTOPSP1:69;
then A10:
( (LSeg |[1,0 ]|,p1) /\ (LSeg |[1,0 ]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) & (LSeg |[1,0 ]|,p1) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {} )
by A8, Lm18, XBOOLE_0:def 4, XBOOLE_1:26;
|[0 ,0 ]| in LSeg p1,|[0 ,0 ]|
by RLTOPSP1:69;
then A11:
( (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & |[0 ,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) )
by A7, Lm13, XBOOLE_0:def 4, XBOOLE_1:26;
A12:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[1,0 ]|) = {p1}
by A3, TOPREAL1:14;
( (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by A7, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A13:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by XBOOLE_1:3;
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 A14:
p2 in LSeg |[0 ,0 ]|,
|[0 ,1]|
;
:: thesis: 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 A15:
ex
q being
Point of
(TOP-REAL 2) st
(
q = p2 &
q `1 = 0 &
q `2 <= 1 &
q `2 >= 0 )
by TOPREAL1:19;
A16:
LSeg |[0 ,0 ]|,
p2 c= LSeg |[0 ,0 ]|,
|[0 ,1]|
by A14, Lm13, TOPREAL1:12;
A17:
LSeg p2,
|[0 ,1]| c= LSeg |[0 ,0 ]|,
|[0 ,1]|
by A14, Lm15, TOPREAL1:12;
take P1 =
(LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,p2);
:: thesis: 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));
:: thesis: ( 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 p1,
|[0 ,0 ]| &
|[0 ,0 ]| in LSeg |[0 ,0 ]|,
p2 )
by RLTOPSP1:69;
then
(
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) &
|[0 ,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) &
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[0 ,0 ]|} )
by A7, A16, TOPREAL1:23, XBOOLE_0:def 4, XBOOLE_1:27;
then
(
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|} & (
p1 <> |[0 ,0 ]| or
|[0 ,0 ]| <> p2 ) )
by A1, ZFMISC_1:39;
hence
P1 is_an_arc_of p1,
p2
by TOPREAL1:18;
:: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
(
LSeg |[1,0 ]|,
|[1,1]| is_an_arc_of |[1,0 ]|,
|[1,1]| &
LSeg |[0 ,1]|,
|[1,1]| is_an_arc_of |[1,1]|,
|[0 ,1]| )
by Lm4, TOPREAL1:15;
then A18:
(LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[1,0 ]|,
|[0 ,1]|
by TOPREAL1:5, TOPREAL1:24;
A19:
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {}
by A17, Lm3, XBOOLE_1:3, XBOOLE_1:26;
|[0 ,1]| in LSeg |[0 ,1]|,
p2
by RLTOPSP1:69;
then A20:
(
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) &
|[0 ,1]| in (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) )
by A17, Lm16, XBOOLE_0:def 4, XBOOLE_1:27;
((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 A19, A20, TOPREAL1:21, ZFMISC_1:39
;
then A21:
((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[1,0 ]|,
p2
by A18, TOPREAL1:16;
A22:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A8, A17, XBOOLE_1:27;
now assume
|[0 ,0 ]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2)
;
:: thesis: contradictionthen
(
|[0 ,0 ]| in LSeg p1,
|[1,0 ]| &
|[0 ,0 ]| in LSeg p2,
|[0 ,1]| &
p1 `1 <= |[1,0 ]| `1 &
p2 `2 <= |[0 ,1]| `2 )
by A5, A6, A15, EUCLID:56, XBOOLE_0:def 4;
then A23:
(
0 = p1 `2 &
0 = p2 `2 &
0 = p1 `1 &
0 = p2 `1 )
by A5, A6, A15, Lm4, TOPREAL1:9, TOPREAL1:10;
then p1 =
|[0 ,0 ]|
by EUCLID:57
.=
p2
by A23, EUCLID:57
;
hence
contradiction
by A1;
:: thesis: verum end; then
{|[0 ,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2)
by ZFMISC_1:37;
then A24:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {}
by A22, TOPREAL1:23, ZFMISC_1:39;
(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 A24, XBOOLE_1:23
.=
{|[1,0 ]|}
by A9, A10, TOPREAL1:22, ZFMISC_1:39
;
hence
P2 is_an_arc_of p1,
p2
by A21, TOPREAL1:17;
:: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )A25:
(LSeg p1,|[0 ,0 ]|) \/ (LSeg p1,|[1,0 ]|) = LSeg |[0 ,0 ]|,
|[1,0 ]|
by A3, TOPREAL1:11;
A26:
(LSeg |[0 ,1]|,p2) \/ (LSeg |[0 ,0 ]|,p2) = LSeg |[0 ,0 ]|,
|[0 ,1]|
by A14, TOPREAL1:11;
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 A25, 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 A26, TOPREAL1:def 4, XBOOLE_1:4
;
:: thesis: P1 /\ P2 = {p1,p2}A27:
{p1} = (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[1,0 ]|)
by A3, TOPREAL1:14;
(
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) &
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by A7, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A28:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by XBOOLE_1:3;
A29:
{p2} = (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,p2)
by A14, TOPREAL1:14;
(
(LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) &
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} )
by A16, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:26;
then A30:
(LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by XBOOLE_1:3;
A31:
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 A27, 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 A28, 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 A29, 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 A30
;
A32:
now per cases
( p1 = |[0 ,0 ]| or p1 = |[1,0 ]| or ( p1 <> |[1,0 ]| & p1 <> |[0 ,0 ]| ) )
;
suppose A33:
p1 = |[0 ,0 ]|
;
:: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})then
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[0 ,0 ]|} /\ (LSeg |[1,0 ]|,|[1,1]|)
by RLTOPSP1:71;
then A34:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by Lm1, Lm5;
(
p1 in LSeg |[0 ,0 ]|,
p2 &
p1 in LSeg p1,
|[1,0 ]| )
by A33, RLTOPSP1:69;
then
(
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) c= {p1} &
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) <> {} )
by A16, A33, TOPREAL1:23, XBOOLE_0:def 4, XBOOLE_1:26;
then
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) = {p1}
by ZFMISC_1:39;
hence P1 /\ P2 =
({p1} \/ ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})
by A31, A34, 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})
;
:: thesis: verum end; suppose A35:
p1 = |[1,0 ]|
;
:: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})then A36:
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) = (LSeg |[0 ,0 ]|,p2) /\ {|[1,0 ]|}
by RLTOPSP1:71;
not
|[1,0 ]| in LSeg |[0 ,0 ]|,
p2
by A16, Lm4, TOPREAL1:9;
then
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) = {}
by A36, 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 A31, A35, TOPREAL1:22, XBOOLE_1:4
.=
({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})
;
:: thesis: verum end; suppose A37:
(
p1 <> |[1,0 ]| &
p1 <> |[0 ,0 ]| )
;
:: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})A38:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|}
by A3, Lm14, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
now assume
|[1,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)
;
:: thesis: contradictionthen
(
|[1,0 ]| in LSeg |[0 ,0 ]|,
p1 &
|[0 ,0 ]| `1 <= p1 `1 )
by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then
|[1,0 ]| `1 <= p1 `1
by TOPREAL1:9;
then
p1 `1 = 1
by A5, A6, Lm4, XXREAL_0:1;
hence
contradiction
by A5, A6, A37, EUCLID:57;
:: thesis: verum end; then
{|[1,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)
by ZFMISC_1:37;
then A39:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by A38, ZFMISC_1:39;
A40:
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) c= {|[0 ,0 ]|}
by A8, A16, TOPREAL1:23, XBOOLE_1:27;
now assume
|[0 ,0 ]| in (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|)
;
:: thesis: contradictionthen
(
|[0 ,0 ]| in LSeg p1,
|[1,0 ]| &
p1 `1 <= |[1,0 ]| `1 )
by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then
0 = p1 `1
by A5, A6, Lm4, TOPREAL1:9;
hence
contradiction
by A5, A6, A37, EUCLID:57;
:: thesis: verum end; then
{|[0 ,0 ]|} <> (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|)
by ZFMISC_1:37;
then
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) = {}
by A40, ZFMISC_1:39;
hence
P1 /\ P2 = ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})
by A31, A39;
:: thesis: verum end; now per cases
( p2 = |[0 ,0 ]| or p2 = |[0 ,1]| or ( p2 <> |[0 ,1]| & p2 <> |[0 ,0 ]| ) )
;
suppose A41:
p2 = |[0 ,0 ]|
;
:: thesis: ( P1 /\ P2 = {p1,p2} & P1 /\ P2 = {p1,p2} )A42:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A7, A17, XBOOLE_1:27;
|[0 ,0 ]| in LSeg p1,
|[0 ,0 ]|
by RLTOPSP1:69;
then
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) <> {}
by A41, Lm13, XBOOLE_0:def 4;
then A43:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {p2}
by A41, A42, TOPREAL1:23, ZFMISC_1:39;
(LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {|[0 ,0 ]|} /\ (LSeg |[0 ,1]|,|[1,1]|)
by A41, RLTOPSP1:71;
then
(LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by Lm1, Lm6;
hence P1 /\ P2 =
{p1} \/ ({p2} \/ {p2})
by A32, A43, XBOOLE_1:4
.=
{p1,p2}
by ENUMSET1:41
;
:: thesis: P1 /\ P2 = {p1,p2}hence
P1 /\ P2 = {p1,p2}
;
:: thesis: verum end; suppose A44:
p2 = |[0 ,1]|
;
:: thesis: ( P1 /\ P2 = {p1,p2} & P1 /\ P2 = {p1,p2} )then A45:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = (LSeg p1,|[0 ,0 ]|) /\ {|[0 ,1]|}
by RLTOPSP1:71;
not
|[0 ,1]| in LSeg p1,
|[0 ,0 ]|
by A7, Lm4, TOPREAL1:10;
then A46:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {}
by A45, Lm1;
hence
P1 /\ P2 = {p1,p2}
by A32, A44, ENUMSET1:41, TOPREAL1:21;
:: thesis: P1 /\ P2 = {p1,p2}thus
P1 /\ P2 = {p1,p2}
by A32, A44, A46, ENUMSET1:41, TOPREAL1:21;
:: thesis: verum end; suppose A47:
(
p2 <> |[0 ,1]| &
p2 <> |[0 ,0 ]| )
;
:: thesis: ( P1 /\ P2 = {p1,p2} & P1 /\ P2 = {p1,p2} )A48:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A7, A17, XBOOLE_1:27;
now assume
|[0 ,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)
;
:: thesis: contradictionthen
(
|[0 ,0 ]| in LSeg p2,
|[0 ,1]| &
p2 `2 <= |[0 ,1]| `2 )
by A15, EUCLID:56, XBOOLE_0:def 4;
then
p2 `2 = 0
by A15, Lm4, TOPREAL1:10;
hence
contradiction
by A15, A47, EUCLID:57;
:: thesis: verum end; then
{|[0 ,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)
by ZFMISC_1:37;
then A49:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {}
by A48, TOPREAL1:23, ZFMISC_1:39;
A50:
(LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|}
by A14, Lm13, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
now assume
|[0 ,1]| in (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)
;
:: thesis: contradictionthen
(
|[0 ,1]| in LSeg |[0 ,0 ]|,
p2 &
|[0 ,0 ]| `2 <= p2 `2 )
by A15, EUCLID:56, XBOOLE_0:def 4;
then
|[0 ,1]| `2 <= p2 `2
by TOPREAL1:10;
then
1
= p2 `2
by A15, Lm4, XXREAL_0:1;
hence
contradiction
by A15, A47, EUCLID:57;
:: thesis: verum end; then
{|[0 ,1]|} <> (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)
by ZFMISC_1:37;
then A51:
(LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by A50, ZFMISC_1:39;
hence
P1 /\ P2 = {p1,p2}
by A32, A49, ENUMSET1:41;
:: thesis: P1 /\ P2 = {p1,p2}thus
P1 /\ P2 = {p1,p2}
by A32, A49, A51, ENUMSET1:41;
:: thesis: verum end; hence
P1 /\ P2 = {p1,p2}
;
:: thesis: verum end; suppose A52:
p2 in LSeg |[0 ,1]|,
|[1,1]|
;
:: thesis: 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 A53:
ex
q being
Point of
(TOP-REAL 2) st
(
q = p2 &
q `1 <= 1 &
q `1 >= 0 &
q `2 = 1 )
by TOPREAL1:19;
take P1 =
((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2);
:: thesis: 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);
:: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )A54:
LSeg p2,
|[0 ,1]| c= LSeg |[0 ,1]|,
|[1,1]|
by A52, Lm16, TOPREAL1:12;
A55:
LSeg p2,
|[1,1]| c= LSeg |[0 ,1]|,
|[1,1]|
by A52, Lm19, TOPREAL1:12;
|[0 ,1]| in LSeg |[0 ,1]|,
p2
by RLTOPSP1:69;
then
(
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) c= {|[0 ,1]|} &
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} )
by A54, Lm15, TOPREAL1:21, XBOOLE_0:def 4, XBOOLE_1:26;
then
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) = {|[0 ,1]|}
by ZFMISC_1:39;
then A56:
(LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[0 ,0 ]|,
p2
by Lm4, TOPREAL1:18;
A57:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {}
by A7, A54, Lm2, XBOOLE_1:3, XBOOLE_1:27;
(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 A11, A57, TOPREAL1:23, ZFMISC_1:39
;
then
(LSeg p1,|[0 ,0 ]|) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,p2)) is_an_arc_of p1,
p2
by A56, TOPREAL1:17;
hence
P1 is_an_arc_of p1,
p2
by XBOOLE_1:4;
:: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
(
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) &
|[1,1]| in LSeg |[1,1]|,
p2 )
by A55, RLTOPSP1:69, XBOOLE_1:26;
then
(
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= {|[1,1]|} &
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} )
by Lm20, TOPREAL1:24, XBOOLE_0:def 4;
then
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|}
by ZFMISC_1:39;
then A58:
(LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,1]|,p2) is_an_arc_of |[1,0 ]|,
p2
by Lm4, TOPREAL1:18;
A59:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {}
by A8, A55, Lm2, XBOOLE_1:3, XBOOLE_1:27;
(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 A10, A59, TOPREAL1:22, ZFMISC_1:39
;
then
(LSeg p1,|[1,0 ]|) \/ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,1]|,p2)) is_an_arc_of p1,
p2
by A58, TOPREAL1:17;
hence
P2 is_an_arc_of p1,
p2
by XBOOLE_1:4;
:: thesis: ( 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 A52, TOPREAL1:11, TOPREAL1:def 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
.=
((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:11
.=
((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
;
:: thesis: P1 /\ P2 = {p1,p2}A60:
(LSeg |[0 ,1]|,p2) /\ (LSeg |[1,1]|,p2) = {p2}
by A52, TOPREAL1:14;
A61:
(LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {}
by A8, A54, Lm2, XBOOLE_1:3, XBOOLE_1:27;
(
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) &
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by A7, A55, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:27;
then A62:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) = {}
by XBOOLE_1:3;
A63:
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 A60, 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 A61, 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 A12, A62, 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
;
A64:
now per cases
( p1 = |[0 ,0 ]| or p1 = |[1,0 ]| or ( p1 <> |[1,0 ]| & p1 <> |[0 ,0 ]| ) )
;
suppose A65:
p1 = |[0 ,0 ]|
;
:: thesis: 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:71;
then
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by Lm1, Lm5;
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 A63, A65, TOPREAL1:23, XBOOLE_1:4
.=
({p1} \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})
;
:: thesis: verum end; suppose A66:
p1 = |[1,0 ]|
;
:: thesis: 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:71;
then
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|) = {}
by Lm1, Lm9;
hence
P1 /\ P2 = ({p1} \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})
by A63, A66, TOPREAL1:22;
:: thesis: verum end; suppose A67:
(
p1 <> |[1,0 ]| &
p1 <> |[0 ,0 ]| )
;
:: thesis: P1 /\ P2 = ({p1} \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})A68:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|}
by A3, Lm14, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
now assume
|[1,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)
;
:: thesis: contradictionthen
(
|[1,0 ]| in LSeg |[0 ,0 ]|,
p1 &
|[0 ,0 ]| `1 <= p1 `1 )
by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then
|[1,0 ]| `1 <= p1 `1
by TOPREAL1:9;
then
1
= p1 `1
by A5, A6, Lm4, XXREAL_0:1;
hence
contradiction
by A5, A6, A67, EUCLID:57;
:: thesis: verum end; then
{|[1,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)
by ZFMISC_1:37;
then A69:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by A68, ZFMISC_1:39;
A70:
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|) c= {|[0 ,0 ]|}
by A3, Lm17, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
now assume
|[0 ,0 ]| in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|)
;
:: thesis: contradictionthen
(
|[0 ,0 ]| in LSeg p1,
|[1,0 ]| &
p1 `1 <= |[1,0 ]| `1 )
by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then
0 = p1 `1
by A5, A6, Lm4, TOPREAL1:9;
hence
contradiction
by A5, A6, A67, EUCLID:57;
:: thesis: verum end; then
{|[0 ,0 ]|} <> (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|)
by ZFMISC_1:37;
then
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|) = {}
by A70, ZFMISC_1:39;
hence
P1 /\ P2 = ({p1} \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})
by A63, A69;
:: thesis: verum end; now per cases
( p2 = |[0 ,1]| or p2 = |[1,1]| or ( p2 <> |[1,1]| & p2 <> |[0 ,1]| ) )
;
suppose A71:
p2 = |[0 ,1]|
;
:: thesis: P1 /\ P2 = {p1,p2}then
(LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[0 ,1]|} /\ (LSeg |[1,0 ]|,|[1,1]|)
by RLTOPSP1:71;
then
(LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by Lm1, Lm8;
hence P1 /\ P2 =
{p1} \/ ({p2} \/ {p2})
by A64, A71, TOPREAL1:21, XBOOLE_1:4
.=
{p1,p2}
by ENUMSET1:41
;
:: thesis: verum end; suppose A72:
p2 = |[1,1]|
;
:: thesis: P1 /\ P2 = {p1,p2}then
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ {|[1,1]|}
by RLTOPSP1:71;
then
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {}
by Lm1, Lm11;
hence
P1 /\ P2 = {p1,p2}
by A64, A72, ENUMSET1:41, TOPREAL1:24;
:: thesis: verum end; suppose A73:
(
p2 <> |[1,1]| &
p2 <> |[0 ,1]| )
;
:: thesis: P1 /\ P2 = {p1,p2}A74:
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) c= {|[0 ,1]|}
by A52, Lm19, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
now assume
|[0 ,1]| in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)
;
:: thesis: contradictionthen
(
|[0 ,1]| in LSeg p2,
|[1,1]| &
p2 `1 <= |[1,1]| `1 )
by A53, EUCLID:56, XBOOLE_0:def 4;
then
p2 `1 = 0
by A53, Lm4, TOPREAL1:9;
hence
contradiction
by A53, A73, EUCLID:57;
:: thesis: verum end; then
{|[0 ,1]|} <> (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)
by ZFMISC_1:37;
then A75:
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {}
by A74, ZFMISC_1:39;
A76:
(LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,1]|}
by A52, Lm16, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;
now assume
|[1,1]| in (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)
;
:: thesis: contradictionthen
(
|[1,1]| in LSeg |[0 ,1]|,
p2 &
|[0 ,1]| `1 <= p2 `1 )
by A53, EUCLID:56, XBOOLE_0:def 4;
then
|[1,1]| `1 <= p2 `1
by TOPREAL1:9;
then
1
= p2 `1
by A53, Lm4, XXREAL_0:1;
hence
contradiction
by A53, A73, EUCLID:57;
:: thesis: verum end; then
{|[1,1]|} <> (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)
by ZFMISC_1:37;
then
(LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by A76, ZFMISC_1:39;
hence
P1 /\ P2 = {p1,p2}
by A64, A75, ENUMSET1:41;
:: thesis: verum end; hence
P1 /\ P2 = {p1,p2}
;
:: thesis: verum end; suppose A77:
p2 in LSeg |[0 ,0 ]|,
|[1,0 ]|
;
:: thesis: 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 consider q being
Point of
(TOP-REAL 2) such that A78:
q = p2
and A79:
(
q `1 <= 1 &
q `1 >= 0 &
q `2 = 0 )
by TOPREAL1:19;
A80:
(
p = |[(p `1 ),(p `2 )]| &
q = |[(q `1 ),(q `2 )]| )
by EUCLID:57;
A81:
LSeg p2,
|[1,0 ]| c= LSeg |[0 ,0 ]|,
|[1,0 ]|
by A77, Lm17, TOPREAL1:12;
A82:
LSeg p2,
|[0 ,0 ]| c= LSeg |[0 ,0 ]|,
|[1,0 ]|
by A77, Lm14, TOPREAL1:12;
A83:
LSeg p1,
p2 c= LSeg |[0 ,0 ]|,
|[1,0 ]|
by A3, A77, TOPREAL1:12;
now per cases
( p `1 < q `1 or q `1 < p `1 )
by A1, A5, A6, A78, A79, A80, XXREAL_0:1;
suppose A84:
p `1 < q `1
;
:: thesis: ex P1 being Element of K21(the carrier of (TOP-REAL 2)) ex P2 being Element of K21(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 P1 =
LSeg p1,
p2;
:: thesis: ex P2 being Element of K21(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));
:: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )thus
P1 is_an_arc_of p1,
p2
by A1, TOPREAL1:15;
:: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )A85:
now assume A86:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {}
;
:: thesis: contradictionconsider a being
Element of
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2);
reconsider p =
a as
Point of
(TOP-REAL 2) by A86, TARSKI:def 3;
(
p in LSeg |[0 ,0 ]|,
p1 &
p in LSeg p2,
|[1,0 ]| &
|[0 ,0 ]| `1 <= p1 `1 &
p2 `1 <= |[1,0 ]| `1 )
by A5, A6, A78, A79, A86, EUCLID:56, XBOOLE_0:def 4;
then
(
p `1 <= p1 `1 &
p2 `1 <= p `1 )
by TOPREAL1:9;
hence
contradiction
by A5, A78, A84, XXREAL_0:2;
:: thesis: verum end; A87:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|}
by A3, Lm14, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
now assume
|[1,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)
;
:: thesis: contradictionthen
(
|[1,0 ]| in LSeg |[0 ,0 ]|,
p1 &
|[0 ,0 ]| `1 <= p1 `1 )
by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then
|[1,0 ]| `1 <= p1 `1
by TOPREAL1:9;
hence
contradiction
by A5, A6, A79, A84, Lm4, XXREAL_0:1;
:: thesis: verum end; then
{|[1,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)
by ZFMISC_1:37;
then A88:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by A87, ZFMISC_1:39;
(
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) &
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by A7, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A89:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by XBOOLE_1:3;
A90:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A3, Lm14, TOPREAL1:12, XBOOLE_1:26;
|[0 ,0 ]| in LSeg p1,
|[0 ,0 ]|
by RLTOPSP1:69;
then A91:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {}
by Lm13, XBOOLE_0:def 4;
A92:
(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 A85, XBOOLE_1:23
.=
((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))
by A88, XBOOLE_1:23
.=
{|[0 ,0 ]|}
by A89, A90, A91, TOPREAL1:23, ZFMISC_1:39
;
A93:
(LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[0 ,0 ]|,
|[1,1]|
by Lm4, TOPREAL1:15, TOPREAL1:16, TOPREAL1:21;
((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:24
;
then A94:
((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[0 ,0 ]|,
|[1,0 ]|
by A93, TOPREAL1:16;
A95:
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)
by A77, Lm17, TOPREAL1:12, XBOOLE_1:26;
|[1,0 ]| in LSeg |[1,0 ]|,
p2
by RLTOPSP1:69;
then
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) <> {}
by Lm18, XBOOLE_0:def 4;
then A96:
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|}
by A95, TOPREAL1:22, ZFMISC_1:39;
A97:
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) c= {|[0 ,0 ]|}
by A77, Lm17, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
now assume
|[0 ,0 ]| in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2)
;
:: thesis: contradictionthen
(
|[0 ,0 ]| in LSeg p2,
|[1,0 ]| &
p2 `1 <= |[1,0 ]| `1 )
by A78, A79, EUCLID:56, XBOOLE_0:def 4;
hence
contradiction
by A6, A78, A84, Lm4, TOPREAL1:9;
:: thesis: verum end; then
{|[0 ,0 ]|} <> (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2)
by ZFMISC_1:37;
then A98:
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {}
by A97, ZFMISC_1:39;
(
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) &
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by A81, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A99:
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {}
by XBOOLE_1:3;
(((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 A96, XBOOLE_1:23
.=
{|[1,0 ]|}
by A98, A99
;
then
(((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 A94, TOPREAL1:16;
hence
P2 is_an_arc_of p1,
p2
by A92, TOPREAL1:17;
:: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )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, A77, TOPREAL1:13
.=
R^2-unit_square
by TOPREAL1:def 4, XBOOLE_1:4
;
:: thesis: P1 /\ P2 = {p1,p2}
(
p1 in LSeg p1,
p2 &
p1 in LSeg p1,
|[0 ,0 ]| )
by RLTOPSP1:69;
then
p1 in (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|)
by XBOOLE_0:def 4;
then A100:
{p1} c= (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|)
by ZFMISC_1:37;
(LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) c= {p1}
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) or a in {p1} )
assume A101:
a in (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|)
;
:: thesis: a in {p1}
then reconsider p =
a as
Point of
(TOP-REAL 2) ;
(
p in LSeg p1,
p2 &
p in LSeg |[0 ,0 ]|,
p1 &
p1 `2 <= p2 `2 &
p1 `1 <= p2 `1 &
|[0 ,0 ]| `1 <= p1 `1 )
by A5, A6, A78, A79, A84, A101, EUCLID:56, XBOOLE_0:def 4;
then
(
p1 `2 <= p `2 &
p `2 <= p2 `2 &
p1 `1 <= p `1 &
p `1 <= p1 `1 )
by TOPREAL1:9, TOPREAL1:10;
then
(
p1 `1 = p `1 &
p `2 = 0 )
by A5, A6, A78, A79, XXREAL_0:1;
then p =
|[(p1 `1 ),0 ]|
by EUCLID:57
.=
p1
by A5, A6, EUCLID:57
;
hence
a in {p1}
by TARSKI:def 1;
:: thesis: verum
end; then A102:
(LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) = {p1}
by A100, XBOOLE_0:def 10;
(
p2 in LSeg p1,
p2 &
p2 in LSeg |[1,0 ]|,
p2 )
by RLTOPSP1:69;
then
p2 in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2)
by XBOOLE_0:def 4;
then A103:
{p2} c= (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2)
by ZFMISC_1:37;
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) c= {p2}
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) or a in {p2} )
assume A104:
a in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2)
;
:: thesis: a in {p2}
then reconsider p =
a as
Point of
(TOP-REAL 2) ;
(
p in LSeg p1,
p2 &
p in LSeg p2,
|[1,0 ]| &
p1 `2 <= p2 `2 &
p1 `1 <= p2 `1 &
p2 `1 <= |[1,0 ]| `1 )
by A5, A6, A78, A79, A84, A104, EUCLID:56, XBOOLE_0:def 4;
then
(
p1 `2 <= p `2 &
p `2 <= p2 `2 &
p2 `1 <= p `1 &
p `1 <= p2 `1 )
by TOPREAL1:9, TOPREAL1:10;
then
(
p2 `1 = p `1 &
p `2 = 0 )
by A5, A6, A78, A79, XXREAL_0:1;
then p =
|[(p2 `1 ),0 ]|
by EUCLID:57
.=
p2
by A78, A79, EUCLID:57
;
hence
a in {p2}
by TARSKI:def 1;
:: thesis: verum
end; then A105:
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) = {p2}
by A103, XBOOLE_0:def 10;
(
(LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) &
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by A83, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A106:
(LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by XBOOLE_1:3;
A107:
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 A102, A105, 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 A106, 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
;
A108:
now per cases
( p1 = |[0 ,0 ]| or p1 <> |[0 ,0 ]| )
;
suppose A109:
p1 = |[0 ,0 ]|
;
:: thesis: P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})A110:
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A3, A77, TOPREAL1:12, XBOOLE_1:26;
p1 in LSeg p1,
p2
by RLTOPSP1:69;
then
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {}
by A109, Lm13, XBOOLE_0:def 4;
then
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {p1}
by A109, A110, TOPREAL1:23, ZFMISC_1:39;
hence
P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})
by A107;
:: thesis: verum end; suppose A111:
p1 <> |[0 ,0 ]|
;
:: thesis: P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})A112:
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A3, A77, TOPREAL1:12, XBOOLE_1:26;
now assume
|[0 ,0 ]| in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
;
:: thesis: contradictionthen
(
|[0 ,0 ]| in LSeg p1,
p2 &
p1 `1 <= p2 `1 )
by A5, A78, A84, XBOOLE_0:def 4;
then
p1 `1 = 0
by A5, A6, Lm4, TOPREAL1:9;
hence
contradiction
by A5, A6, A111, EUCLID:57;
:: thesis: verum end; then
{|[0 ,0 ]|} <> (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by ZFMISC_1:37;
then
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {}
by A112, TOPREAL1:23, ZFMISC_1:39;
hence
P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})
by A107;
:: thesis: verum end; now per cases
( p2 = |[1,0 ]| or p2 <> |[1,0 ]| )
;
suppose A113:
p2 = |[1,0 ]|
;
:: thesis: P1 /\ P2 = {p1,p2}then A114:
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {p2}
by A3, A77, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
p2 in LSeg p1,
p2
by RLTOPSP1:69;
then
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {}
by A113, Lm18, XBOOLE_0:def 4;
then
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {p2}
by A114, ZFMISC_1:39;
hence
P1 /\ P2 = {p1,p2}
by A108, ENUMSET1:41;
:: thesis: verum end; suppose A115:
p2 <> |[1,0 ]|
;
:: thesis: P1 /\ P2 = {p1,p2}A116:
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|}
by A3, A77, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
now assume
|[1,0 ]| in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)
;
:: thesis: contradictionthen
(
|[1,0 ]| in LSeg p1,
p2 &
p1 `1 <= p2 `1 )
by A5, A78, A84, XBOOLE_0:def 4;
then
|[1,0 ]| `1 <= p2 `1
by TOPREAL1:9;
then
p2 `1 = 1
by A78, A79, Lm4, XXREAL_0:1;
hence
contradiction
by A78, A79, A115, EUCLID:57;
:: thesis: verum end; then
{|[1,0 ]|} <> (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)
by ZFMISC_1:37;
then
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by A116, ZFMISC_1:39;
hence
P1 /\ P2 = {p1,p2}
by A108, ENUMSET1:41;
:: thesis: verum end; hence
P1 /\ P2 = {p1,p2}
;
:: thesis: verum end; suppose A117:
q `1 < p `1
;
:: thesis: ex P1 being Element of K21(the carrier of (TOP-REAL 2)) ex P2 being Element of K21(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 P1 =
LSeg p1,
p2;
:: thesis: ex P2 being Element of K21(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));
:: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )thus
P1 is_an_arc_of p1,
p2
by A1, TOPREAL1:15;
:: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )A118:
now assume A119:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {}
;
:: thesis: contradictionconsider a being
Element of
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2);
reconsider p =
a as
Point of
(TOP-REAL 2) by A119, TARSKI:def 3;
(
p in LSeg p1,
|[1,0 ]| &
p in LSeg |[0 ,0 ]|,
p2 &
p1 `1 <= |[1,0 ]| `1 &
|[0 ,0 ]| `1 <= p2 `1 )
by A5, A6, A78, A79, A119, EUCLID:56, XBOOLE_0:def 4;
then
(
p1 `1 <= p `1 &
p `1 <= p2 `1 )
by TOPREAL1:9;
hence
contradiction
by A5, A78, A117, XXREAL_0:2;
:: thesis: verum end; A120:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A3, Lm17, TOPREAL1:12, XBOOLE_1:26;
now assume
|[0 ,0 ]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
;
:: thesis: contradictionthen
(
|[0 ,0 ]| in LSeg p1,
|[1,0 ]| &
p1 `1 <= |[1,0 ]| `1 )
by A5, A6, EUCLID:56, XBOOLE_0:def 4;
hence
contradiction
by A5, A79, A117, Lm4, TOPREAL1:9;
:: thesis: verum end; then
{|[0 ,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by ZFMISC_1:37;
then A121:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {}
by A120, TOPREAL1:23, ZFMISC_1:39;
(
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) &
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by A8, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A122:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by XBOOLE_1:3;
A123:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|}
by A3, Lm17, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
|[1,0 ]| in LSeg p1,
|[1,0 ]|
by RLTOPSP1:69;
then A124:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {}
by Lm18, XBOOLE_0:def 4;
A125:
(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 A118, XBOOLE_1:23
.=
((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))
by A121, XBOOLE_1:23
.=
{|[1,0 ]|}
by A122, A123, A124, ZFMISC_1:39
;
A126:
(LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[1,0 ]|,
|[0 ,1]|
by Lm4, TOPREAL1:15, TOPREAL1:16, TOPREAL1:24;
((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:21
;
then A127:
((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,0 ]|,
|[0 ,0 ]|
by A126, TOPREAL1:16;
A128:
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= {|[0 ,0 ]|}
by A77, Lm14, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
|[0 ,0 ]| in LSeg |[0 ,0 ]|,
p2
by RLTOPSP1:69;
then
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) <> {}
by Lm13, XBOOLE_0:def 4;
then A129:
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|}
by A128, ZFMISC_1:39;
A130:
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)
by A77, Lm14, TOPREAL1:12, XBOOLE_1:26;
now assume
|[1,0 ]| in (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)
;
:: thesis: contradictionthen
(
|[1,0 ]| in LSeg |[0 ,0 ]|,
p2 &
|[0 ,0 ]| `1 <= p2 `1 )
by A78, A79, EUCLID:56, XBOOLE_0:def 4;
then
|[1,0 ]| `1 <= p2 `1
by TOPREAL1:9;
hence
contradiction
by A6, A78, A79, A117, Lm4, XXREAL_0:1;
:: thesis: verum end; then
{|[1,0 ]|} <> (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)
by ZFMISC_1:37;
then A131:
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {}
by A130, TOPREAL1:22, ZFMISC_1:39;
(
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) &
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by A82, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A132:
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {}
by XBOOLE_1:3;
(((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 A129, XBOOLE_1:23
.=
{|[0 ,0 ]|}
by A131, A132
;
then
(((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 A127, TOPREAL1:16;
hence
P2 is_an_arc_of p1,
p2
by A125, TOPREAL1:17;
:: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )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, A77, TOPREAL1:13
.=
(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 4, XBOOLE_1:4
;
:: thesis: P1 /\ P2 = {p1,p2}
(
p1 in LSeg p1,
p2 &
p1 in LSeg p1,
|[1,0 ]| )
by RLTOPSP1:69;
then
p1 in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|)
by XBOOLE_0:def 4;
then A133:
{p1} c= (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|)
by ZFMISC_1:37;
(LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) c= {p1}
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) or a in {p1} )
assume A134:
a in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|)
;
:: thesis: a in {p1}
then reconsider p =
a as
Point of
(TOP-REAL 2) ;
(
p in LSeg p2,
p1 &
p in LSeg p1,
|[1,0 ]| &
p2 `2 <= p1 `2 &
p2 `1 <= p1 `1 &
p1 `1 <= |[1,0 ]| `1 )
by A5, A6, A78, A79, A117, A134, EUCLID:56, XBOOLE_0:def 4;
then
(
p2 `2 <= p `2 &
p `2 <= p1 `2 &
p1 `1 <= p `1 &
p `1 <= p1 `1 )
by TOPREAL1:9, TOPREAL1:10;
then
(
p1 `1 = p `1 &
p `2 = 0 )
by A5, A6, A78, A79, XXREAL_0:1;
then p =
|[(p1 `1 ),0 ]|
by EUCLID:57
.=
p1
by A5, A6, EUCLID:57
;
hence
a in {p1}
by TARSKI:def 1;
:: thesis: verum
end; then A135:
(LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) = {p1}
by A133, XBOOLE_0:def 10;
(
p2 in LSeg p1,
p2 &
p2 in LSeg |[0 ,0 ]|,
p2 )
by RLTOPSP1:69;
then
p2 in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2)
by XBOOLE_0:def 4;
then A136:
{p2} c= (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2)
by ZFMISC_1:37;
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2) c= {p2}
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2) or a in {p2} )
assume A137:
a in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2)
;
:: thesis: a in {p2}
then reconsider p =
a as
Point of
(TOP-REAL 2) ;
(
p in LSeg p2,
p1 &
p in LSeg |[0 ,0 ]|,
p2 &
p2 `1 <= p1 `1 &
p2 `2 <= p1 `2 &
|[0 ,0 ]| `1 <= p2 `1 )
by A5, A6, A78, A79, A117, A137, EUCLID:56, XBOOLE_0:def 4;
then
(
p2 `2 <= p `2 &
p `2 <= p1 `2 &
p2 `1 <= p `1 &
p `1 <= p2 `1 )
by TOPREAL1:9, TOPREAL1:10;
then
(
p2 `1 = p `1 &
p `2 = 0 )
by A5, A6, A78, A79, XXREAL_0:1;
then p =
|[(p2 `1 ),0 ]|
by EUCLID:57
.=
p2
by A78, A79, EUCLID:57
;
hence
a in {p2}
by TARSKI:def 1;
:: thesis: verum
end; then A138:
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2}
by A136, XBOOLE_0:def 10;
(
(LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) &
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} )
by A83, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A139:
(LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by XBOOLE_1:3;
A140:
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 A135, XBOOLE_1:23
.=
{p1} \/ (((LSeg p1,p2) /\ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2})
by A138, 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 A139, 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
;
A141:
now per cases
( p2 = |[0 ,0 ]| or p2 <> |[0 ,0 ]| )
;
suppose A142:
p2 = |[0 ,0 ]|
;
:: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}A143:
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A3, A77, TOPREAL1:12, XBOOLE_1:26;
p2 in LSeg p1,
p2
by RLTOPSP1:69;
then
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {}
by A142, Lm13, XBOOLE_0:def 4;
then
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {p2}
by A142, A143, TOPREAL1:23, ZFMISC_1:39;
hence
P1 /\ P2 = ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}
by A140;
:: thesis: verum end; suppose A144:
p2 <> |[0 ,0 ]|
;
:: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}A145:
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A3, A77, TOPREAL1:12, XBOOLE_1:26;
now assume
|[0 ,0 ]| in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
;
:: thesis: contradictionthen
(
|[0 ,0 ]| in LSeg p2,
p1 &
p2 `1 <= p1 `1 )
by A5, A78, A117, XBOOLE_0:def 4;
then
p2 `1 = 0
by A78, A79, Lm4, TOPREAL1:9;
hence
contradiction
by A78, A79, A144, EUCLID:57;
:: thesis: verum end; then
{|[0 ,0 ]|} <> (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by ZFMISC_1:37;
then
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {}
by A145, TOPREAL1:23, ZFMISC_1:39;
hence
P1 /\ P2 = ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}
by A140;
:: thesis: verum end; now per cases
( p1 = |[1,0 ]| or p1 <> |[1,0 ]| )
;
suppose A146:
p1 = |[1,0 ]|
;
:: thesis: P1 /\ P2 = {p1,p2}then A147:
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {p1}
by A3, A77, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
p1 in LSeg p1,
p2
by RLTOPSP1:69;
then
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {}
by A146, Lm18, XBOOLE_0:def 4;
then
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {p1}
by A147, ZFMISC_1:39;
hence
P1 /\ P2 = {p1,p2}
by A141, ENUMSET1:41;
:: thesis: verum end; suppose A148:
p1 <> |[1,0 ]|
;
:: thesis: P1 /\ P2 = {p1,p2}A149:
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|}
by A3, A77, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
now assume
|[1,0 ]| in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)
;
:: thesis: contradictionthen
(
|[1,0 ]| in LSeg p2,
p1 &
p2 `1 <= p1 `1 )
by A5, A78, A117, XBOOLE_0:def 4;
then
|[1,0 ]| `1 <= p1 `1
by TOPREAL1:9;
then
p1 `1 = 1
by A5, A6, Lm4, XXREAL_0:1;
hence
contradiction
by A5, A6, A148, EUCLID:57;
:: thesis: verum end; then
{|[1,0 ]|} <> (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)
by ZFMISC_1:37;
then
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {}
by A149, ZFMISC_1:39;
hence
P1 /\ P2 = {p1,p2}
by A141, ENUMSET1:41;
:: thesis: verum end; hence
P1 /\ P2 = {p1,p2}
;
:: thesis: 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} )
;
:: thesis: verum end; suppose A150:
p2 in LSeg |[1,0 ]|,
|[1,1]|
;
:: thesis: 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 A151:
ex
q being
Point of
(TOP-REAL 2) st
(
q = p2 &
q `1 = 1 &
q `2 <= 1 &
q `2 >= 0 )
by TOPREAL1:19;
A152:
LSeg p2,
|[1,0 ]| c= LSeg |[1,0 ]|,
|[1,1]|
by A150, Lm18, TOPREAL1:12;
A153:
LSeg p2,
|[1,1]| c= LSeg |[1,0 ]|,
|[1,1]|
by A150, Lm20, TOPREAL1:12;
take P1 =
(LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,p2);
:: thesis: 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));
:: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
(
|[1,0 ]| in LSeg p1,
|[1,0 ]| &
|[1,0 ]| in LSeg |[1,0 ]|,
p2 )
by RLTOPSP1:69;
then
(
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) &
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[1,0 ]|} &
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} )
by A8, A152, TOPREAL1:22, XBOOLE_0:def 4, XBOOLE_1:27;
then
(
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} & (
p1 <> |[1,0 ]| or
p2 <> |[1,0 ]| ) )
by A1, ZFMISC_1:39;
hence
P1 is_an_arc_of p1,
p2
by TOPREAL1:18;
:: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
(
LSeg |[0 ,0 ]|,
|[0 ,1]| is_an_arc_of |[0 ,0 ]|,
|[0 ,1]| &
LSeg |[0 ,1]|,
|[1,1]| is_an_arc_of |[0 ,1]|,
|[1,1]| )
by Lm4, TOPREAL1:15;
then A154:
(LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[0 ,0 ]|,
|[1,1]|
by TOPREAL1:5, TOPREAL1:21;
A155:
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {}
by A153, Lm3, XBOOLE_1:3, XBOOLE_1:26;
|[1,1]| in LSeg |[1,1]|,
p2
by RLTOPSP1:69;
then A156:
(
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= {|[1,1]|} &
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} )
by A153, Lm19, TOPREAL1:24, XBOOLE_0:def 4, XBOOLE_1:27;
((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 A155, A156, ZFMISC_1:39
;
then A157:
((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2) is_an_arc_of |[0 ,0 ]|,
p2
by A154, TOPREAL1:16;
A158:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) c= {|[1,0 ]|}
by A7, A153, TOPREAL1:22, XBOOLE_1:27;
now assume
|[1,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2)
;
:: thesis: contradictionthen
(
|[1,0 ]| in LSeg |[0 ,0 ]|,
p1 &
|[1,0 ]| in LSeg p2,
|[1,1]| &
|[0 ,0 ]| `1 <= p1 `1 &
p2 `2 <= |[1,1]| `2 )
by A5, A6, A151, EUCLID:56, XBOOLE_0:def 4;
then
(
|[1,0 ]| `1 <= p1 `1 &
p2 `2 <= |[1,0 ]| `2 )
by TOPREAL1:9, TOPREAL1:10;
then
(
0 = p1 `2 &
0 = p2 `2 & 1
= p1 `1 & 1
= p2 `1 )
by A5, A6, A151, Lm4, XXREAL_0:1;
then
(
p1 = |[1,0 ]| &
p2 = |[1,0 ]| )
by EUCLID:57;
hence
contradiction
by A1;
:: thesis: verum end; then
{|[1,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2)
by ZFMISC_1:37;
then A159:
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) = {}
by A158, ZFMISC_1:39;
(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 A159, XBOOLE_1:23
.=
{|[0 ,0 ]|}
by A11, A13, TOPREAL1:23, ZFMISC_1:39
;
hence
P2 is_an_arc_of p1,
p2
by A157, TOPREAL1:17;
:: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )A160:
LSeg |[0 ,0 ]|,
|[1,0 ]| = (LSeg p1,|[1,0 ]|) \/ (LSeg p1,|[0 ,0 ]|)
by A3, TOPREAL1:11;
A161:
LSeg |[1,0 ]|,
|[1,1]| = (LSeg |[1,1]|,p2) \/ (LSeg |[1,0 ]|,p2)
by A150, TOPREAL1:11;
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 A160, 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 A161, XBOOLE_1:4
.=
R^2-unit_square
by TOPREAL1:def 4, XBOOLE_1:4
;
:: thesis: P1 /\ P2 = {p1,p2}A162:
(LSeg p1,|[1,0 ]|) /\ (LSeg p1,|[0 ,0 ]|) = {p1}
by A3, TOPREAL1:14;
A163:
(LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) = {p2}
by A150, TOPREAL1:14;
(
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) &
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} )
by A152, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:26;
then A164:
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {}
by XBOOLE_1:3;
A165:
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 A162, 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 A9, 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 A163, 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 A164
;
A166:
now per cases
( p1 = |[0 ,0 ]| or p1 = |[1,0 ]| or ( p1 <> |[1,0 ]| & p1 <> |[0 ,0 ]| ) )
;
suppose A167:
p1 = |[0 ,0 ]|
;
:: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})then A168:
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = (LSeg |[1,0 ]|,p2) /\ {|[0 ,0 ]|}
by RLTOPSP1:71;
not
|[0 ,0 ]| in LSeg |[1,0 ]|,
p2
by A152, Lm4, TOPREAL1:9;
then
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = {}
by A168, 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 A165, A167, TOPREAL1:23, XBOOLE_1:4
.=
({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})
;
:: thesis: verum end; suppose A169:
p1 = |[1,0 ]|
;
:: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})then
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {|[1,0 ]|} /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by RLTOPSP1:71;
then A170:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {}
by Lm1, Lm9;
A171:
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)
by A7, A152, XBOOLE_1:27;
(
p1 in LSeg |[1,0 ]|,
p2 &
p1 in LSeg p1,
|[0 ,0 ]| )
by A169, RLTOPSP1:69;
then
{} <> (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|)
by XBOOLE_0:def 4;
then
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = {p1}
by A169, A171, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 =
({p1} \/ ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})
by A165, A170, 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})
;
:: thesis: verum end; suppose A172:
(
p1 <> |[1,0 ]| &
p1 <> |[0 ,0 ]| )
;
:: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})A173:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by A3, Lm17, TOPREAL1:12, XBOOLE_1:26;
now assume
|[0 ,0 ]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
;
:: thesis: contradictionthen
(
|[0 ,0 ]| in LSeg p1,
|[1,0 ]| &
p1 `1 <= |[1,0 ]| `1 )
by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then
p1 `1 = 0
by A5, A6, Lm4, TOPREAL1:9;
hence
contradiction
by A5, A6, A172, EUCLID:57;
:: thesis: verum end; then
{|[0 ,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)
by ZFMISC_1:37;
then A174:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {}
by A173, TOPREAL1:23, ZFMISC_1:39;
A175:
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)
by A7, A152, XBOOLE_1:27;
now assume
|[1,0 ]| in (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|)
;
:: thesis: contradictionthen
(
|[1,0 ]| in LSeg |[0 ,0 ]|,
p1 &
|[0 ,0 ]| `1 <= p1 `1 )
by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then
|[1,0 ]| `1 <= p1 `1
by TOPREAL1:9;
then
p1 `1 = 1
by A5, A6, Lm4, XXREAL_0:1;
hence
contradiction
by A5, A6, A172, EUCLID:57;
:: thesis: verum end; then
{|[1,0 ]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|)
by ZFMISC_1:37;
then
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = {}
by A175, TOPREAL1:22, ZFMISC_1:39;
hence
P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})
by A165, A174;
:: thesis: verum end; now per cases
( p2 = |[1,0 ]| or p2 = |[1,1]| or ( p2 <> |[1,1]| & p2 <> |[1,0 ]| ) )
;
suppose A176:
p2 = |[1,0 ]|
;
:: thesis: P1 /\ P2 = {p1,p2}then A177:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= {p2}
by A8, TOPREAL1:22, XBOOLE_1:27;
|[1,0 ]| in LSeg p1,
|[1,0 ]|
by RLTOPSP1:69;
then
{} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)
by A176, Lm18, XBOOLE_0:def 4;
then A178:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {p2}
by A177, ZFMISC_1:39;
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {|[1,0 ]|} /\ (LSeg |[0 ,1]|,|[1,1]|)
by A176, RLTOPSP1:71;
then
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by Lm1, Lm10;
hence P1 /\ P2 =
{p1} \/ ({p2} \/ {p2})
by A166, A178, XBOOLE_1:4
.=
{p1,p2}
by ENUMSET1:41
;
:: thesis: verum end; suppose A179:
p2 = |[1,1]|
;
:: thesis: P1 /\ P2 = {p1,p2}then A180:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = (LSeg p1,|[1,0 ]|) /\ {|[1,1]|}
by RLTOPSP1:71;
not
|[1,1]| in LSeg p1,
|[1,0 ]|
by A8, Lm4, TOPREAL1:10;
then
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {}
by A180, Lm1;
hence
P1 /\ P2 = {p1,p2}
by A166, A179, ENUMSET1:41, TOPREAL1:24;
:: thesis: verum end; suppose A181:
(
p2 <> |[1,1]| &
p2 <> |[1,0 ]| )
;
:: thesis: P1 /\ P2 = {p1,p2}A182:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= {|[1,0 ]|}
by A8, A153, TOPREAL1:22, XBOOLE_1:27;
now assume
|[1,0 ]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)
;
:: thesis: contradictionthen
(
|[1,0 ]| in LSeg p2,
|[1,1]| &
p2 `2 <= |[1,1]| `2 )
by A151, EUCLID:56, XBOOLE_0:def 4;
then
p2 `2 = 0
by A151, Lm4, TOPREAL1:10;
hence
contradiction
by A151, A181, EUCLID:57;
:: thesis: verum end; then
{|[1,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)
by ZFMISC_1:37;
then A183:
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {}
by A182, ZFMISC_1:39;
A184:
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|)
by A150, Lm18, TOPREAL1:12, XBOOLE_1:26;
now assume
|[1,1]| in (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)
;
:: thesis: contradictionthen
(
|[1,1]| in LSeg |[1,0 ]|,
p2 &
|[1,0 ]| `2 <= p2 `2 )
by A151, EUCLID:56, XBOOLE_0:def 4;
then
|[1,1]| `2 <= p2 `2
by TOPREAL1:10;
then
1
= p2 `2
by A151, Lm4, XXREAL_0:1;
hence
contradiction
by A151, A181, EUCLID:57;
:: thesis: verum end; then
{|[1,1]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)
by ZFMISC_1:37;
then
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {}
by A184, TOPREAL1:24, ZFMISC_1:39;
hence
P1 /\ P2 = {p1,p2}
by A166, A183, ENUMSET1:41;
:: thesis: verum end; hence
P1 /\ P2 = {p1,p2}
;
:: thesis: verum end;