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;
A5: (LSeg |[1,0 ]|,p1) /\ (LSeg |[1,0 ]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by A3, Lm24, TOPREAL1:12, XBOOLE_1:26;
|[0 ,0 ]| in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
then A6: |[0 ,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by Lm20, XBOOLE_0:def 4;
|[1,0 ]| in LSeg |[1,0 ]|,p1 by RLTOPSP1:69;
then A7: (LSeg |[1,0 ]|,p1) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {} by Lm25, XBOOLE_0:def 4;
A8: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, Lm21, TOPREAL1:12, XBOOLE_1:26;
A9: (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[1,0 ]|) = {p1} by A3, TOPREAL1:14;
A10: LSeg |[0 ,0 ]|,p1 c= LSeg |[0 ,0 ]|,|[1,0 ]| by A3, Lm21, TOPREAL1:12;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A11: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A10, XBOOLE_1:3, XBOOLE_1:26;
A12: LSeg |[1,0 ]|,p1 c= LSeg |[0 ,0 ]|,|[1,0 ]| by A3, Lm24, TOPREAL1:12;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A13: (LSeg |[1,0 ]|,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A12, XBOOLE_1:3, XBOOLE_1:26;
consider p being Point of (TOP-REAL 2) such that
A14: p = p1 and
A15: p `1 <= 1 and
A16: p `1 >= 0 and
A17: p `2 = 0 by A3, TOPREAL1: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 A18: 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} )

A19: LSeg |[0 ,1]|,|[1,1]| is_an_arc_of |[1,1]|,|[0 ,1]| by Lm6, Lm10, TOPREAL1:15;
LSeg |[1,0 ]|,|[1,1]| is_an_arc_of |[1,0 ]|,|[1,1]| by Lm9, Lm11, TOPREAL1:15;
then A20: (LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[1,0 ]|,|[0 ,1]| by A19, TOPREAL1:5, TOPREAL1:24;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A21: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A10, XBOOLE_1:3, XBOOLE_1:26;
take P1 = (LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,p2); :: 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} )
A22: (LSeg p1,|[0 ,0 ]|) \/ (LSeg p1,|[1,0 ]|) = LSeg |[0 ,0 ]|,|[1,0 ]| by A3, TOPREAL1:11;
|[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then A23: |[0 ,1]| in (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) by Lm23, XBOOLE_0:def 4;
A24: |[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
|[0 ,0 ]| in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
then A25: |[0 ,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) by A24, XBOOLE_0:def 4;
A26: LSeg |[0 ,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A18, Lm20, TOPREAL1:12;
then (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A10, XBOOLE_1:27;
then A27: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|} by A25, TOPREAL1:23, ZFMISC_1:39;
A28: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 0 & q `2 <= 1 & q `2 >= 0 ) by A18, TOPREAL1:19;

now

A29: p2 `2 <= |[0 ,1]| `2 by A28, EUCLID:56;
assume A30: |[0 ,0 ]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) ; :: thesis: contradiction
then A31: |[0 ,0 ]| in LSeg p1,|[1,0 ]| by XBOOLE_0:def 4;
|[0 ,0 ]| in LSeg p2,|[0 ,1]| by A30, XBOOLE_0:def 4;
then A32: 0 = p2 `2 by A28, A29, Lm5, TOPREAL1:10;
p1 `1 <= |[1,0 ]| `1 by A14, A15, EUCLID:56;
then 0 = p1 `1 by A14, A16, A31, Lm4, TOPREAL1:9;
then p1 = |[0 ,0 ]| by A14, A17, EUCLID:57
.= p2 by A28, A32, EUCLID:57 ;
hence contradiction by A1; :: thesis: verum

end;

then A33: {|[0 ,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
( p1 <> |[0 ,0 ]| or |[0 ,0 ]| <> p2 ) by A1;
hence P1 is_an_arc_of p1,p2 by A27, TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A34: {p1} = (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[1,0 ]|) by A3, TOPREAL1:14;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A35: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A26, XBOOLE_1:3, XBOOLE_1:26;
A36: LSeg p2,|[0 ,1]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A18, Lm22, TOPREAL1:12;
then A37: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by XBOOLE_1:27;
A38: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {} by A36, Lm3, XBOOLE_1:3, XBOOLE_1:26;
((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (LSeg |[0 ,1]|,p2) = ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= {|[0 ,1]|} by A38, A37, A23, TOPREAL1:21, ZFMISC_1:39 ;
then A39: ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[1,0 ]|,p2 by A20, TOPREAL1:16;
A40: {p2} = (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,p2) by A18, TOPREAL1:14;
A41: (LSeg |[0 ,1]|,p2) \/ (LSeg |[0 ,0 ]|,p2) = LSeg |[0 ,0 ]|,|[0 ,1]| by A18, TOPREAL1:11;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A12, A36, XBOOLE_1:27;
then A42: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by A33, TOPREAL1: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 A42, XBOOLE_1:23
.= {|[1,0 ]|} by A13, A5, A7, TOPREAL1:22, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A39, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg |[0 ,0 ]|,p2) \/ ((LSeg p1,|[0 ,0 ]|) \/ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by XBOOLE_1:4
.= (LSeg |[0 ,0 ]|,p2) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2))) by A22, XBOOLE_1:4
.= (LSeg |[0 ,0 ]|,p2) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:4
.= (LSeg |[0 ,0 ]|,p2) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:4
.= (LSeg |[0 ,0 ]|,p2) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2))) by XBOOLE_1:4
.= (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2)) \/ (LSeg |[0 ,0 ]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) by XBOOLE_1:4
.= R^2-unit_square by A41, TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A43: P1 /\ P2 = ((LSeg p1,|[0 ,0 ]|) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2)))) \/ ((LSeg |[0 ,0 ]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by XBOOLE_1:23
.= (((LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2)))) \/ ((LSeg |[0 ,0 ]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,0 ]|) /\ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)))) \/ ((LSeg |[0 ,0 ]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by A34, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)))) \/ ((LSeg |[0 ,0 ]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg |[0 ,0 ]|,p2) /\ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,1]|,p2)))) by A21, XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ (((LSeg |[0 ,0 ]|,p2) /\ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2})) by A40, XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ ((((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})) by A35 ;

A44: now

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

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

A46: p1 in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
p1 in LSeg |[0 ,0 ]|,p2 by A45, RLTOPSP1:69;
then A47: (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) <> {} by A46, XBOOLE_0:def 4;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[0 ,0 ]|} /\ (LSeg |[1,0 ]|,|[1,1]|) by A45, RLTOPSP1:71;
then A48: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by Lm1, Lm12;
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) c= {p1} by A18, A45, Lm20, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
then (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) = {p1} by A47, 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 A43, A48, XBOOLE_1:4
.= (({p1} \/ {p1}) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) ;
:: thesis: verum

end;

suppose A49: 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 A50: (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 A26, Lm4, Lm6, Lm8, TOPREAL1:9;
then (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) = {} by A50, Lm1;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by A43, A49, TOPREAL1: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 A51: ( 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})

now

assume |[0 ,0 ]| in (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) ; :: thesis: contradiction
then A52: |[0 ,0 ]| in LSeg p1,|[1,0 ]| by XBOOLE_0:def 4;
p1 `1 <= |[1,0 ]| `1 by A14, A15, EUCLID:56;
then 0 = p1 `1 by A14, A16, A52, Lm4, TOPREAL1:9;
hence contradiction by A14, A17, A51, EUCLID:57; :: thesis: verum

end;

then A53: {|[0 ,0 ]|} <> (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) c= {|[0 ,0 ]|} by A12, A26, TOPREAL1:23, XBOOLE_1:27;
then A54: (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[1,0 ]|) = {} by A53, ZFMISC_1:39;

now

assume |[1,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: contradiction
then A55: |[1,0 ]| in LSeg |[0 ,0 ]|,p1 by XBOOLE_0:def 4;
|[0 ,0 ]| `1 <= p1 `1 by A14, A16, EUCLID:56;
then |[1,0 ]| `1 <= p1 `1 by A55, TOPREAL1:9;
then p1 `1 = 1 by A14, A15, Lm8, XXREAL_0:1;
hence contradiction by A14, A17, A51, EUCLID:57; :: thesis: verum

end;

then A56: {|[1,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|} by A3, Lm21, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
then (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A56, 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 A43, A54; :: thesis: verum

end;

end;

end;

now

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

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

|[0 ,0 ]| in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
then A58: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) <> {} by A57, Lm20, XBOOLE_0:def 4;
(LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {|[0 ,0 ]|} /\ (LSeg |[0 ,1]|,|[1,1]|) by A57, RLTOPSP1:71;
then A59: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by Lm1, Lm13;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A10, A36, XBOOLE_1:27;
then (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {p2} by A57, A58, TOPREAL1:23, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A44, A59, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: P1 /\ P2 = {p1,p2}
hence P1 /\ P2 = {p1,p2} ; :: thesis: verum

end;

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

then A61: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = (LSeg p1,|[0 ,0 ]|) /\ {|[0 ,1]|} by RLTOPSP1:71;
not |[0 ,1]| in LSeg p1,|[0 ,0 ]| by A10, Lm5, Lm7, Lm9, TOPREAL1:10;
then A62: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by A61, Lm1;
hence P1 /\ P2 = {p1,p2} by A44, A60, ENUMSET1:41, TOPREAL1:21; :: thesis: P1 /\ P2 = {p1,p2}
thus P1 /\ P2 = {p1,p2} by A44, A60, A62, ENUMSET1:41, TOPREAL1:21; :: thesis: verum

end;

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

now

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

end;

then A65: {|[0 ,1]|} <> (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A18, Lm20, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
then A66: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A65, ZFMISC_1:39;

now

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

end;

then A68: {|[0 ,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A10, A36, XBOOLE_1:27;
then A69: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by A68, TOPREAL1:23, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A44, A66, ENUMSET1:41; :: thesis: P1 /\ P2 = {p1,p2}
thus P1 /\ P2 = {p1,p2} by A44, A69, A66, ENUMSET1:41; :: thesis: verum

end;

end;

end;

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

end;

suppose A70: 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 A71: LSeg p2,|[1,1]| c= LSeg |[0 ,1]|,|[1,1]| by Lm26, TOPREAL1:12;
then A72: (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A12, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A73: LSeg p2,|[0 ,1]| c= LSeg |[0 ,1]|,|[1,1]| by A70, Lm23, TOPREAL1:12;
then A74: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by A10, Lm2, XBOOLE_1:3, XBOOLE_1:27;
take P1 = ((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2); :: 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} )
|[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then A75: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} by Lm22, XBOOLE_0:def 4;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) c= {|[0 ,1]|} by A70, Lm23, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
then (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) = {|[0 ,1]|} by A75, ZFMISC_1:39;
then A76: (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[0 ,0 ]|,p2 by Lm5, Lm7, TOPREAL1:18;
(LSeg p1,|[0 ,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,p2)) = ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= {|[0 ,0 ]|} by A8, A6, A74, TOPREAL1: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 A76, 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} )
|[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
then A77: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} by Lm27, XBOOLE_0:def 4;
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A70, Lm26, TOPREAL1:12, XBOOLE_1:26;
then (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} by A77, TOPREAL1:24, ZFMISC_1:39;
then A78: (LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,1]|,p2) is_an_arc_of |[1,0 ]|,p2 by Lm9, Lm11, TOPREAL1:18;
(LSeg p1,|[1,0 ]|) /\ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,1]|,p2)) = ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)) by XBOOLE_1:23
.= {|[1,0 ]|} by A5, A7, A72, TOPREAL1: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 A78, 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 A70, 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}
A79: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) by A70, TOPREAL1:19;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A80: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A10, A71, XBOOLE_1:3, XBOOLE_1:27;
A81: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {} by A12, A73, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A82: (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,1]|,p2) = {p2} by A70, TOPREAL1:14;
A83: P1 /\ P2 = (((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) \/ ((LSeg |[0 ,1]|,p2) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by XBOOLE_1:23
.= (((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}) by A82, XBOOLE_1:23
.= (((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) \/ ((((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= (((LSeg p1,|[0 ,0 ]|) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by A81, XBOOLE_1:23
.= ((((LSeg p1,|[0 ,0 ]|) /\ ((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by A9, A80, XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ ((LSeg p1,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by Lm3 ;

A84: now

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

suppose A85: 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, Lm12;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by A83, A85, TOPREAL1: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 A86: 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, Lm16;
hence P1 /\ P2 = ({p1} \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by A83, A86, TOPREAL1:22; :: thesis: verum

end;

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

now

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

end;

then A89: {|[0 ,0 ]|} <> (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|) by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|) c= {|[0 ,0 ]|} by A3, Lm24, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
then A90: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg p1,|[1,0 ]|) = {} by A89, ZFMISC_1:39;

now

assume |[1,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: contradiction
then A91: |[1,0 ]| in LSeg |[0 ,0 ]|,p1 by XBOOLE_0:def 4;
|[0 ,0 ]| `1 <= p1 `1 by A14, A16, EUCLID:56;
then |[1,0 ]| `1 <= p1 `1 by A91, TOPREAL1:9;
then 1 = p1 `1 by A14, A15, Lm8, XXREAL_0:1;
hence contradiction by A14, A17, A87, EUCLID:57; :: thesis: verum

end;

then A92: {|[1,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|} by A3, Lm21, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
then (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A92, 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 A83, A90; :: thesis: verum

end;

end;

end;

now

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

suppose A93: 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, Lm15;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A84, A93, TOPREAL1:21, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

suppose A94: 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, Lm18;
hence P1 /\ P2 = {p1,p2} by A84, A94, ENUMSET1:41, TOPREAL1:24; :: thesis: verum

end;

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

now

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

end;

then A97: {|[1,1]|} <> (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
(LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,1]|} by A70, Lm23, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;
then A98: (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A97, ZFMISC_1:39;

now

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

end;

then A100: {|[0 ,1]|} <> (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) c= {|[0 ,1]|} by A70, Lm26, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
then (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {} by A100, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A84, A98, ENUMSET1:41; :: thesis: verum

end;

end;

end;

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

end;

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

A102: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A103: LSeg p1,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| by A3, A101, TOPREAL1:12;
consider q being Point of (TOP-REAL 2) such that
A104: q = p2 and
A105: q `1 <= 1 and
A106: q `1 >= 0 and
A107: q `2 = 0 by A101, TOPREAL1:19;
A108: q = |[(q `1 ),(q `2 )]| by EUCLID:57;

now

per cases ( p `1 < q `1 or q `1 < p `1 ) by A1, A14, A17, A104, A107, A102, A108, XXREAL_0:1;

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

now

assume |[1,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: contradiction
then A110: |[1,0 ]| in LSeg |[0 ,0 ]|,p1 by XBOOLE_0:def 4;
|[0 ,0 ]| `1 <= p1 `1 by A14, A16, EUCLID:56;
then |[1,0 ]| `1 <= p1 `1 by A110, TOPREAL1:9;
hence contradiction by A14, A15, A105, A109, Lm8, XXREAL_0:1; :: thesis: verum

end;

then A111: {|[1,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|} by A3, Lm21, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
then A112: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A111, ZFMISC_1:39;
|[0 ,0 ]| in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
then A113: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {} by Lm20, XBOOLE_0:def 4;

now

assume |[0 ,0 ]| in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) ; :: thesis: contradiction
then A114: |[0 ,0 ]| in LSeg p2,|[1,0 ]| by XBOOLE_0:def 4;
p2 `1 <= |[1,0 ]| `1 by A104, A105, EUCLID:56;
hence contradiction by A16, A104, A109, A114, Lm4, TOPREAL1:9; :: thesis: verum

end;

then A115: {|[0 ,0 ]|} <> (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) c= {|[0 ,0 ]|} by A101, Lm24, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
then A116: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A115, ZFMISC_1:39;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A117: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A103, XBOOLE_1:3, XBOOLE_1:26;
A118: (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) c= {p1}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) or a in {p1} )
assume A119: a in (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A120: p in LSeg |[0 ,0 ]|,p1 by A119, XBOOLE_0:def 4;
|[0 ,0 ]| `1 <= p1 `1 by A14, A16, EUCLID:56;
then A121: p `1 <= p1 `1 by A120, TOPREAL1:9;
A122: p in LSeg p1,p2 by A119, XBOOLE_0:def 4;
then p1 `1 <= p `1 by A14, A104, A109, TOPREAL1:9;
then A123: p1 `1 = p `1 by A121, XXREAL_0:1;
p1 `2 <= p `2 by A14, A17, A104, A107, A122, TOPREAL1:10;
then p `2 = 0 by A14, A17, A104, A107, A122, TOPREAL1:10;
then p = |[(p1 `1 ),0 ]| by A123, EUCLID:57
.= p1 by A14, A17, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

A124: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, Lm21, TOPREAL1:12, XBOOLE_1:26;
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} )
A125: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A101, Lm24, TOPREAL1:12, XBOOLE_1:26;
then A126: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A125, XBOOLE_1:3;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:15; :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A127: ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (LSeg |[1,0 ]|,|[1,1]|) = ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) by XBOOLE_1:23
.= {|[1,1]|} by Lm3, TOPREAL1:24 ;
A128: (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 A129: a in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A130: p in LSeg p2,|[1,0 ]| by A129, XBOOLE_0:def 4;
p2 `1 <= |[1,0 ]| `1 by A104, A105, EUCLID:56;
then A131: p2 `1 <= p `1 by A130, TOPREAL1:9;
A132: p in LSeg p1,p2 by A129, XBOOLE_0:def 4;
then p `1 <= p2 `1 by A14, A104, A109, TOPREAL1:9;
then A133: p2 `1 = p `1 by A131, XXREAL_0:1;
p1 `2 <= p `2 by A14, A17, A104, A107, A132, TOPREAL1:10;
then p `2 = 0 by A14, A17, A104, A107, A132, TOPREAL1:10;
then p = |[(p2 `1 ),0 ]| by A133, EUCLID:57
.= p2 by A104, A107, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A134: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A10, XBOOLE_1:3, XBOOLE_1:26;

A135: now

consider a being Element of (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2);
assume A136: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} ; :: thesis: contradiction
then reconsider p = a as Point of (TOP-REAL 2) by TARSKI:def 3;
A137: p in LSeg |[0 ,0 ]|,p1 by A136, XBOOLE_0:def 4;
A138: p in LSeg p2,|[1,0 ]| by A136, XBOOLE_0:def 4;
p2 `1 <= |[1,0 ]| `1 by A104, A105, EUCLID:56;
then A139: p2 `1 <= p `1 by A138, TOPREAL1:9;
|[0 ,0 ]| `1 <= p1 `1 by A14, A16, EUCLID:56;
then p `1 <= p1 `1 by A137, TOPREAL1:9;
hence contradiction by A14, A104, A109, A139, XXREAL_0:2; :: thesis: verum

end;

|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then A140: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) <> {} by Lm25, XBOOLE_0:def 4;
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A101, Lm24, TOPREAL1:12, XBOOLE_1:26;
then A141: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} by A140, TOPREAL1:22, ZFMISC_1:39;
(LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[0 ,0 ]|,|[1,1]| by Lm5, Lm7, TOPREAL1:15, TOPREAL1:16, TOPREAL1:21;
then A142: ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[0 ,0 ]|,|[1,0 ]| by A127, TOPREAL1:16;
(((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) /\ (LSeg |[1,0 ]|,p2) = (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (LSeg |[1,0 ]|,p2)) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= (((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2)) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2))) \/ {|[1,0 ]|} by A141, XBOOLE_1:23
.= {|[1,0 ]|} by A116, A126 ;
then A143: (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[0 ,0 ]|,p2 by A142, TOPREAL1:16;
(LSeg p1,|[0 ,0 ]|) /\ ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)) = ((LSeg p1,|[0 ,0 ]|) /\ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[0 ,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) by A135, XBOOLE_1:23
.= ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) by A112, XBOOLE_1:23
.= {|[0 ,0 ]|} by A134, A124, A113, TOPREAL1:23, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A143, TOPREAL1:17; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A144: p1 in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) by A144, XBOOLE_0:def 4;
then {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) by ZFMISC_1:37;
then A145: (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) = {p1} by A118, XBOOLE_0:def 10;
thus P1 \/ P2 = ((LSeg |[0 ,0 ]|,p1) \/ (LSeg p1,p2)) \/ ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:4
.= (((LSeg |[0 ,0 ]|,p1) \/ (LSeg p1,p2)) \/ (LSeg p2,|[1,0 ]|)) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) by XBOOLE_1:4
.= (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, A101, TOPREAL1:13
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A146: 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 A146, XBOOLE_0:def 4;
then {p2} c= (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
then A147: (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) = {p2} by A128, XBOOLE_0:def 10;
A148: P1 /\ P2 = ((LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ ((LSeg p1,p2) /\ ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2))) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}) by A145, A147, XBOOLE_1:23
.= {p1} \/ ((((LSeg p1,p2) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})) by A117, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by XBOOLE_1:4 ;

A149: now

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

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

p1 in LSeg p1,p2 by RLTOPSP1:69;
then A151: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {} by A150, Lm20, XBOOLE_0:def 4;
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, A101, TOPREAL1:12, XBOOLE_1:26;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {p1} by A150, A151, TOPREAL1:23, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by A148; :: thesis: verum

end;

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

now

assume |[0 ,0 ]| in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) ; :: thesis: contradiction
then |[0 ,0 ]| in LSeg p1,p2 by XBOOLE_0:def 4;
then p1 `1 = 0 by A14, A16, A104, A109, Lm4, TOPREAL1:9;
hence contradiction by A14, A17, A152, EUCLID:57; :: thesis: verum

end;

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

end;

end;

end;

now

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

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

p2 in LSeg p1,p2 by RLTOPSP1:69;
then A155: (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {} by A154, Lm25, XBOOLE_0:def 4;
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {p2} by A3, A101, A154, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
then (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {p2} by A155, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A149, ENUMSET1:41; :: thesis: verum

end;

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

now

assume |[1,0 ]| in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: contradiction
then |[1,0 ]| in LSeg p1,p2 by XBOOLE_0:def 4;
then |[1,0 ]| `1 <= p2 `1 by A14, A104, A109, TOPREAL1:9;
then p2 `1 = 1 by A104, A105, Lm8, XXREAL_0:1;
hence contradiction by A104, A107, A156, EUCLID:57; :: thesis: verum

end;

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

end;

end;

end;

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

end;

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

A159: (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 A160: a in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A161: p in LSeg |[0 ,0 ]|,p2 by A160, XBOOLE_0:def 4;
|[0 ,0 ]| `1 <= p2 `1 by A104, A106, EUCLID:56;
then A162: p `1 <= p2 `1 by A161, TOPREAL1:9;
A163: p in LSeg p2,p1 by A160, XBOOLE_0:def 4;
then p2 `1 <= p `1 by A14, A104, A158, TOPREAL1:9;
then A164: p2 `1 = p `1 by A162, XXREAL_0:1;
p2 `2 <= p `2 by A14, A17, A104, A107, A163, TOPREAL1:10;
then p `2 = 0 by A14, A17, A104, A107, A163, TOPREAL1:10;
then p = |[(p2 `1 ),0 ]| by A164, EUCLID:57
.= p2 by A104, A107, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

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

now

assume |[1,0 ]| in (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) ; :: thesis: contradiction
then A166: |[1,0 ]| in LSeg |[0 ,0 ]|,p2 by XBOOLE_0:def 4;
|[0 ,0 ]| `1 <= p2 `1 by A104, A106, EUCLID:56;
then |[1,0 ]| `1 <= p2 `1 by A166, TOPREAL1:9;
hence contradiction by A15, A104, A105, A158, Lm8, XXREAL_0:1; :: thesis: verum

end;

then A167: {|[1,0 ]|} <> (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A101, Lm21, TOPREAL1:12, XBOOLE_1:26;
then A168: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A167, TOPREAL1:22, ZFMISC_1:39;
A169: ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by XBOOLE_1:23
.= {|[0 ,1]|} by Lm3, TOPREAL1:21 ;
(LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[1,0 ]|,|[0 ,1]| by Lm9, Lm11, TOPREAL1:15, TOPREAL1:16, TOPREAL1:24;
then A170: ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,0 ]|,|[0 ,0 ]| by A169, TOPREAL1:16;

now

assume |[0 ,0 ]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) ; :: thesis: contradiction
then A171: |[0 ,0 ]| in LSeg p1,|[1,0 ]| by XBOOLE_0:def 4;
p1 `1 <= |[1,0 ]| `1 by A14, A15, EUCLID:56;
hence contradiction by A14, A106, A158, A171, Lm4, TOPREAL1:9; :: thesis: verum

end;

then A172: {|[0 ,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by ZFMISC_1:37;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, Lm24, TOPREAL1:12, XBOOLE_1:26;
then A173: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A172, TOPREAL1:23, ZFMISC_1:39;
|[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
then A174: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} by Lm20, XBOOLE_0:def 4;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= {|[0 ,0 ]|} by A101, Lm21, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
then A175: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|} by A174, ZFMISC_1:39;
A176: (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 A177: a in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A178: p in LSeg p1,|[1,0 ]| by A177, XBOOLE_0:def 4;
p1 `1 <= |[1,0 ]| `1 by A14, A15, EUCLID:56;
then A179: p1 `1 <= p `1 by A178, TOPREAL1:9;
A180: p in LSeg p2,p1 by A177, XBOOLE_0:def 4;
then p `1 <= p1 `1 by A14, A104, A158, TOPREAL1:9;
then A181: p1 `1 = p `1 by A179, XXREAL_0:1;
p2 `2 <= p `2 by A14, A17, A104, A107, A180, TOPREAL1:10;
then p `2 = 0 by A14, A17, A104, A107, A180, TOPREAL1:10;
then p = |[(p1 `1 ),0 ]| by A181, EUCLID:57
.= p1 by A14, A17, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A182: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A12, XBOOLE_1:3, XBOOLE_1:26;

A183: now

consider a being Element of (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2);
assume A184: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} ; :: thesis: contradiction
then reconsider p = a as Point of (TOP-REAL 2) by TARSKI:def 3;
A185: p in LSeg p1,|[1,0 ]| by A184, XBOOLE_0:def 4;
A186: p in LSeg |[0 ,0 ]|,p2 by A184, XBOOLE_0:def 4;
|[0 ,0 ]| `1 <= p2 `1 by A104, A106, EUCLID:56;
then A187: p `1 <= p2 `1 by A186, TOPREAL1:9;
p1 `1 <= |[1,0 ]| `1 by A14, A15, EUCLID:56;
then p1 `1 <= p `1 by A185, TOPREAL1:9;
hence contradiction by A14, A104, A158, A187, XXREAL_0:2; :: thesis: verum

end;

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} )
A188: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A101, Lm21, TOPREAL1:12, XBOOLE_1:26;
then A189: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A188, XBOOLE_1:3;
A190: (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|} by A3, Lm24, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
(((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (LSeg |[0 ,0 ]|,p2) = (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (LSeg |[0 ,0 ]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:23
.= (((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ {|[0 ,0 ]|} by A175, XBOOLE_1:23
.= {|[0 ,0 ]|} by A168, A189 ;
then A191: (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2) is_an_arc_of |[1,0 ]|,p2 by A170, TOPREAL1:16;
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} )
A192: p2 in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
(LSeg p1,|[1,0 ]|) /\ ((((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)) = ((LSeg p1,|[1,0 ]|) /\ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[1,0 ]|) /\ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A183, XBOOLE_1:23
.= ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) by A173, XBOOLE_1:23
.= {|[1,0 ]|} by A182, A190, A165, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A191, TOPREAL1:17; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A193: p1 in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
thus P1 \/ P2 = ((LSeg p2,p1) \/ (LSeg p1,|[1,0 ]|)) \/ ((((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:4
.= ((LSeg |[0 ,0 ]|,p2) \/ ((LSeg p2,p1) \/ (LSeg p1,|[1,0 ]|))) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by XBOOLE_1:4
.= (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A3, A101, TOPREAL1: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}
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A194: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A103, XBOOLE_1:3, XBOOLE_1:26;
p2 in LSeg p1,p2 by RLTOPSP1:69;
then p2 in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2) by A192, XBOOLE_0:def 4;
then {p2} c= (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
then A195: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A159, XBOOLE_0:def 10;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) by A193, XBOOLE_0:def 4;
then {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) = {p1} by A176, XBOOLE_0:def 10;
then A196: P1 /\ P2 = {p1} \/ ((LSeg p1,p2) /\ ((((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) by A195, XBOOLE_1:23
.= {p1} \/ ((((LSeg p1,p2) /\ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})) by A194, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by XBOOLE_1:4 ;

A197: now

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

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

p2 in LSeg p1,p2 by RLTOPSP1:69;
then A199: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {} by A198, Lm20, XBOOLE_0:def 4;
(LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, A101, TOPREAL1:12, XBOOLE_1:26;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {p2} by A198, A199, TOPREAL1:23, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2} by A196; :: thesis: verum

end;

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

now

assume |[0 ,0 ]| in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) ; :: thesis: contradiction
then |[0 ,0 ]| in LSeg p2,p1 by XBOOLE_0:def 4;
then p2 `1 = 0 by A14, A104, A106, A158, Lm4, TOPREAL1:9;
hence contradiction by A104, A107, A200, EUCLID:57; :: thesis: verum

end;

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

end;

end;

end;

now

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

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

p1 in LSeg p1,p2 by RLTOPSP1:69;
then A203: (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {} by A202, Lm25, XBOOLE_0:def 4;
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {p1} by A3, A101, A202, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
then (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {p1} by A203, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A197, ENUMSET1:41; :: thesis: verum

end;

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

now

assume |[1,0 ]| in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: contradiction
then |[1,0 ]| in LSeg p2,p1 by XBOOLE_0:def 4;
then |[1,0 ]| `1 <= p1 `1 by A14, A104, A158, TOPREAL1:9;
then p1 `1 = 1 by A14, A15, Lm8, XXREAL_0:1;
hence contradiction by A14, A17, A204, EUCLID:57; :: thesis: verum

end;

then A205: {|[1,0 ]|} <> (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|} by A3, A101, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
then (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A205, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A197, 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;

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

now

assume A208: |[1,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) ; :: thesis: contradiction
then A209: |[1,0 ]| in LSeg |[0 ,0 ]|,p1 by XBOOLE_0:def 4;
|[0 ,0 ]| `1 <= p1 `1 by A14, A16, EUCLID:56;
then |[1,0 ]| `1 <= p1 `1 by A209, TOPREAL1:9;
then 1 = p1 `1 by A14, A15, Lm8, XXREAL_0:1;
then A210: p1 = |[1,0 ]| by A14, A17, EUCLID:57;
A211: p2 `2 <= |[1,1]| `2 by A207, EUCLID:56;
|[1,0 ]| in LSeg p2,|[1,1]| by A208, XBOOLE_0:def 4;
then 0 = p2 `2 by A207, A211, Lm9, TOPREAL1:10;
hence contradiction by A1, A207, A210, EUCLID:57; :: thesis: verum

end;

then A212: {|[1,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
A213: LSeg |[0 ,1]|,|[1,1]| is_an_arc_of |[0 ,1]|,|[1,1]| by Lm6, Lm10, TOPREAL1:15;
LSeg |[0 ,0 ]|,|[0 ,1]| is_an_arc_of |[0 ,0 ]|,|[0 ,1]| by Lm5, Lm7, TOPREAL1:15;
then A214: (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[0 ,0 ]|,|[1,1]| by A213, 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,|[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} )
A215: LSeg |[0 ,0 ]|,|[1,0 ]| = (LSeg p1,|[1,0 ]|) \/ (LSeg p1,|[0 ,0 ]|) by A3, TOPREAL1:11;
|[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
then A216: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} by Lm26, XBOOLE_0:def 4;
A217: |[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
|[1,0 ]| in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
then A218: (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} by A217, XBOOLE_0:def 4;
A219: LSeg p2,|[1,0 ]| c= LSeg |[1,0 ]|,|[1,1]| by A206, Lm25, TOPREAL1:12;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by A12, XBOOLE_1:27;
then A220: (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} by A218, TOPREAL1:22, ZFMISC_1:39;
( p1 <> |[1,0 ]| or p2 <> |[1,0 ]| ) by A1;
hence P1 is_an_arc_of p1,p2 by A220, TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A221: (LSeg p1,|[1,0 ]|) /\ (LSeg p1,|[0 ,0 ]|) = {p1} by A3, TOPREAL1:14;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A222: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A219, XBOOLE_1:3, XBOOLE_1:26;
A223: LSeg p2,|[1,1]| c= LSeg |[1,0 ]|,|[1,1]| by A206, Lm27, TOPREAL1:12;
then A224: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= {|[1,1]|} by TOPREAL1:24, XBOOLE_1:27;
A225: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {} by A223, Lm3, XBOOLE_1:3, XBOOLE_1:26;
((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) /\ (LSeg |[1,1]|,p2) = ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)) \/ ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2)) by XBOOLE_1:23
.= {|[1,1]|} by A225, A224, A216, ZFMISC_1:39 ;
then A226: ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2) is_an_arc_of |[0 ,0 ]|,p2 by A214, TOPREAL1:16;
A227: (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) = {p2} by A206, TOPREAL1:14;
A228: LSeg |[1,0 ]|,|[1,1]| = (LSeg |[1,1]|,p2) \/ (LSeg |[1,0 ]|,p2) by A206, TOPREAL1:11;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) c= {|[1,0 ]|} by A10, A223, TOPREAL1:22, XBOOLE_1:27;
then A229: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A212, 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 A229, XBOOLE_1:23
.= {|[0 ,0 ]|} by A8, A6, A11, TOPREAL1:23, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A226, 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,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by XBOOLE_1:4
.= (LSeg |[1,0 ]|,p2) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by A215, XBOOLE_1:4
.= ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,1]|,p2)) \/ (LSeg |[1,0 ]|,p2) by XBOOLE_1:4
.= (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|) by A228, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A230: P1 /\ P2 = ((LSeg p1,|[1,0 ]|) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by XBOOLE_1:23
.= (((LSeg p1,|[1,0 ]|) /\ (LSeg p1,|[0 ,0 ]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by A221, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg |[1,0 ]|,p1) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by A13, XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ (((LSeg |[1,0 ]|,p2) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2})) by A227, XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ ((((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})) by A222 ;

A231: now

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

suppose A232: 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 A233: (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 A219, Lm4, Lm8, Lm10, TOPREAL1:9;
then (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = {} by A233, Lm1;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by A230, A232, TOPREAL1: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 A234: 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})

A235: p1 in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
p1 in LSeg |[1,0 ]|,p2 by A234, RLTOPSP1:69;
then A236: {} <> (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) by A235, XBOOLE_0:def 4;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {|[1,0 ]|} /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A234, RLTOPSP1:71;
then A237: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by Lm1, Lm16;
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A10, A219, XBOOLE_1:27;
then (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = {p1} by A234, A236, TOPREAL1: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 A230, A237, XBOOLE_1:4
.= (({p1} \/ {p1}) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) ;
:: thesis: verum

end;

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

now

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

end;

then A240: {|[1,0 ]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) by ZFMISC_1:37;
(LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A10, A219, XBOOLE_1:27;
then A241: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = {} by A240, TOPREAL1:22, ZFMISC_1:39;

now

assume |[0 ,0 ]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) ; :: thesis: contradiction
then A242: |[0 ,0 ]| in LSeg p1,|[1,0 ]| by XBOOLE_0:def 4;
p1 `1 <= |[1,0 ]| `1 by A14, A15, EUCLID:56;
then p1 `1 = 0 by A14, A16, A242, Lm4, TOPREAL1:9;
hence contradiction by A14, A17, A238, EUCLID:57; :: thesis: verum

end;

then A243: {|[0 ,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by ZFMISC_1:37;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, Lm24, TOPREAL1:12, XBOOLE_1:26;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A243, TOPREAL1:23, 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 A230, A241; :: thesis: verum

end;

end;

end;

now

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

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

|[1,0 ]| in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
then A245: {} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) by A244, Lm25, XBOOLE_0:def 4;
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {|[1,0 ]|} /\ (LSeg |[0 ,1]|,|[1,1]|) by A244, RLTOPSP1:71;
then A246: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by Lm1, Lm17;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= {p2} by A12, A244, TOPREAL1:22, XBOOLE_1:27;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {p2} by A245, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A231, A246, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

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

then A248: (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 A12, Lm5, Lm9, Lm11, TOPREAL1:10;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A248, Lm1;
hence P1 /\ P2 = {p1,p2} by A231, A247, ENUMSET1:41, TOPREAL1:24; :: thesis: verum

end;

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

now

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

end;

then A251: {|[1,1]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A206, Lm25, TOPREAL1:12, XBOOLE_1:26;
then A252: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A251, TOPREAL1:24, ZFMISC_1:39;

now

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

end;

then A254: {|[1,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
(LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= {|[1,0 ]|} by A12, A223, TOPREAL1:22, XBOOLE_1:27;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A254, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A231, A252, ENUMSET1:41; :: thesis: verum

end;

end;

end;

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

end;

end;