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

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

suppose A15: p2 in LSeg |[0 ,0 ]|,|[0 ,1]| ; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )

then A16: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 0 & q `2 <= 1 & q `2 >= 0 ) by TOPREAL1:19;
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} )
A17: LSeg p2,|[0 ,1]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A15, Lm15, TOPREAL1:12;
A18: LSeg p2,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A15, Lm13, TOPREAL1:12;
|[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then ( (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & |[0 ,1]| in (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) ) by A17, Lm16, XBOOLE_0:def 4, XBOOLE_1:26;
then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {|[0 ,1]|} by TOPREAL1:21, ZFMISC_1:39;
then A19: (LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[1,1]|,p2 by Lm4, TOPREAL1:15, TOPREAL1:16;
A20: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {} by A7, A17, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(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 A11, A12, A20, 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 A19, TOPREAL1:17;
hence P1 is_an_arc_of p1,p2 by XBOOLE_1:4; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
( (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & |[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 ) by A18, RLTOPSP1:69, XBOOLE_1:26;
then ( (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= {|[0 ,0 ]|} & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} ) by Lm14, TOPREAL1:23, XBOOLE_0:def 4;
then (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|} by ZFMISC_1:39;
then A21: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,p2) is_an_arc_of |[1,0 ]|,p2 by Lm4, TOPREAL1:15, TOPREAL1:16;
A22: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A8, A18, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(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, A10, A22, 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 A21, 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} )
A23: (LSeg p1,|[1,1]|) \/ (LSeg p1,|[1,0 ]|) = LSeg |[1,0 ]|,|[1,1]| by A3, TOPREAL1:11;
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 A15, 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 A23, 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}
A24: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A15, TOPREAL1:14;
( (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,0 ]|) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} ) by A8, A17, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:27;
then A25: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {} by XBOOLE_1:3;
( (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} ) by A7, A18, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:27;
then A26: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by XBOOLE_1:3;
A27: (LSeg p1,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) = {p1} by A3, TOPREAL1:14;
A28: 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 A24, 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 A26, A27, XBOOLE_1:23 ;

A29: now

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

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

end;

suppose A31: 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, Lm12;
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 A28, A31, 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 A32: ( 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})

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

now

assume |[1,0 ]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then ( |[1,0 ]| in LSeg p1,|[1,1]| & p1 `2 <= |[1,1]| `2 ) by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then p1 `2 = 0 by A5, A6, Lm4, TOPREAL1:10;
hence contradiction by A5, A6, A32, EUCLID:57; :: thesis: verum

end;

then {|[1,0 ]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
then A34: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A33, TOPREAL1:22, ZFMISC_1:39;
A35: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) c= {|[1,1]|} by A3, Lm18, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;

now

assume |[1,1]| in (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) ; :: thesis: contradiction
then ( |[1,1]| in LSeg |[1,0 ]|,p1 & |[1,0 ]| `2 <= p1 `2 ) by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then |[1,1]| `2 <= p1 `2 by TOPREAL1:10;
then 1 = p1 `2 by A5, A6, Lm4, XXREAL_0:1;
hence contradiction by A5, A6, A32, EUCLID:57; :: thesis: verum

end;

then {|[1,1]|} <> (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) by ZFMISC_1:37;
then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) = {} by A35, 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 A28, A34; :: thesis: verum

end;

end;

end;

now

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

suppose A36: 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, Lm6;
hence P1 /\ P2 = {p1,p2} by A29, A36, ENUMSET1:41, TOPREAL1:23; :: thesis: verum

end;

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

end;

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

A39: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A15, Lm13, TOPREAL1:12, XBOOLE_1:26;

now

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

end;

then {|[0 ,1]|} <> (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
then A40: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A39, TOPREAL1:21, ZFMISC_1:39;
A41: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A15, Lm15, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;

now

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

end;

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

end;

end;

end;

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

end;

suppose A42: 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 A43: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) by TOPREAL1:19;
take P1 = (LSeg p1,|[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} )
A44: LSeg |[1,1]|,p2 c= LSeg |[0 ,1]|,|[1,1]| by A42, Lm19, TOPREAL1:12;
A45: LSeg p2,|[0 ,1]| c= LSeg |[0 ,1]|,|[1,1]| by A42, Lm16, TOPREAL1:12;
( |[1,1]| in LSeg p1,|[1,1]| & |[1,1]| in LSeg |[1,1]|,p2 ) by RLTOPSP1:69;
then ( (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) & |[1,1]| in (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) & (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[1,1]|} ) by A7, A44, TOPREAL1:24, XBOOLE_0:def 4, XBOOLE_1:27;
then ( (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} & ( p1 <> |[1,1]| or |[1,1]| <> p2 ) ) by A1, ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
( LSeg |[0 ,0 ]|,|[1,0 ]| is_an_arc_of |[1,0 ]|,|[0 ,0 ]| & LSeg |[0 ,0 ]|,|[0 ,1]| is_an_arc_of |[0 ,0 ]|,|[0 ,1]| ) by Lm4, TOPREAL1:15;
then A46: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,0 ]|,|[0 ,1]| by TOPREAL1:5, TOPREAL1:23;
A47: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by A45, Lm2, XBOOLE_1:3, XBOOLE_1:26;
|[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then A48: ( (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) c= {|[0 ,1]|} & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} ) by A45, Lm15, TOPREAL1:21, XBOOLE_0:def 4, XBOOLE_1:27;
((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 A47, A48, ZFMISC_1:39 ;
then A49: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[1,0 ]|,p2 by A46, TOPREAL1:16;
A50: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A8, A45, XBOOLE_1:27;

now

assume |[1,1]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) ; :: thesis: contradiction
then ( |[1,1]| in LSeg |[1,0 ]|,p1 & |[1,1]| in LSeg |[0 ,1]|,p2 & |[0 ,1]| `1 <= p2 `1 & |[1,0 ]| `2 <= p1 `2 ) by A5, A6, A43, EUCLID:56, XBOOLE_0:def 4;
then ( |[1,1]| `2 <= p1 `2 & |[1,1]| `1 <= p2 `1 ) by TOPREAL1:9, TOPREAL1:10;
then A51: ( 1 = p1 `2 & 1 = p2 `2 & 1 = p1 `1 & 1 = p2 `1 ) by A5, A6, A43, Lm4, XXREAL_0:1;
then p1 = |[1,1]| by EUCLID:57
.= p2 by A51, EUCLID:57 ;
hence contradiction by A1; :: thesis: verum

end;

then {|[1,1]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
then A52: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by A50, 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 A52, XBOOLE_1:23
.= {|[1,0 ]|} by A9, A10, A13, TOPREAL1:22, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A49, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A53: (LSeg p1,|[1,1]|) \/ (LSeg p1,|[1,0 ]|) = LSeg |[1,0 ]|,|[1,1]| by A3, TOPREAL1:11;
A54: (LSeg |[0 ,1]|,p2) \/ (LSeg |[1,1]|,p2) = LSeg |[0 ,1]|,|[1,1]| by A42, TOPREAL1:11;
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 A53, 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 A54, TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A55: {p1} = (LSeg p1,|[1,1]|) /\ (LSeg p1,|[1,0 ]|) by A3, TOPREAL1:14;
( (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} ) by A7, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:26;
then A56: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by XBOOLE_1:3;
A57: {p2} = (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,1]|,p2) by A42, TOPREAL1:14;
( (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} ) by A44, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A58: (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by XBOOLE_1:3;
A59: 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 A55, 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 A56, 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 A57, 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 A58 ;

A60: now

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

suppose A61: 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 A62: (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 A44, Lm4, TOPREAL1:10;
then A63: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {} by A62, 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 A59, A61, 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 A63 ; :: thesis: verum

end;

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

then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[1,1]|} /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by RLTOPSP1:71;
then A65: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by Lm1, Lm12;
|[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
then A66: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) <> {} by A64, Lm20, XBOOLE_0:def 4;
(LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) c= {p1} by A44, A64, TOPREAL1:24, XBOOLE_1:27;
then (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {p1} by A66, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A59, A65, 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 A67: ( 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})

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

now

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

end;

then {|[1,0 ]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
then A69: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A68, TOPREAL1:22, ZFMISC_1:39;
A70: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) c= {|[1,1]|} by A8, A44, TOPREAL1:24, XBOOLE_1:27;

now

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

end;

then {|[1,1]|} <> (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) by ZFMISC_1:37;
then (LSeg |[1,1]|,p2) /\ (LSeg p1,|[1,0 ]|) = {} by A70, 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 A59, A69; :: thesis: verum

end;

end;

end;

now

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

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

then A72: (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 A7, Lm4, TOPREAL1:9;
then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {} by A72, Lm1;
hence P1 /\ P2 = {p1,p2} by A60, A71, ENUMSET1:41, TOPREAL1:21; :: thesis: verum

end;

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

A74: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A7, A45, XBOOLE_1:27;
|[1,1]| in LSeg p1,|[1,1]| by RLTOPSP1:69;
then (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} by A73, Lm19, XBOOLE_0:def 4;
then A75: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {p2} by A73, A74, TOPREAL1:24, ZFMISC_1:39;
(LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {|[1,1]|} /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A73, RLTOPSP1:71;
then (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by Lm1, Lm11;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A60, A75, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

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

A77: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A7, A45, XBOOLE_1:27;

now

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

end;

then {|[1,1]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
then A78: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {} by A77, TOPREAL1:24, ZFMISC_1:39;
A79: (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A42, Lm19, TOPREAL1:12, XBOOLE_1:26;

now

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

end;

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

end;

end;

end;

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

end;

suppose A80: 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 A81: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 0 ) by TOPREAL1:19;
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} )
A82: LSeg p2,|[1,0 ]| c= LSeg |[0 ,0 ]|,|[1,0 ]| by A80, Lm17, TOPREAL1:12;
A83: LSeg p2,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[1,0 ]| by A80, Lm14, TOPREAL1:12;
( |[1,0 ]| in LSeg p1,|[1,0 ]| & |[1,0 ]| in LSeg |[1,0 ]|,p2 ) by RLTOPSP1:69;
then ( (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[1,0 ]|} & (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} ) by A8, A82, TOPREAL1:22, XBOOLE_0:def 4, XBOOLE_1:27;
then ( (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} & ( p1 <> |[1,0 ]| or p2 <> |[1,0 ]| ) ) by A1, ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
( LSeg |[0 ,1]|,|[1,1]| is_an_arc_of |[1,1]|,|[0 ,1]| & LSeg |[0 ,0 ]|,|[0 ,1]| is_an_arc_of |[0 ,1]|,|[0 ,0 ]| ) by Lm4, TOPREAL1:15;
then A84: (LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by TOPREAL1:5, TOPREAL1:21;
A85: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A83, Lm2, XBOOLE_1:3, XBOOLE_1:26;
|[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
then A86: ( (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= {|[0 ,0 ]|} & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} ) by A83, Lm13, TOPREAL1:23, XBOOLE_0:def 4, XBOOLE_1:27;
((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 A85, A86, ZFMISC_1:39 ;
then A87: ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2) is_an_arc_of |[1,1]|,p2 by A84, TOPREAL1:16;
A88: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A7, A83, XBOOLE_1:27;

now

assume |[1,0 ]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) ; :: thesis: contradiction
then ( |[1,0 ]| in LSeg p1,|[1,1]| & |[1,0 ]| in LSeg |[0 ,0 ]|,p2 & p1 `2 <= |[1,1]| `2 & |[0 ,0 ]| `1 <= p2 `1 ) by A5, A6, A81, EUCLID:56, XBOOLE_0:def 4;
then ( |[1,0 ]| `1 <= p2 `1 & p1 `2 <= |[1,0 ]| `2 ) by TOPREAL1:9, TOPREAL1:10;
then ( 0 = p1 `2 & 0 = p2 `2 & 1 = p1 `1 & 1 = p2 `1 ) by A5, A6, A81, Lm4, XXREAL_0:1;
then ( p1 = |[1,0 ]| & p2 = |[1,0 ]| ) by EUCLID:57;
hence contradiction by A1; :: thesis: verum

end;

then {|[1,0 ]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
then A89: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A88, 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 A89, XBOOLE_1:23
.= {|[1,1]|} by A11, A12, A14, TOPREAL1:24, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A87, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A90: (LSeg p1,|[1,0 ]|) \/ (LSeg p1,|[1,1]|) = LSeg |[1,0 ]|,|[1,1]| by A3, TOPREAL1:11;
A91: (LSeg |[0 ,0 ]|,p2) \/ (LSeg |[1,0 ]|,p2) = LSeg |[0 ,0 ]|,|[1,0 ]| by A80, TOPREAL1:11;
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 A90, 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 A91, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A92: (LSeg p1,|[1,0 ]|) /\ (LSeg p1,|[1,1]|) = {p1} by A3, TOPREAL1:14;
A93: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A80, TOPREAL1:14;
( (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} ) by A82, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A94: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by XBOOLE_1:3;
A95: 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 A92, 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 A13, 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 A93, 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 A94 ;

A96: now

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

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

then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {|[1,0 ]|} /\ (LSeg |[0 ,1]|,|[1,1]|) by RLTOPSP1:71;
then A98: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by Lm1, Lm10;
A99: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) c= {p1} by A82, A97, TOPREAL1:22, XBOOLE_1:27;
|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) <> {} by A97, Lm18, XBOOLE_0:def 4;
then (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) = {p1} by A99, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ({p1} \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A95, A98, 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 A100: 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 A101: (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 A82, Lm4, TOPREAL1:10;
then (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) = {} by A101, 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 A95, A100, 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 A102: ( 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})

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

now

assume |[1,1]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then ( |[1,1]| in LSeg |[1,0 ]|,p1 & |[1,0 ]| `2 <= p1 `2 ) by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then |[1,1]| `2 <= p1 `2 by TOPREAL1:10;
then p1 `2 = 1 by A5, A6, Lm4, XXREAL_0:1;
hence contradiction by A5, A6, A102, EUCLID:57; :: thesis: verum

end;

then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) <> {|[1,1]|} by ZFMISC_1:37;
then A104: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A103, TOPREAL1:24, ZFMISC_1:39;
A105: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) c= {|[1,0 ]|} by A7, A82, TOPREAL1:22, XBOOLE_1:27;

now

assume |[1,0 ]| in (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) ; :: thesis: contradiction
then ( |[1,0 ]| in LSeg p1,|[1,1]| & p1 `2 <= |[1,1]| `2 ) by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then p1 `2 = 0 by A5, A6, Lm4, TOPREAL1:10;
hence contradiction by A5, A6, A102, EUCLID:57; :: thesis: verum

end;

then {|[1,0 ]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) by ZFMISC_1:37;
then (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[1,1]|) = {} by A105, 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 A95, A104; :: thesis: verum

end;

end;

end;

now

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

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

then A107: (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 A8, Lm4, TOPREAL1:9;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A107, Lm1;
hence P1 /\ P2 = {p1,p2} by A96, A106, ENUMSET1:41, TOPREAL1:23; :: thesis: verum

end;

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

A109: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A8, A83, XBOOLE_1:27;
|[1,0 ]| in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
then (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} by A108, Lm17, XBOOLE_0:def 4;
then A110: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A108, A109, TOPREAL1:22, ZFMISC_1:39;
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {|[1,0 ]|} /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A108, RLTOPSP1:71;
then (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by Lm1, Lm9;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A96, A110, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

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

A112: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A8, A83, XBOOLE_1:27;

now

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

end;

then {|[1,0 ]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
then A113: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A112, TOPREAL1:22, ZFMISC_1:39;
A114: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A80, Lm17, TOPREAL1:12, XBOOLE_1:26;

now

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

end;

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

end;

end;

end;

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

end;

suppose A115: 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 consider q being Point of (TOP-REAL 2) such that
A116: q = p2 and
A117: ( q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) by TOPREAL1:19;
A118: ( p = |[(p `1 ),(p `2 )]| & q = |[(q `1 ),(q `2 )]| ) by EUCLID:57;
A119: LSeg |[1,1]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A115, Lm20, TOPREAL1:12;
A120: LSeg |[1,0 ]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A115, Lm18, TOPREAL1:12;
A121: LSeg p1,p2 c= LSeg |[1,0 ]|,|[1,1]| by A3, A115, TOPREAL1:12;

now

per cases ( p `2 < q `2 or q `2 < p `2 ) by A1, A5, A6, A116, A117, A118, XXREAL_0:1;

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

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} )
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} )

A123: now

assume A124: (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) <> {} ; :: thesis: contradiction
consider a being Element of (LSeg p1,|[1,0 ]|) /\ (LSeg |[1,1]|,p2);
reconsider p = a as Point of (TOP-REAL 2) by A124, TARSKI:def 3;
( p in LSeg |[1,0 ]|,p1 & p in LSeg p2,|[1,1]| & |[1,0 ]| `2 <= p1 `2 & p2 `2 <= |[1,1]| `2 ) by A5, A6, A116, A117, A124, EUCLID:56, XBOOLE_0:def 4;
then ( p `2 <= p1 `2 & p2 `2 <= p `2 ) by TOPREAL1:10;
hence contradiction by A5, A116, A122, XXREAL_0:2; :: thesis: verum

end;

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

now

assume |[1,1]| in (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then ( |[1,1]| in LSeg |[1,0 ]|,p1 & |[1,0 ]| `2 <= p1 `2 ) by A5, A6, EUCLID:56, XBOOLE_0:def 4;
then |[1,1]| `2 <= p1 `2 by TOPREAL1:10;
hence contradiction by A5, A6, A117, A122, Lm4, XXREAL_0:1; :: thesis: verum

end;

then {|[1,1]|} <> (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
then A126: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A125, TOPREAL1:24, ZFMISC_1:39;
A127: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, Lm18, TOPREAL1:12, XBOOLE_1:26;
|[1,0 ]| in LSeg p1,|[1,0 ]| by RLTOPSP1:69;
then A128: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) <> {} by Lm17, XBOOLE_0:def 4;
( (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} ) by A8, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:26;
then A129: (LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by XBOOLE_1:3;
A130: (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 A123, XBOOLE_1:23
.= ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A126, XBOOLE_1:23
.= {|[1,0 ]|} by A127, A128, A129, TOPREAL1:22, ZFMISC_1:39 ;
A131: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,0 ]|,|[0 ,1]| by Lm4, TOPREAL1:15, TOPREAL1:16, TOPREAL1:23;
((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 ;
then A132: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|) is_an_arc_of |[1,0 ]|,|[1,1]| by A131, TOPREAL1:16;
A133: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= {|[1,1]|} by A115, Lm20, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;
|[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} by Lm19, XBOOLE_0:def 4;
then A134: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} by A133, ZFMISC_1:39;
A135: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= {|[1,0 ]|} by A115, Lm20, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;

now

assume |[1,0 ]| in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) ; :: thesis: contradiction
then ( |[1,0 ]| in LSeg p2,|[1,1]| & p2 `2 <= |[1,1]| `2 ) by A116, A117, EUCLID:56, XBOOLE_0:def 4;
hence contradiction by A6, A116, A122, Lm4, TOPREAL1:10; :: thesis: verum

end;

then {|[1,0 ]|} <> (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
then A136: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A135, ZFMISC_1:39;
( (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} ) by A119, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:26;
then A137: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {} by 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 A134, XBOOLE_1:23
.= {|[1,1]|} by A136, A137 ;
then (((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 A132, TOPREAL1:16;
hence P2 is_an_arc_of p1,p2 by A130, 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, A115, 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}
( p1 in LSeg p1,p2 & p1 in LSeg p1,|[1,0 ]| ) by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) by XBOOLE_0:def 4;
then A138: {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) by ZFMISC_1:37;
(LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) c= {p1}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) or a in {p1} )
assume A139: a in (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
( p in LSeg p1,p2 & p in LSeg |[1,0 ]|,p1 & p1 `1 <= p2 `1 & p1 `2 <= p2 `2 & |[1,0 ]| `2 <= p1 `2 ) by A5, A6, A116, A117, A122, A139, EUCLID:56, XBOOLE_0:def 4;
then ( p `1 <= p2 `1 & p1 `1 <= p `1 & p `2 <= p1 `2 & p1 `2 <= p `2 ) by TOPREAL1:9, TOPREAL1:10;
then ( p1 `2 = p `2 & p `1 = 1 ) by A5, A6, A116, A117, XXREAL_0:1;
then p = |[1,(p1 `2 )]| by EUCLID:57
.= p1 by A5, A6, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

then A140: (LSeg p1,p2) /\ (LSeg p1,|[1,0 ]|) = {p1} by A138, XBOOLE_0:def 10;
( p2 in LSeg p1,p2 & p2 in LSeg |[1,1]|,p2 ) by RLTOPSP1:69;
then p2 in (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) by XBOOLE_0:def 4;
then A141: {p2} c= (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
(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 A142: a in (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
( p in LSeg p1,p2 & p in LSeg p2,|[1,1]| & p1 `1 <= p2 `1 & p1 `2 <= p2 `2 & p2 `2 <= |[1,1]| `2 ) by A5, A6, A116, A117, A122, A142, EUCLID:56, XBOOLE_0:def 4;
then ( p `1 <= p2 `1 & p1 `1 <= p `1 & p `2 <= p2 `2 & p2 `2 <= p `2 ) by TOPREAL1:9, TOPREAL1:10;
then ( p2 `2 = p `2 & p `1 = 1 ) by A5, A6, A116, A117, XXREAL_0:1;
then p = |[1,(p2 `2 )]| by EUCLID:57
.= p2 by A116, A117, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

then A143: (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) = {p2} by A141, XBOOLE_0:def 10;
( (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} ) by A121, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:26;
then A144: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by XBOOLE_1:3;
A145: 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 A140, XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2}) by A143, 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 A144, 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 ;
A146: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, A115, TOPREAL1:12, XBOOLE_1:26;

A147: now

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

suppose A148: 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 Lm17, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p1} by A146, A148, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by A145; :: thesis: verum

end;

suppose A149: 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 & p1 `2 <= p2 `2 ) by A5, A116, A122, XBOOLE_0:def 4;
then p1 `2 = 0 by A5, A6, Lm4, TOPREAL1:10;
hence contradiction by A5, A6, A149, 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 A146, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by A145; :: thesis: verum

end;

end;

end;

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

now

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

suppose A151: 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 Lm19, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {p2} by A150, A151, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A147, ENUMSET1:41; :: thesis: verum

end;

suppose A152: 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 & p1 `2 <= p2 `2 ) by A5, A116, A122, XBOOLE_0:def 4;
then |[1,1]| `2 <= p2 `2 by TOPREAL1:10;
then p2 `2 = 1 by A116, A117, Lm4, XXREAL_0:1;
hence contradiction by A116, A117, A152, 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 A150, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A147, ENUMSET1:41; :: thesis: verum

end;

end;

end;

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

end;

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

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} )
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} )

A154: now

assume A155: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) <> {} ; :: thesis: contradiction
consider a being Element of (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2);
reconsider p = a as Point of (TOP-REAL 2) by A155, TARSKI:def 3;
( p in LSeg p1,|[1,1]| & p in LSeg |[1,0 ]|,p2 & p1 `2 <= |[1,1]| `2 & |[1,0 ]| `2 <= p2 `2 ) by A5, A6, A116, A117, A155, EUCLID:56, XBOOLE_0:def 4;
then ( p `2 <= p2 `2 & p1 `2 <= p `2 ) by TOPREAL1:10;
hence contradiction by A5, A116, A153, XXREAL_0:2; :: thesis: verum

end;

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

now

assume |[1,0 ]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then ( |[1,0 ]| in LSeg p1,|[1,1]| & p1 `2 <= |[1,1]| `2 ) by A5, A6, EUCLID:56, XBOOLE_0:def 4;
hence contradiction by A5, A117, A153, Lm4, TOPREAL1:10; :: thesis: verum

end;

then {|[1,0 ]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
then A157: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A156, TOPREAL1:22, ZFMISC_1:39;
A158: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, Lm20, TOPREAL1:12, XBOOLE_1:26;
|[1,1]| in LSeg p1,|[1,1]| by RLTOPSP1:69;
then A159: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) <> {} by Lm19, XBOOLE_0:def 4;
( (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} ) by A7, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:26;
then A160: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by XBOOLE_1:3;
A161: (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 A154, XBOOLE_1:23
.= ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A157, XBOOLE_1:23
.= {|[1,1]|} by A158, A159, A160, TOPREAL1:24, ZFMISC_1:39 ;
A162: (LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by Lm4, TOPREAL1:15, TOPREAL1:16, TOPREAL1:21;
((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 ;
then A163: ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) is_an_arc_of |[1,1]|,|[1,0 ]| by A162, TOPREAL1:16;
A164: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,0 ]|} by A115, Lm18, TOPREAL1:12, TOPREAL1:22, XBOOLE_1:26;
|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} by Lm17, XBOOLE_0:def 4;
then A165: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} by A164, ZFMISC_1:39;
A166: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,1]|} by A115, Lm18, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;

now

assume |[1,1]| in (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) ; :: thesis: contradiction
then ( |[1,1]| in LSeg |[1,0 ]|,p2 & |[1,0 ]| `2 <= p2 `2 ) by A116, A117, EUCLID:56, XBOOLE_0:def 4;
then |[1,1]| `2 <= p2 `2 by TOPREAL1:10;
hence contradiction by A6, A116, A117, A153, Lm4, XXREAL_0:1; :: thesis: verum

end;

then {|[1,1]|} <> (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
then A167: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A166, ZFMISC_1:39;
( (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} ) by A120, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:26;
then A168: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by 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 A165, XBOOLE_1:23
.= {|[1,0 ]|} by A167, A168 ;
then (((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 A163, TOPREAL1:16;
hence P2 is_an_arc_of p1,p2 by A161, 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, A115, TOPREAL1:13
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
( p1 in LSeg p1,p2 & p1 in LSeg p1,|[1,1]| ) by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) by XBOOLE_0:def 4;
then A169: {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) by ZFMISC_1:37;
(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 A170: a in (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
( p in LSeg p2,p1 & p in LSeg p1,|[1,1]| & p2 `1 <= p1 `1 & p2 `2 <= p1 `2 & p1 `2 <= |[1,1]| `2 ) by A5, A6, A116, A117, A153, A170, EUCLID:56, XBOOLE_0:def 4;
then ( p `1 <= p1 `1 & p2 `1 <= p `1 & p `2 <= p1 `2 & p1 `2 <= p `2 ) by TOPREAL1:9, TOPREAL1:10;
then ( p1 `2 = p `2 & p `1 = 1 ) by A5, A6, A116, A117, XXREAL_0:1;
then p = |[1,(p1 `2 )]| by EUCLID:57
.= p1 by A5, A6, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

then A171: (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) = {p1} by A169, XBOOLE_0:def 10;
( p2 in LSeg p1,p2 & p2 in LSeg |[1,0 ]|,p2 ) by RLTOPSP1:69;
then p2 in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) by XBOOLE_0:def 4;
then A172: {p2} c= (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
(LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) c= {p2}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) or a in {p2} )
assume A173: a in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
( p in LSeg p2,p1 & p in LSeg |[1,0 ]|,p2 & p2 `1 <= p1 `1 & p2 `2 <= p1 `2 & |[1,0 ]| `2 <= p2 `2 ) by A5, A6, A116, A117, A153, A173, EUCLID:56, XBOOLE_0:def 4;
then ( p `1 <= p1 `1 & p2 `1 <= p `1 & p `2 <= p2 `2 & p2 `2 <= p `2 ) by TOPREAL1:9, TOPREAL1:10;
then ( p2 `2 = p `2 & p `1 = 1 ) by A5, A6, A116, A117, XXREAL_0:1;
then p = |[1,(p2 `2 )]| by EUCLID:57
.= p2 by A116, A117, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

then A174: (LSeg p1,p2) /\ (LSeg |[1,0 ]|,p2) = {p2} by A172, XBOOLE_0:def 10;
( (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} ) by A121, TOPREAL1:26, XBOOLE_0:def 7, XBOOLE_1:26;
then A175: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by XBOOLE_1:3;
A176: 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 A171, XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2}) by A174, 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 A175, 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 ;
A177: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, A115, TOPREAL1:12, XBOOLE_1:26;

A178: now

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

suppose A179: 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 Lm19, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {p1} by A177, A179, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A176; :: thesis: verum

end;

suppose A180: 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 & p2 `2 <= p1 `2 ) by A5, A116, A153, XBOOLE_0:def 4;
then |[1,1]| `2 <= p1 `2 by TOPREAL1:10;
then p1 `2 = 1 by A5, A6, Lm4, XXREAL_0:1;
hence contradiction by A5, A6, A180, 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 A177, TOPREAL1:24, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A176; :: thesis: verum

end;

end;

end;

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

now

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

suppose A182: 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 Lm17, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p2} by A181, A182, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A178, ENUMSET1:41; :: thesis: verum

end;

suppose A183: 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 & p2 `2 <= p1 `2 ) by A5, A116, A153, XBOOLE_0:def 4;
then p2 `2 = 0 by A116, A117, Lm4, TOPREAL1:10;
hence contradiction by A116, A117, A183, 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 A181, TOPREAL1:22, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A178, 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;