let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg |[1,0 ]|,|[1,1]| implies ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) )
assume that
A1: p1 <> p2 and
A2: p2 in R^2-unit_square and
A3: p1 in LSeg |[1,0 ]|,|[1,1]| ; :: 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;
A5: LSeg p1,|[1,1]| c= LSeg |[1,0 ]|,|[1,1]| by A3, Lm27, TOPREAL1:12;
|[1,1]| in LSeg p1,|[1,1]| by RLTOPSP1:69;
then A6: {} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by Lm26, XBOOLE_0:def 4;
|[1,0 ]| in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
then A7: {} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by Lm24, XBOOLE_0:def 4;
A8: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, Lm27, TOPREAL1:12, XBOOLE_1:26;
A9: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, Lm25, TOPREAL1:12, XBOOLE_1:26;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A10: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A5, XBOOLE_1:3, XBOOLE_1:26;
A11: LSeg p1,|[1,0 ]| c= LSeg |[1,0 ]|,|[1,1]| by A3, Lm25, TOPREAL1:12;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A12: (LSeg |[1,0 ]|,p1) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A11, XBOOLE_1:3, XBOOLE_1:26;
consider p being Point of (TOP-REAL 2) such that
A13: p = p1 and
A14: p `1 = 1 and
A15: p `2 <= 1 and
A16: p `2 >= 0 by A3, TOPREAL1:19;

per cases ( p2 in LSeg |[0 ,0 ]|,|[0 ,1]| or p2 in LSeg |[0 ,1]|,|[1,1]| or p2 in LSeg |[0 ,0 ]|,|[1,0 ]| or p2 in LSeg |[1,0 ]|,|[1,1]| ) by A4, XBOOLE_0:def 3;

suppose A17: p2 in LSeg |[0 ,0 ]|,|[0 ,1]| ; :: 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} )

|[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
then A18: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} by Lm21, XBOOLE_0:def 4;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A17, Lm20, TOPREAL1:12, XBOOLE_1:26;
then (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|} by A18, TOPREAL1:23, ZFMISC_1:39;
then A19: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,p2) is_an_arc_of |[1,0 ]|,p2 by Lm4, Lm8, TOPREAL1:15, TOPREAL1:16;
A20: LSeg p2,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A17, Lm20, TOPREAL1:12;
then A21: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A11, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A22: LSeg p2,|[0 ,1]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A17, Lm22, TOPREAL1:12;
then A23: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {} by A5, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A24: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A5, A20, XBOOLE_1:3, XBOOLE_1:27;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A25: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {} by A11, A22, XBOOLE_1:3, XBOOLE_1:27;
A26: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A17, TOPREAL1:14;
|[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then A27: |[0 ,1]| in (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) by Lm23, XBOOLE_0:def 4;
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A17, Lm22, TOPREAL1:12, XBOOLE_1:26;
then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {|[0 ,1]|} by A27, TOPREAL1:21, ZFMISC_1:39;
then A28: (LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[1,1]|,p2 by Lm6, Lm10, TOPREAL1:15, TOPREAL1:16;
take P1 = ((LSeg p1,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,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 |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,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} )
A29: (LSeg p1,|[1,1]|) \/ (LSeg p1,|[1,0 ]|) = LSeg |[1,0 ]|,|[1,1]| by A3, TOPREAL1:11;
(LSeg p1,|[1,1]|) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2)) = ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= {|[1,1]|} by A8, A6, A23, TOPREAL1:24, ZFMISC_1:39 ;
then (LSeg p1,|[1,1]|) \/ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2)) is_an_arc_of p1,p2 by A28, 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} )
A30: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 0 & q `2 <= 1 & q `2 >= 0 ) by A17, TOPREAL1:19;
(LSeg p1,|[1,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,p2)) = ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:23
.= {|[1,0 ]|} by A9, A7, A21, TOPREAL1:22, ZFMISC_1:39 ;
then (LSeg p1,|[1,0 ]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,p2)) is_an_arc_of p1,p2 by A19, 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 ]|,p2) \/ (LSeg |[0 ,1]|,p2)) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) by A17, TOPREAL1:11, TOPREAL1:def 4
.= ((LSeg |[0 ,0 ]|,p2) \/ ((LSeg |[0 ,1]|,p2) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) by XBOOLE_1:4
.= ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2)) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:4
.= ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2)) \/ ((LSeg |[1,0 ]|,|[1,1]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:4
.= ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2)) \/ ((LSeg p1,|[1,1]|) \/ ((LSeg p1,|[1,0 ]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,p2)))) by A29, XBOOLE_1:4
.= ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2)) \/ ((LSeg p1,|[1,1]|) \/ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:4
.= ((LSeg p1,|[1,1]|) \/ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2))) \/ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A31: (LSeg p1,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) = {p1} by A3, TOPREAL1:14;
A32: P1 /\ P2 = (((LSeg p1,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2))) \/ ((LSeg |[0 ,1]|,p2) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:23
.= (((LSeg p1,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2}) by A26, XBOOLE_1:23
.= (((LSeg p1,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2))) \/ ((((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2}) by XBOOLE_1:23
.= (((LSeg p1,|[1,1]|) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2))) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A25, XBOOLE_1:23
.= (((LSeg p1,|[1,1]|) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,|[1,1]|) /\ ((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by XBOOLE_1:23
.= (((LSeg p1,|[1,1]|) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,p2))) \/ ((((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by XBOOLE_1:23
.= ((((LSeg p1,|[1,1]|) /\ ((LSeg p1,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by Lm2, XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ (((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A24, A31, XBOOLE_1:23 ;

A33: now

per cases ( p1 = |[1,0 ]| or p1 = |[1,1]| or ( p1 <> |[1,1]| & p1 <> |[1,0 ]| ) ) ;

suppose A34: p1 = |[1,0 ]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2})

then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) = (LSeg |[0 ,1]|,|[1,1]|) /\ {|[1,0 ]|} by RLTOPSP1:71;
then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) = {} by Lm1, Lm17;
hence P1 /\ P2 = ({p1} \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A32, A34, TOPREAL1:22; :: thesis: verum

end;

suppose A35: p1 = |[1,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2})

then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[1,1]|} /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by RLTOPSP1:71;
then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by Lm1, Lm19;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A32, A35, TOPREAL1:24, XBOOLE_1:4
.= ({p1} \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) ;
:: thesis: verum

end;

suppose A36: ( p1 <> |[1,1]| & p1 <> |[1,0 ]| ) ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2})

now

assume |[1,1]| in (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) ; :: thesis: contradiction
then A37: |[1,1]| in LSeg |[1,0 ]|,p1 by XBOOLE_0:def 4;
|[1,0 ]| `2 <= p1 `2 by A13, A16, EUCLID:56;
then |[1,1]| `2 <= p1 `2 by A37, TOPREAL1:10;
then 1 = p1 `2 by A13, A15, Lm11, XXREAL_0:1;
hence contradiction by A13, A14, A36, EUCLID:57; :: thesis: verum

end;

then A38: {|[1,1]|} <> (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) by ZFMISC_1:37;
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) c= {|[1,1]|} by A3, Lm25, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;
then A39: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) = {} by A38, ZFMISC_1:39;

now

assume |[1,0 ]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then A40: |[1,0 ]| in LSeg p1,|[1,1]| by XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2 by A13, A15, EUCLID:56;
then p1 `2 = 0 by A13, A16, A40, Lm9, TOPREAL1:10;
hence contradiction by A13, A14, A36, EUCLID:57; :: thesis: verum

end;

then A41: {|[1,0 ]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, Lm27, TOPREAL1:12, XBOOLE_1:26;
then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A41, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A32, A39; :: thesis: verum

end;

end;

end;

now

per cases ( p2 = |[0 ,0 ]| or p2 = |[0 ,1]| or ( p2 <> |[0 ,1]| & p2 <> |[0 ,0 ]| ) ) ;

suppose A42: p2 = |[0 ,0 ]| ; :: thesis: P1 /\ P2 = {p1,p2}

then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = (LSeg |[0 ,1]|,|[1,1]|) /\ {|[0 ,0 ]|} by RLTOPSP1:71;
then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by Lm1, Lm13;
hence P1 /\ P2 = {p1,p2} by A33, A42, ENUMSET1:41, TOPREAL1:23; :: thesis: verum

end;

suppose A43: p2 = |[0 ,1]| ; :: thesis: P1 /\ P2 = {p1,p2}

then (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[0 ,1]|} /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by RLTOPSP1:71;
then (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by Lm1, Lm14;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A33, A43, TOPREAL1:21, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

suppose A44: ( p2 <> |[0 ,1]| & p2 <> |[0 ,0 ]| ) ; :: thesis: P1 /\ P2 = {p1,p2}

now

assume |[0 ,0 ]| in (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then A45: |[0 ,0 ]| in LSeg p2,|[0 ,1]| by XBOOLE_0:def 4;
p2 `2 <= |[0 ,1]| `2 by A30, EUCLID:56;
then 0 = p2 `2 by A30, A45, Lm5, TOPREAL1:10;
hence contradiction by A30, A44, EUCLID:57; :: thesis: verum

end;

then A46: {|[0 ,0 ]|} <> (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
(LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A17, Lm22, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
then A47: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A46, ZFMISC_1:39;

now

assume |[0 ,1]| in (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) ; :: thesis: contradiction
then A48: |[0 ,1]| in LSeg |[0 ,0 ]|,p2 by XBOOLE_0:def 4;
|[0 ,0 ]| `2 <= p2 `2 by A30, EUCLID:56;
then |[0 ,1]| `2 <= p2 `2 by A48, TOPREAL1:10;
then p2 `2 = 1 by A30, Lm7, XXREAL_0:1;
hence contradiction by A30, A44, EUCLID:57; :: thesis: verum

end;

then A49: {|[0 ,1]|} <> (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A17, Lm20, TOPREAL1:12, XBOOLE_1:26;
then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A49, TOPREAL1:21, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A33, A47, ENUMSET1:41; :: thesis: verum

end;

end;

end;

hence P1 /\ P2 = {p1,p2} ; :: thesis: verum

end;

suppose A50: 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 A51: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) by TOPREAL1:19;

now

A52: |[0 ,1]| `1 <= p2 `1 by A51, EUCLID:56;
assume A53: |[1,1]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) ; :: thesis: contradiction
then A54: |[1,1]| in LSeg |[1,0 ]|,p1 by XBOOLE_0:def 4;
|[1,1]| in LSeg |[0 ,1]|,p2 by A53, XBOOLE_0:def 4;
then |[1,1]| `1 <= p2 `1 by A52, TOPREAL1:9;
then A55: 1 = p2 `1 by A51, Lm10, XXREAL_0:1;
|[1,0 ]| `2 <= p1 `2 by A13, A16, EUCLID:56;
then |[1,1]| `2 <= p1 `2 by A54, TOPREAL1:10;
then 1 = p1 `2 by A13, A15, Lm11, XXREAL_0:1;
then p1 = |[1,1]| by A13, A14, EUCLID:57
.= p2 by A51, A55, EUCLID:57 ;
hence contradiction by A1; :: thesis: verum

end;

then A56: {|[1,1]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
A57: LSeg |[0 ,0 ]|,|[0 ,1]| is_an_arc_of |[0 ,0 ]|,|[0 ,1]| by Lm5, Lm7, TOPREAL1:15;
LSeg |[0 ,0 ]|,|[1,0 ]| is_an_arc_of |[1,0 ]|,|[0 ,0 ]| by Lm4, Lm8, TOPREAL1:15;
then A58: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,0 ]|,|[0 ,1]| by A57, TOPREAL1:5, TOPREAL1:23;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A59: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A5, XBOOLE_1:3, XBOOLE_1:26;
take P1 = (LSeg p1,|[1,1]|) \/ (LSeg |[1,1]|,p2); :: 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 |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,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} )
A60: (LSeg p1,|[1,1]|) \/ (LSeg p1,|[1,0 ]|) = LSeg |[1,0 ]|,|[1,1]| by A3, TOPREAL1:11;
|[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then A61: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} by Lm22, XBOOLE_0:def 4;
A62: |[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
|[1,1]| in LSeg p1,|[1,1]| by RLTOPSP1:69;
then A63: |[1,1]| in (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) by A62, XBOOLE_0:def 4;
A64: LSeg |[1,1]|,p2 c= LSeg |[0 ,1]|,|[1,1]| by A50, Lm26, TOPREAL1:12;
then (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A5, XBOOLE_1:27;
then A65: (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} by A63, TOPREAL1:24, ZFMISC_1:39;
( p1 <> |[1,1]| or |[1,1]| <> p2 ) by A1;
hence P1 is_an_arc_of p1,p2 by A65, TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A66: {p1} = (LSeg p1,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) by A3, TOPREAL1:14;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A67: (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A64, XBOOLE_1:3, XBOOLE_1:26;
A68: LSeg p2,|[0 ,1]| c= LSeg |[0 ,1]|,|[1,1]| by A50, Lm23, TOPREAL1:12;
then A69: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) c= {|[0 ,1]|} by TOPREAL1:21, XBOOLE_1:27;
A70: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by A68, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (LSeg |[0 ,1]|,p2) = ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= {|[0 ,1]|} by A70, A69, A61, ZFMISC_1:39 ;
then A71: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[1,0 ]|,p2 by A58, TOPREAL1:16;
A72: {p2} = (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,1]|,p2) by A50, TOPREAL1:14;
A73: (LSeg |[0 ,1]|,p2) \/ (LSeg |[1,1]|,p2) = LSeg |[0 ,1]|,|[1,1]| by A50, TOPREAL1:11;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A11, A68, XBOOLE_1:27;
then A74: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by A56, TOPREAL1:24, ZFMISC_1:39;
(LSeg p1,|[1,0 ]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)) = ((LSeg p1,|[1,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg |[1,0 ]|,p1) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A74, XBOOLE_1:23
.= {|[1,0 ]|} by A9, A7, A12, TOPREAL1:22, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A71, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg |[1,1]|,p2) \/ ((LSeg p1,|[1,1]|) \/ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by XBOOLE_1:4
.= (LSeg |[1,1]|,p2) \/ ((LSeg |[1,0 ]|,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) by A60, XBOOLE_1:4
.= (LSeg |[1,1]|,p2) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:4
.= (LSeg |[1,1]|,p2) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:4
.= (LSeg |[1,1]|,p2) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,p2))) by XBOOLE_1:4
.= (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,p2)) \/ (LSeg |[1,1]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) by XBOOLE_1:4
.= R^2-unit_square by A73, TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A75: P1 /\ P2 = ((LSeg p1,|[1,1]|) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)))) \/ ((LSeg |[1,1]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by XBOOLE_1:23
.= (((LSeg p1,|[1,1]|) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg p1,|[1,1]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)))) \/ ((LSeg |[1,1]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,1]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)))) \/ ((LSeg |[1,1]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by A66, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)))) \/ ((LSeg |[1,1]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg |[1,1]|,p2) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by A59, XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ (((LSeg |[1,1]|,p2) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2})) by A72, XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ ((((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})) by A67 ;

A76: now

per cases ( p1 = |[1,0 ]| or p1 = |[1,1]| or ( p1 <> |[1,1]| & p1 <> |[1,0 ]| ) ) ;

suppose A77: p1 = |[1,0 ]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})

then A78: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = (LSeg |[1,1]|,p2) /\ {|[1,0 ]|} by RLTOPSP1:71;
not |[1,0 ]| in LSeg |[1,1]|,p2 by A64, Lm7, Lm9, Lm11, TOPREAL1:10;
then A79: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {} by A78, Lm1;
thus P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})) by A75, A77, TOPREAL1:22, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A79 ; :: thesis: verum

end;

suppose A80: p1 = |[1,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})

|[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
then A81: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) <> {} by A80, Lm27, XBOOLE_0:def 4;
(LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) c= {p1} by A64, A80, TOPREAL1:24, XBOOLE_1:27;
then A82: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {p1} by A81, ZFMISC_1:39;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[1,1]|} /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A80, RLTOPSP1:71;
then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by Lm1, Lm19;
hence P1 /\ P2 = ({p1} \/ ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A75, A82, XBOOLE_1:4
.= (({p1} \/ {p1}) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) ;
:: thesis: verum

end;

suppose A83: ( p1 <> |[1,1]| & p1 <> |[1,0 ]| ) ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})

now

assume |[1,1]| in (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) ; :: thesis: contradiction
then A84: |[1,1]| in LSeg |[1,0 ]|,p1 by XBOOLE_0:def 4;
|[1,0 ]| `2 <= p1 `2 by A13, A16, EUCLID:56;
then |[1,1]| `2 <= p1 `2 by A84, TOPREAL1:10;
then 1 = p1 `2 by A13, A15, Lm11, XXREAL_0:1;
hence contradiction by A13, A14, A83, EUCLID:57; :: thesis: verum

end;

then A85: {|[1,1]|} <> (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) by ZFMISC_1:37;
(LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) c= {|[1,1]|} by A11, A64, TOPREAL1:24, XBOOLE_1:27;
then A86: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {} by A85, ZFMISC_1:39;

now

assume |[1,0 ]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then A87: |[1,0 ]| in LSeg p1,|[1,1]| by XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2 by A13, A15, EUCLID:56;
then p1 `2 = 0 by A13, A16, A87, Lm9, TOPREAL1:10;
hence contradiction by A13, A14, A83, EUCLID:57; :: thesis: verum

end;

then A88: {|[1,0 ]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, Lm27, TOPREAL1:12, XBOOLE_1:26;
then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A88, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A75, A86; :: thesis: verum

end;

end;

end;

now

per cases ( p2 = |[0 ,1]| or p2 = |[1,1]| or ( p2 <> |[1,1]| & p2 <> |[0 ,1]| ) ) ;

suppose A89: p2 = |[0 ,1]| ; :: thesis: P1 /\ P2 = {p1,p2}

then A90: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = (LSeg p1,|[1,1]|) /\ {|[0 ,1]|} by RLTOPSP1:71;
not |[0 ,1]| in LSeg p1,|[1,1]| by A5, Lm6, Lm8, Lm10, TOPREAL1:9;
then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {} by A90, Lm1;
hence P1 /\ P2 = {p1,p2} by A76, A89, ENUMSET1:41, TOPREAL1:21; :: thesis: verum

end;

suppose A91: p2 = |[1,1]| ; :: thesis: P1 /\ P2 = {p1,p2}

|[1,1]| in LSeg p1,|[1,1]| by RLTOPSP1:69;
then A92: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} by A91, Lm26, XBOOLE_0:def 4;
(LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {|[1,1]|} /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A91, RLTOPSP1:71;
then A93: (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by Lm1, Lm18;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A5, A68, XBOOLE_1:27;
then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {p2} by A91, A92, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A76, A93, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

suppose A94: ( p2 <> |[1,1]| & p2 <> |[0 ,1]| ) ; :: thesis: P1 /\ P2 = {p1,p2}

now

assume |[0 ,1]| in (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) ; :: thesis: contradiction
then A95: |[0 ,1]| in LSeg p2,|[1,1]| by XBOOLE_0:def 4;
p2 `1 <= |[1,1]| `1 by A51, EUCLID:56;
then p2 `1 = 0 by A51, A95, Lm6, TOPREAL1:9;
hence contradiction by A51, A94, EUCLID:57; :: thesis: verum

end;

then A96: {|[0 ,1]|} <> (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by ZFMISC_1:37;
(LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A50, Lm26, TOPREAL1:12, XBOOLE_1:26;
then A97: (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A96, TOPREAL1:21, ZFMISC_1:39;

now

assume |[1,1]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) ; :: thesis: contradiction
then A98: |[1,1]| in LSeg |[0 ,1]|,p2 by XBOOLE_0:def 4;
|[0 ,1]| `1 <= p2 `1 by A51, EUCLID:56;
then |[1,1]| `1 <= p2 `1 by A98, TOPREAL1:9;
then 1 = p2 `1 by A51, Lm10, XXREAL_0:1;
hence contradiction by A51, A94, EUCLID:57; :: thesis: verum

end;

then A99: {|[1,1]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A5, A68, XBOOLE_1:27;
then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {} by A99, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A76, A97, ENUMSET1:41; :: thesis: verum

end;

end;

end;

hence P1 /\ P2 = {p1,p2} ; :: thesis: verum

end;

suppose A100: 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 A101: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 0 ) by TOPREAL1:19;

now

A102: |[0 ,0 ]| `1 <= p2 `1 by A101, EUCLID:56;
assume A103: |[1,0 ]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) ; :: thesis: contradiction
then A104: |[1,0 ]| in LSeg p1,|[1,1]| by XBOOLE_0:def 4;
|[1,0 ]| in LSeg |[0 ,0 ]|,p2 by A103, XBOOLE_0:def 4;
then |[1,0 ]| `1 <= p2 `1 by A102, TOPREAL1:9;
then A105: 1 = p2 `1 by A101, Lm8, XXREAL_0:1;
p1 `2 <= |[1,1]| `2 by A13, A15, EUCLID:56;
then 0 = p1 `2 by A13, A16, A104, Lm9, TOPREAL1:10;
then p1 = |[1,0 ]| by A13, A14, EUCLID:57;
hence contradiction by A1, A101, A105, EUCLID:57; :: thesis: verum

end;

then A106: {|[1,0 ]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
A107: LSeg |[0 ,0 ]|,|[0 ,1]| is_an_arc_of |[0 ,1]|,|[0 ,0 ]| by Lm5, Lm7, TOPREAL1:15;
LSeg |[0 ,1]|,|[1,1]| is_an_arc_of |[1,1]|,|[0 ,1]| by Lm6, Lm10, TOPREAL1:15;
then A108: (LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by A107, TOPREAL1:5, TOPREAL1:21;
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,|[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 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A109: (LSeg p1,|[1,0 ]|) \/ (LSeg p1,|[1,1]|) = LSeg |[1,0 ]|,|[1,1]| by A3, TOPREAL1:11;
|[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
then A110: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} by Lm20, XBOOLE_0:def 4;
A111: |[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
|[1,0 ]| in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
then A112: (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} by A111, XBOOLE_0:def 4;
A113: LSeg p2,|[1,0 ]| c= LSeg |[0 ,0 ]|,|[1,0 ]| by A100, Lm24, TOPREAL1:12;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A11, XBOOLE_1:27;
then A114: (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} by A112, TOPREAL1:22, ZFMISC_1:39;
( p1 <> |[1,0 ]| or p2 <> |[1,0 ]| ) by A1;
hence P1 is_an_arc_of p1,p2 by A114, TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A115: (LSeg p1,|[1,0 ]|) /\ (LSeg p1,|[1,1]|) = {p1} by A3, TOPREAL1:14;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A116: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A113, XBOOLE_1:3, XBOOLE_1:26;
A117: LSeg p2,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[1,0 ]| by A100, Lm21, TOPREAL1:12;
then A118: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= {|[0 ,0 ]|} by TOPREAL1:23, XBOOLE_1:27;
A119: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A117, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (LSeg |[0 ,0 ]|,p2) = ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:23
.= {|[0 ,0 ]|} by A119, A118, A110, ZFMISC_1:39 ;
then A120: ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2) is_an_arc_of |[1,1]|,p2 by A108, TOPREAL1:16;
A121: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A100, TOPREAL1:14;
A122: (LSeg |[0 ,0 ]|,p2) \/ (LSeg |[1,0 ]|,p2) = LSeg |[0 ,0 ]|,|[1,0 ]| by A100, TOPREAL1:11;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A5, A117, XBOOLE_1:27;
then A123: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A106, TOPREAL1:22, ZFMISC_1:39;
(LSeg p1,|[1,1]|) /\ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)) = ((LSeg p1,|[1,1]|) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A123, XBOOLE_1:23
.= {|[1,1]|} by A8, A6, A10, TOPREAL1:24, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A120, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg |[1,0 ]|,p2) \/ ((LSeg p1,|[1,0 ]|) \/ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by XBOOLE_1:4
.= (LSeg |[1,0 ]|,p2) \/ ((LSeg |[1,0 ]|,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) by A109, XBOOLE_1:4
.= ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2)) \/ (LSeg |[1,0 ]|,p2) by XBOOLE_1:4
.= (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A122, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A124: P1 /\ P2 = ((LSeg p1,|[1,0 ]|) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by XBOOLE_1:23
.= (((LSeg p1,|[1,0 ]|) /\ (LSeg p1,|[1,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by A115, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,0 ]|,p1) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|)) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by A12, XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|)) \/ (((LSeg |[1,0 ]|,p2) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2})) by A121, XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|)) \/ ((((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|)) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})) by A116 ;

A125: now

per cases ( p1 = |[1,0 ]| or p1 = |[1,1]| or ( p1 <> |[1,1]| & p1 <> |[1,0 ]| ) ) ;

suppose A126: p1 = |[1,0 ]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})

|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then A127: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) <> {} by A126, Lm25, XBOOLE_0:def 4;
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) c= {p1} by A113, A126, TOPREAL1:22, XBOOLE_1:27;
then A128: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) = {p1} by A127, ZFMISC_1:39;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {|[1,0 ]|} /\ (LSeg |[0 ,1]|,|[1,1]|) by A126, RLTOPSP1:71;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by Lm1, Lm17;
hence P1 /\ P2 = ({p1} \/ ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A124, A128, XBOOLE_1:4
.= (({p1} \/ {p1}) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) ;
:: thesis: verum

end;

suppose A129: p1 = |[1,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})

then A130: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) = (LSeg |[1,0 ]|,p2) /\ {|[1,1]|} by RLTOPSP1:71;
not |[1,1]| in LSeg |[1,0 ]|,p2 by A113, Lm5, Lm9, Lm11, TOPREAL1:10;
then (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) = {} by A130, Lm1;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A124, A129, TOPREAL1:24, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) ;
:: thesis: verum

end;

suppose A131: ( p1 <> |[1,1]| & p1 <> |[1,0 ]| ) ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})

now

assume |[1,0 ]| in (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) ; :: thesis: contradiction
then A132: |[1,0 ]| in LSeg p1,|[1,1]| by XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2 by A13, A15, EUCLID:56;
then p1 `2 = 0 by A13, A16, A132, Lm9, TOPREAL1:10;
hence contradiction by A13, A14, A131, EUCLID:57; :: thesis: verum

end;

then A133: {|[1,0 ]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) by ZFMISC_1:37;
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) c= {|[1,0 ]|} by A5, A113, TOPREAL1:22, XBOOLE_1:27;
then A134: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) = {} by A133, ZFMISC_1:39;

now

assume |[1,1]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then A135: |[1,1]| in LSeg |[1,0 ]|,p1 by XBOOLE_0:def 4;
|[1,0 ]| `2 <= p1 `2 by A13, A16, EUCLID:56;
then |[1,1]| `2 <= p1 `2 by A135, TOPREAL1:10;
then p1 `2 = 1 by A13, A15, Lm11, XXREAL_0:1;
hence contradiction by A13, A14, A131, EUCLID:57; :: thesis: verum

end;

then A136: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) <> {|[1,1]|} by ZFMISC_1:37;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, Lm25, TOPREAL1:12, XBOOLE_1:26;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A136, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A124, A134; :: thesis: verum

end;

end;

end;

now

per cases ( p2 = |[0 ,0 ]| or p2 = |[1,0 ]| or ( p2 <> |[1,0 ]| & p2 <> |[0 ,0 ]| ) ) ;

suppose A137: p2 = |[0 ,0 ]| ; :: thesis: P1 /\ P2 = {p1,p2}

then A138: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = (LSeg p1,|[1,0 ]|) /\ {|[0 ,0 ]|} by RLTOPSP1:71;
not |[0 ,0 ]| in LSeg p1,|[1,0 ]| by A11, Lm4, Lm8, Lm10, TOPREAL1:9;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A138, Lm1;
hence P1 /\ P2 = {p1,p2} by A125, A137, ENUMSET1:41, TOPREAL1:23; :: thesis: verum

end;

suppose A139: p2 = |[1,0 ]| ; :: thesis: P1 /\ P2 = {p1,p2}

|[1,0 ]| in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
then A140: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} by A139, Lm24, XBOOLE_0:def 4;
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {|[1,0 ]|} /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A139, RLTOPSP1:71;
then A141: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by Lm1, Lm16;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A11, A117, XBOOLE_1:27;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A139, A140, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A125, A141, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

suppose A142: ( p2 <> |[1,0 ]| & p2 <> |[0 ,0 ]| ) ; :: thesis: P1 /\ P2 = {p1,p2}

now

assume |[0 ,0 ]| in (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) ; :: thesis: contradiction
then A143: |[0 ,0 ]| in LSeg p2,|[1,0 ]| by XBOOLE_0:def 4;
p2 `1 <= |[1,0 ]| `1 by A101, EUCLID:56;
then p2 `1 = 0 by A101, A143, Lm4, TOPREAL1:9;
hence contradiction by A101, A142, EUCLID:57; :: thesis: verum

end;

then A144: {|[0 ,0 ]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by ZFMISC_1:37;
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A100, Lm24, TOPREAL1:12, XBOOLE_1:26;
then A145: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A144, TOPREAL1:23, ZFMISC_1:39;

now

assume |[1,0 ]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) ; :: thesis: contradiction
then A146: |[1,0 ]| in LSeg |[0 ,0 ]|,p2 by XBOOLE_0:def 4;
|[0 ,0 ]| `1 <= p2 `1 by A101, EUCLID:56;
then |[1,0 ]| `1 <= p2 `1 by A146, TOPREAL1:9;
then p2 `1 = 1 by A101, Lm8, XXREAL_0:1;
hence contradiction by A101, A142, EUCLID:57; :: thesis: verum

end;

then A147: {|[1,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A11, A117, XBOOLE_1:27;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A147, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A125, A145, ENUMSET1:41; :: thesis: verum

end;

end;

end;

hence P1 /\ P2 = {p1,p2} ; :: thesis: verum

end;

suppose A148: 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} )

A149: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A150: LSeg p1,p2 c= LSeg |[1,0 ]|,|[1,1]| by A3, A148, TOPREAL1:12;
consider q being Point of (TOP-REAL 2) such that
A151: q = p2 and
A152: q `1 = 1 and
A153: q `2 <= 1 and
A154: q `2 >= 0 by A148, TOPREAL1:19;
A155: q = |[(q `1 ),(q `2 )]| by EUCLID:57;

now

per cases ( p `2 < q `2 or q `2 < p `2 ) by A1, A13, A14, A151, A152, A149, A155, XXREAL_0:1;

suppose A156: p `2 < q `2 ; :: 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} )

A157: (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) c= {p2}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) or a in {p2} )
assume A158: a in (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A159: p in LSeg p2,|[1,1]| by A158, XBOOLE_0:def 4;
p2 `2 <= |[1,1]| `2 by A151, A153, EUCLID:56;
then A160: p2 `2 <= p `2 by A159, TOPREAL1:10;
A161: p in LSeg p1,p2 by A158, XBOOLE_0:def 4;
then A162: p1 `1 <= p `1 by A13, A14, A151, A152, TOPREAL1:9;
p `2 <= p2 `2 by A13, A151, A156, A161, TOPREAL1:10;
then A163: p2 `2 = p `2 by A160, XXREAL_0:1;
p `1 <= p2 `1 by A13, A14, A151, A152, A161, TOPREAL1:9;
then p `1 = 1 by A13, A14, A151, A152, A162, XXREAL_0:1;
then p = |[1,(p2 `2 )]| by A163, EUCLID:57
.= p2 by A151, A152, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

|[1,0 ]| in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
then A164: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) <> {} by Lm24, XBOOLE_0:def 4;

A165: now

consider a being Element of (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2);
assume A166: (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) <> {} ; :: thesis: contradiction
then reconsider p = a as Point of (TOP-REAL 2) by TARSKI:def 3;
A167: p in LSeg |[1,0 ]|,p1 by A166, XBOOLE_0:def 4;
A168: p in LSeg p2,|[1,1]| by A166, XBOOLE_0:def 4;
p2 `2 <= |[1,1]| `2 by A151, A153, EUCLID:56;
then A169: p2 `2 <= p `2 by A168, TOPREAL1:10;
|[1,0 ]| `2 <= p1 `2 by A13, A16, EUCLID:56;
then p `2 <= p1 `2 by A167, TOPREAL1:10;
hence contradiction by A13, A151, A156, A169, XXREAL_0:2; :: thesis: verum

end;

A170: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (LSeg |[0 ,1]|,|[1,1]|) = ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) by XBOOLE_1:23
.= {|[0 ,1]|} by Lm2, TOPREAL1:21 ;
(LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,0 ]|,|[0 ,1]| by Lm4, Lm8, TOPREAL1:15, TOPREAL1:16, TOPREAL1:23;
then A171: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[1,0 ]|,|[1,1]| by A170, TOPREAL1:16;

now

assume |[1,1]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then A172: |[1,1]| in LSeg |[1,0 ]|,p1 by XBOOLE_0:def 4;
|[1,0 ]| `2 <= p1 `2 by A13, A16, EUCLID:56;
then |[1,1]| `2 <= p1 `2 by A172, TOPREAL1:10;
hence contradiction by A13, A15, A153, A156, Lm11, XXREAL_0:1; :: thesis: verum

end;

then A173: {|[1,1]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, Lm25, TOPREAL1:12, XBOOLE_1:26;
then A174: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A173, TOPREAL1:24, ZFMISC_1:39;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A175: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A11, XBOOLE_1:3, XBOOLE_1:26;

now

assume |[1,0 ]| in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) ; :: thesis: contradiction
then A176: |[1,0 ]| in LSeg p2,|[1,1]| by XBOOLE_0:def 4;
p2 `2 <= |[1,1]| `2 by A151, A153, EUCLID:56;
hence contradiction by A16, A151, A156, A176, Lm9, TOPREAL1:10; :: thesis: verum

end;

then A177: {|[1,0 ]|} <> (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= {|[1,0 ]|} by A148, Lm27, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
then A178: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A177, ZFMISC_1:39;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A179: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A150, XBOOLE_1:3, XBOOLE_1:26;
A180: (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) c= {p1}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) or a in {p1} )
assume A181: a in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A182: p in LSeg |[1,0 ]|,p1 by A181, XBOOLE_0:def 4;
|[1,0 ]| `2 <= p1 `2 by A13, A16, EUCLID:56;
then A183: p `2 <= p1 `2 by A182, TOPREAL1:10;
A184: p in LSeg p1,p2 by A181, XBOOLE_0:def 4;
then A185: p1 `1 <= p `1 by A13, A14, A151, A152, TOPREAL1:9;
p1 `2 <= p `2 by A13, A151, A156, A184, TOPREAL1:10;
then A186: p1 `2 = p `2 by A183, XXREAL_0:1;
p `1 <= p2 `1 by A13, A14, A151, A152, A184, TOPREAL1:9;
then p `1 = 1 by A13, A14, A151, A152, A185, XXREAL_0:1;
then p = |[1,(p1 `2 )]| by A186, EUCLID:57
.= p1 by A13, A14, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

A187: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, Lm25, TOPREAL1:12, XBOOLE_1:26;
|[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
then A188: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} by Lm26, XBOOLE_0:def 4;
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= {|[1,1]|} by A148, Lm27, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;
then A189: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} by A188, ZFMISC_1:39;
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 |[0 ,0 ]|,|[1,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 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A190: p1 in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
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} )
A191: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by A148, Lm27, TOPREAL1:12, XBOOLE_1:26;
then A192: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {} by A191, XBOOLE_1:3;
(((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (LSeg |[1,1]|,p2) = (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (LSeg |[1,1]|,p2)) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2)) by XBOOLE_1:23
.= (((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2))) \/ {|[1,1]|} by A189, XBOOLE_1:23
.= {|[1,1]|} by A178, A192 ;
then A193: (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2) is_an_arc_of |[1,0 ]|,p2 by A171, TOPREAL1:16;
(LSeg p1,|[1,0 ]|) /\ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)) = ((LSeg p1,|[1,0 ]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[1,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) by A165, XBOOLE_1:23
.= ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A174, XBOOLE_1:23
.= {|[1,0 ]|} by A187, A164, A175, TOPREAL1:22, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A193, TOPREAL1:17; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)) \/ ((LSeg p1,|[1,0 ]|) \/ (LSeg p1,p2)) by XBOOLE_1:4
.= (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (((LSeg |[1,0 ]|,p1) \/ (LSeg p1,p2)) \/ (LSeg p2,|[1,1]|)) by XBOOLE_1:4
.= (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|) by A3, A148, TOPREAL1:13
.= ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ (LSeg |[1,0 ]|,|[1,1]|) by XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A194: p2 in LSeg |[1,1]|,p2 by RLTOPSP1:69;
p2 in LSeg p1,p2 by RLTOPSP1:69;
then p2 in (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) by A194, XBOOLE_0:def 4;
then {p2} c= (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
then A195: (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) = {p2} by A157, XBOOLE_0:def 10;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) by A190, XBOOLE_0:def 4;
then {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) = {p1} by A180, XBOOLE_0:def 10;
then A196: P1 /\ P2 = {p1} \/ ((LSeg p1,p2) /\ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2}) by A195, XBOOLE_1:23
.= {p1} \/ ((((LSeg p1,p2) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})) by A179, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by XBOOLE_1:4 ;
A197: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, A148, TOPREAL1:12, XBOOLE_1:26;

A198: now

per cases ( p1 = |[1,0 ]| or p1 <> |[1,0 ]| ) ;

suppose A199: p1 = |[1,0 ]| ; :: thesis: P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})

then |[1,0 ]| in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) <> {} by Lm24, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p1} by A197, A199, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by A196; :: thesis: verum

end;

suppose A200: p1 <> |[1,0 ]| ; :: thesis: P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})

now

assume |[1,0 ]| in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then |[1,0 ]| in LSeg p1,p2 by XBOOLE_0:def 4;
then p1 `2 = 0 by A13, A16, A151, A156, Lm9, TOPREAL1:10;
hence contradiction by A13, A14, A200, EUCLID:57; :: thesis: verum

end;

then {|[1,0 ]|} <> (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A197, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by A196; :: thesis: verum

end;

end;

end;

A201: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, A148, TOPREAL1:12, XBOOLE_1:26;

now

per cases ( p2 = |[1,1]| or p2 <> |[1,1]| ) ;

suppose A202: p2 = |[1,1]| ; :: thesis: P1 /\ P2 = {p1,p2}

then |[1,1]| in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) <> {} by Lm26, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {p2} by A201, A202, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A198, ENUMSET1:41; :: thesis: verum

end;

suppose A203: p2 <> |[1,1]| ; :: thesis: P1 /\ P2 = {p1,p2}

now

assume |[1,1]| in (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then |[1,1]| in LSeg p1,p2 by XBOOLE_0:def 4;
then |[1,1]| `2 <= p2 `2 by A13, A151, A156, TOPREAL1:10;
then p2 `2 = 1 by A151, A153, Lm11, XXREAL_0:1;
hence contradiction by A151, A152, A203, EUCLID:57; :: thesis: verum

end;

then {|[1,1]|} <> (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A201, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A198, ENUMSET1:41; :: thesis: verum

end;

end;

end;

hence P1 /\ P2 = {p1,p2} ; :: thesis: verum

end;

suppose A204: q `2 < p `2 ; :: 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} )

A205: (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 A206: a in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A207: p in LSeg |[1,0 ]|,p2 by A206, XBOOLE_0:def 4;
|[1,0 ]| `2 <= p2 `2 by A151, A154, EUCLID:56;
then A208: p `2 <= p2 `2 by A207, TOPREAL1:10;
A209: p in LSeg p2,p1 by A206, XBOOLE_0:def 4;
then A210: p2 `1 <= p `1 by A13, A14, A151, A152, TOPREAL1:9;
p2 `2 <= p `2 by A13, A151, A204, A209, TOPREAL1:10;
then A211: p2 `2 = p `2 by A208, XXREAL_0:1;
p `1 <= p1 `1 by A13, A14, A151, A152, A209, TOPREAL1:9;
then p `1 = 1 by A13, A14, A151, A152, A210, XXREAL_0:1;
then p = |[1,(p2 `2 )]| by A211, EUCLID:57
.= p2 by A151, A152, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

|[1,1]| in LSeg p1,|[1,1]| by RLTOPSP1:69;
then A212: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) <> {} by Lm26, XBOOLE_0:def 4;

A213: now

consider a being Element of (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2);
assume A214: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) <> {} ; :: thesis: contradiction
then reconsider p = a as Point of (TOP-REAL 2) by TARSKI:def 3;
A215: p in LSeg p1,|[1,1]| by A214, XBOOLE_0:def 4;
A216: p in LSeg |[1,0 ]|,p2 by A214, XBOOLE_0:def 4;
|[1,0 ]| `2 <= p2 `2 by A151, A154, EUCLID:56;
then A217: p `2 <= p2 `2 by A216, TOPREAL1:10;
p1 `2 <= |[1,1]| `2 by A13, A15, EUCLID:56;
then p1 `2 <= p `2 by A215, TOPREAL1:10;
hence contradiction by A13, A151, A204, A217, XXREAL_0:2; :: thesis: verum

end;

A218: ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) by XBOOLE_1:23
.= {|[0 ,0 ]|} by Lm2, TOPREAL1:23 ;
(LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by Lm6, Lm10, TOPREAL1:15, TOPREAL1:16, TOPREAL1:21;
then A219: ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) is_an_arc_of |[1,1]|,|[1,0 ]| by A218, TOPREAL1:16;

now

assume |[1,1]| in (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) ; :: thesis: contradiction
then A220: |[1,1]| in LSeg |[1,0 ]|,p2 by XBOOLE_0:def 4;
|[1,0 ]| `2 <= p2 `2 by A151, A154, EUCLID:56;
then |[1,1]| `2 <= p2 `2 by A220, TOPREAL1:10;
hence contradiction by A15, A151, A153, A204, Lm11, XXREAL_0:1; :: thesis: verum

end;

then A221: {|[1,1]|} <> (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,1]|} by A148, Lm25, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;
then A222: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A221, ZFMISC_1:39;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A223: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A5, XBOOLE_1:3, XBOOLE_1:26;

now

assume |[1,0 ]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then A224: |[1,0 ]| in LSeg p1,|[1,1]| by XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2 by A13, A15, EUCLID:56;
hence contradiction by A13, A154, A204, A224, Lm9, TOPREAL1:10; :: thesis: verum

end;

then A225: {|[1,0 ]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, Lm27, TOPREAL1:12, XBOOLE_1:26;
then A226: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A225, TOPREAL1:22, ZFMISC_1:39;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A227: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A150, XBOOLE_1:3, XBOOLE_1:26;
A228: (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) c= {p1}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) or a in {p1} )
assume A229: a in (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A230: p in LSeg p1,|[1,1]| by A229, XBOOLE_0:def 4;
p1 `2 <= |[1,1]| `2 by A13, A15, EUCLID:56;
then A231: p1 `2 <= p `2 by A230, TOPREAL1:10;
A232: p in LSeg p2,p1 by A229, XBOOLE_0:def 4;
then A233: p2 `1 <= p `1 by A13, A14, A151, A152, TOPREAL1:9;
p `2 <= p1 `2 by A13, A151, A204, A232, TOPREAL1:10;
then A234: p1 `2 = p `2 by A231, XXREAL_0:1;
p `1 <= p1 `1 by A13, A14, A151, A152, A232, TOPREAL1:9;
then p `1 = 1 by A13, A14, A151, A152, A233, XXREAL_0:1;
then p = |[1,(p1 `2 )]| by A234, EUCLID:57
.= p1 by A13, A14, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

A235: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, Lm27, TOPREAL1:12, XBOOLE_1:26;
|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then A236: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} by Lm24, XBOOLE_0:def 4;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,0 ]|} by A148, Lm25, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
then A237: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} by A236, ZFMISC_1:39;
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,1]|) \/ ((((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (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} )
A238: p1 in LSeg p1,|[1,1]| by RLTOPSP1:69;
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} )
A239: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by A148, Lm25, TOPREAL1:12, XBOOLE_1:26;
then A240: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A239, XBOOLE_1:3;
(((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) /\ (LSeg |[1,0 ]|,p2) = (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (LSeg |[1,0 ]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= (((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2))) \/ {|[1,0 ]|} by A237, XBOOLE_1:23
.= {|[1,0 ]|} by A222, A240 ;
then A241: (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[1,1]|,p2 by A219, TOPREAL1:16;
(LSeg p1,|[1,1]|) /\ ((((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)) = ((LSeg p1,|[1,1]|) /\ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[1,1]|) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) by A213, XBOOLE_1:23
.= ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A226, XBOOLE_1:23
.= {|[1,1]|} by A235, A212, A223, TOPREAL1:24, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A241, TOPREAL1:17; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = ((((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)) \/ ((LSeg p1,|[1,1]|) \/ (LSeg p1,p2)) by XBOOLE_1:4
.= (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg |[1,0 ]|,p2) \/ ((LSeg p1,p2) \/ (LSeg p1,|[1,1]|))) by XBOOLE_1:4
.= (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|) by A3, A148, TOPREAL1:13
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A242: p2 in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
p2 in LSeg p1,p2 by RLTOPSP1:69;
then p2 in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) by A242, XBOOLE_0:def 4;
then {p2} c= (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
then A243: (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) = {p2} by A205, XBOOLE_0:def 10;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) by A238, XBOOLE_0:def 4;
then {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) = {p1} by A228, XBOOLE_0:def 10;
then A244: P1 /\ P2 = {p1} \/ ((LSeg p1,p2) /\ ((((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2))) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2}) by A243, XBOOLE_1:23
.= {p1} \/ ((((LSeg p1,p2) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2})) by A227, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by XBOOLE_1:4 ;
A245: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, A148, TOPREAL1:12, XBOOLE_1:26;

A246: now

per cases ( p1 = |[1,1]| or p1 <> |[1,1]| ) ;

suppose A247: p1 = |[1,1]| ; :: thesis: P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2})

then |[1,1]| in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) <> {} by Lm26, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {p1} by A245, A247, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A244; :: thesis: verum

end;

suppose A248: p1 <> |[1,1]| ; :: thesis: P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2})

now

assume |[1,1]| in (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then |[1,1]| in LSeg p2,p1 by XBOOLE_0:def 4;
then |[1,1]| `2 <= p1 `2 by A13, A151, A204, TOPREAL1:10;
then p1 `2 = 1 by A13, A15, Lm11, XXREAL_0:1;
hence contradiction by A13, A14, A248, EUCLID:57; :: thesis: verum

end;

then {|[1,1]|} <> (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A245, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A244; :: thesis: verum

end;

end;

end;

A249: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, A148, TOPREAL1:12, XBOOLE_1:26;

now

per cases ( p2 = |[1,0 ]| or p2 <> |[1,0 ]| ) ;

suppose A250: p2 = |[1,0 ]| ; :: thesis: P1 /\ P2 = {p1,p2}

then |[1,0 ]| in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) <> {} by Lm24, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p2} by A249, A250, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A246, ENUMSET1:41; :: thesis: verum

end;

suppose A251: p2 <> |[1,0 ]| ; :: thesis: P1 /\ P2 = {p1,p2}

now

assume |[1,0 ]| in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then |[1,0 ]| in LSeg p2,p1 by XBOOLE_0:def 4;
then p2 `2 = 0 by A13, A151, A154, A204, Lm9, TOPREAL1:10;
hence contradiction by A151, A152, A251, EUCLID:57; :: thesis: verum

end;

then {|[1,0 ]|} <> (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A249, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A246, ENUMSET1:41; :: thesis: verum

end;

end;

end;

hence P1 /\ P2 = {p1,p2} ; :: thesis: verum

end;

end;

end;

hence ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ; :: thesis: verum

end;

end;