let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg |[0 ,0 ]|,|[0 ,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 |[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} )
A4: LSeg |[0 ,0 ]|,p1 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, Lm20, TOPREAL1:12;
|[0 ,0 ]| in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
then |[0 ,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by Lm21, XBOOLE_0:def 4;
then A5: {|[0 ,0 ]|} c= (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
A6: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A3, Lm20, TOPREAL1:12, XBOOLE_1:26;
then A7: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[0 ,0 ]|} by A5, TOPREAL1:23, XBOOLE_0:def 10;
A8: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A9: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A4, XBOOLE_1:3, XBOOLE_1:26;
|[0 ,1]| in LSeg |[0 ,1]|,p1 by RLTOPSP1:69;
then |[0 ,1]| in (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) by Lm23, XBOOLE_0:def 4;
then A10: {|[0 ,1]|} c= (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
A11: ( 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;
A12: (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A3, Lm22, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
A13: LSeg p1,|[0 ,1]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, Lm22, TOPREAL1:12;
then A14: (LSeg |[0 ,1]|,p1) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A8, XBOOLE_1:3, XBOOLE_1:26;
consider p being Point of (TOP-REAL 2) such that
A15: p = p1 and
A16: p `1 = 0 and
A17: p `2 <= 1 and
A18: 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 A11, XBOOLE_0:def 3;

suppose A19: 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 A20: LSeg p2,p1 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, TOPREAL1:12;
A21: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
consider q being Point of (TOP-REAL 2) such that
A22: q = p2 and
A23: q `1 = 0 and
A24: q `2 <= 1 and
A25: q `2 >= 0 by A19, TOPREAL1:19;
A26: q = |[(q `1 ),(q `2 )]| by EUCLID:57;

now

per cases ( p `2 < q `2 or p `2 > q `2 ) by A1, A15, A16, A22, A23, A21, A26, XXREAL_0:1;

case A27: p `2 < q `2 ; :: thesis: ( LSeg p1,p2 is_an_arc_of p1,p2 & (LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)) is_an_arc_of p1,p2 & R^2-unit_square = (LSeg p1,p2) \/ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) & (LSeg p1,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) = {p1,p2} )

A28: (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 A29: a in (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A30: p in LSeg |[0 ,0 ]|,p1 by A29, XBOOLE_0:def 4;
|[0 ,0 ]| `2 <= p1 `2 by A15, A18, EUCLID:56;
then A31: p `2 <= p1 `2 by A30, TOPREAL1:10;
A32: p in LSeg p1,p2 by A29, XBOOLE_0:def 4;
then p1 `2 <= p `2 by A15, A22, A27, TOPREAL1:10;
then A33: p1 `2 = p `2 by A31, XXREAL_0:1;
p1 `1 <= p `1 by A15, A16, A22, A23, A32, TOPREAL1:9;
then p `1 = 0 by A15, A16, A22, A23, A32, TOPREAL1:9;
then p = |[0 ,(p1 `2 )]| by A33, EUCLID:57
.= p1 by A15, A16, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

A34: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A19, Lm22, TOPREAL1:12, XBOOLE_1:26;

A35: now

consider a being Element of (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2);
assume A36: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) <> {} ; :: thesis: contradiction
then reconsider p = a as Point of (TOP-REAL 2) by TARSKI:def 3;
A37: p in LSeg |[0 ,0 ]|,p1 by A36, XBOOLE_0:def 4;
A38: p in LSeg p2,|[0 ,1]| by A36, XBOOLE_0:def 4;
p2 `2 <= |[0 ,1]| `2 by A22, A24, EUCLID:56;
then A39: p2 `2 <= p `2 by A38, TOPREAL1:10;
|[0 ,0 ]| `2 <= p1 `2 by A15, A18, EUCLID:56;
then p `2 <= p1 `2 by A37, TOPREAL1:10;
hence contradiction by A15, A22, A27, A39, XXREAL_0:2; :: thesis: verum

end;

|[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then |[0 ,1]| in (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) by Lm23, XBOOLE_0:def 4;
then A40: {|[0 ,1]|} c= (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;

now

assume |[0 ,0 ]| in (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then A41: |[0 ,0 ]| in LSeg p2,|[0 ,1]| by XBOOLE_0:def 4;
p2 `2 <= |[0 ,1]| `2 by A22, A24, EUCLID:56;
hence contradiction by A18, A22, A27, A41, Lm5, TOPREAL1:10; :: thesis: verum

end;

then A42: {|[0 ,0 ]|} <> (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
(LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A19, Lm22, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
then A43: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A42, ZFMISC_1:39;
A44: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A3, A19, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
A45: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) c= {p2}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) or a in {p2} )
assume A46: a in (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A47: p in LSeg p2,|[0 ,1]| by A46, XBOOLE_0:def 4;
p2 `2 <= |[0 ,1]| `2 by A22, A24, EUCLID:56;
then A48: p2 `2 <= p `2 by A47, TOPREAL1:10;
A49: p in LSeg p1,p2 by A46, XBOOLE_0:def 4;
then p `2 <= p2 `2 by A15, A22, A27, TOPREAL1:10;
then A50: p2 `2 = p `2 by A48, XXREAL_0:1;
p1 `1 <= p `1 by A15, A16, A22, A23, A49, TOPREAL1:9;
then p `1 = 0 by A15, A16, A22, A23, A49, TOPREAL1:9;
then p = |[0 ,(p2 `2 )]| by A50, EUCLID:57
.= p2 by A22, A23, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

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

now

assume |[0 ,1]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then A52: |[0 ,1]| in LSeg |[0 ,0 ]|,p1 by XBOOLE_0:def 4;
|[0 ,0 ]| `2 <= p1 `2 by A15, A18, EUCLID:56;
then |[0 ,1]| `2 <= p1 `2 by A52, TOPREAL1:10;
hence contradiction by A15, A17, A24, A27, Lm7, XXREAL_0:1; :: thesis: verum

end;

then A53: {|[0 ,1]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
set P1 = LSeg p1,p2;
set P2 = (LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2));
A54: p1 in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
A55: LSeg |[0 ,1]|,p2 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A19, Lm22, TOPREAL1:12;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) by A54, XBOOLE_0:def 4;
then {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) by ZFMISC_1:37;
then A56: (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) = {p1} by A28, XBOOLE_0:def 10;
thus LSeg p1,p2 is_an_arc_of p1,p2 by A1, TOPREAL1:15; :: thesis: ( (LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)) is_an_arc_of p1,p2 & R^2-unit_square = (LSeg p1,p2) \/ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) & (LSeg p1,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) = {p1,p2} )
A57: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) /\ (LSeg |[1,1]|,|[0 ,1]|) = {} \/ {|[1,1]|} by Lm2, TOPREAL1:24, XBOOLE_1:23
.= {|[1,1]|} ;
(LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[0 ,0 ]|,|[1,1]| by Lm4, Lm8, TOPREAL1:18, TOPREAL1:22;
then A58: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|) is_an_arc_of |[0 ,0 ]|,|[0 ,1]| by A57, TOPREAL1:16;
(((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) /\ (LSeg |[0 ,1]|,p2) = ((LSeg |[0 ,1]|,p2) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,1]|,|[0 ,1]|)) by XBOOLE_1:23
.= ({} \/ ((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,1]|,|[0 ,1]|)) by A43, XBOOLE_1:23
.= {} \/ ((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,1]|,|[0 ,1]|)) by A55, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= {|[0 ,1]|} by A40, A34, TOPREAL1:21, XBOOLE_0:def 10 ;
then A59: (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[0 ,0 ]|,p2 by A58, TOPREAL1:16;
(LSeg p1,|[0 ,0 ]|) /\ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)) = ((LSeg p1,|[0 ,0 ]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= (((LSeg p1,|[0 ,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= ((((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= {|[0 ,0 ]|} by A9, A7, A35, A51, A53, ZFMISC_1:39 ;
hence (LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)) is_an_arc_of p1,p2 by A59, TOPREAL1:17; :: thesis: ( R^2-unit_square = (LSeg p1,p2) \/ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) & (LSeg p1,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) = {p1,p2} )
((LSeg |[0 ,1]|,p2) \/ (LSeg p2,p1)) \/ (LSeg p1,|[0 ,0 ]|) = LSeg |[0 ,0 ]|,|[0 ,1]| by A3, A19, TOPREAL1:13;
hence R^2-unit_square = (((LSeg p1,p2) \/ (LSeg |[0 ,1]|,p2)) \/ (LSeg p1,|[0 ,0 ]|)) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) by TOPREAL1:def 4, XBOOLE_1:4
.= ((LSeg p1,p2) \/ ((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,1]|,p2))) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) by XBOOLE_1:4
.= (LSeg p1,p2) \/ (((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,1]|,p2)) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|))) by XBOOLE_1:4
.= (LSeg p1,p2) \/ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) by XBOOLE_1:4 ;
:: thesis: (LSeg p1,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) = {p1,p2}
A60: p2 in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
p2 in LSeg p1,p2 by RLTOPSP1:69;
then p2 in (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) by A60, XBOOLE_0:def 4;
then {p2} c= (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
then A61: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) = {p2} by A45, XBOOLE_0:def 10;
A62: LSeg p1,p2 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, A19, TOPREAL1:12;
A63: (LSeg p1,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) = ((LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ ((LSeg p1,p2) /\ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) by XBOOLE_1:23
.= ((LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ (((LSeg p1,p2) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2))) by XBOOLE_1:23
.= ((LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ ((((LSeg p1,p2) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2))) by XBOOLE_1:23
.= {p1} \/ (((((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2))) by A56, XBOOLE_1:23
.= {p1} \/ (((((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {} ) \/ ((LSeg p1,p2) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2))) by A62, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2})) by A61, 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 ;

A64: now

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

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

then |[0 ,0 ]| in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) <> {} by Lm21, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p1} by A44, A65, ZFMISC_1:39;
hence (LSeg p1,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by A63; :: thesis: verum

end;

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

now

assume |[0 ,0 ]| in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then |[0 ,0 ]| in LSeg p1,p2 by XBOOLE_0:def 4;
then p1 `2 <= |[0 ,0 ]| `2 by A15, A22, A27, TOPREAL1:10;
then |[0 ,0 ]| `2 = p1 `2 by A3, Lm5, Lm7, TOPREAL1:10;
hence contradiction by A15, A16, A66, Lm5, EUCLID:57; :: thesis: verum

end;

then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) <> {|[0 ,0 ]|} by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A44, ZFMISC_1:39;
hence (LSeg p1,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by A63; :: thesis: verum

end;

end;

end;

A67: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A3, A19, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;

now

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

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

now

assume |[0 ,1]| in (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then |[0 ,1]| in LSeg p1,p2 by XBOOLE_0:def 4;
then A69: |[0 ,1]| `2 <= p2 `2 by A15, A22, A27, TOPREAL1:10;
p2 `2 <= |[0 ,1]| `2 by A19, Lm5, Lm7, TOPREAL1:10;
then A70: |[0 ,1]| `2 = p2 `2 by A69, XXREAL_0:1;
p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57
.= |[0 ,1]| by A22, A23, A70, EUCLID:56 ;
hence contradiction by A68; :: thesis: verum

end;

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

end;

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

then |[0 ,1]| in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) <> {} by Lm23, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {p2} by A67, A71, ZFMISC_1:39;
hence (LSeg p1,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) = {p1,p2} by A64, ENUMSET1:41; :: thesis: verum

end;

end;

end;

hence (LSeg p1,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) = {p1,p2} ; :: thesis: verum

end;

case A72: 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 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )

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

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p2,p1) /\ (LSeg |[0 ,1]|,p1) or a in {p1} )
assume A74: a in (LSeg p2,p1) /\ (LSeg |[0 ,1]|,p1) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A75: p in LSeg p1,|[0 ,1]| by A74, XBOOLE_0:def 4;
p1 `2 <= |[0 ,1]| `2 by A15, A17, EUCLID:56;
then A76: p1 `2 <= p `2 by A75, TOPREAL1:10;
A77: p in LSeg p2,p1 by A74, XBOOLE_0:def 4;
then p `2 <= p1 `2 by A15, A22, A72, TOPREAL1:10;
then A78: p1 `2 = p `2 by A76, XXREAL_0:1;
p2 `1 <= p `1 by A15, A16, A22, A23, A77, TOPREAL1:9;
then p `1 = 0 by A15, A16, A22, A23, A77, TOPREAL1:9;
then p = |[0 ,(p1 `2 )]| by A78, EUCLID:57
.= p1 by A15, A16, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

A79: LSeg p2,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A19, Lm20, TOPREAL1:12;

A80: now

consider a being Element of (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p1);
assume A81: (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p1) <> {} ; :: thesis: contradiction
then reconsider p = a as Point of (TOP-REAL 2) by TARSKI:def 3;
A82: p in LSeg |[0 ,0 ]|,p2 by A81, XBOOLE_0:def 4;
A83: p in LSeg p1,|[0 ,1]| by A81, XBOOLE_0:def 4;
p1 `2 <= |[0 ,1]| `2 by A15, A17, EUCLID:56;
then A84: p1 `2 <= p `2 by A83, TOPREAL1:10;
|[0 ,0 ]| `2 <= p2 `2 by A22, A25, EUCLID:56;
then p `2 <= p2 `2 by A82, TOPREAL1:10;
hence contradiction by A15, A22, A72, A84, XXREAL_0:2; :: thesis: verum

end;

A85: (LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A3, A19, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;

now

assume |[0 ,1]| in (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then A86: |[0 ,1]| in LSeg |[0 ,0 ]|,p2 by XBOOLE_0:def 4;
|[0 ,0 ]| `2 <= p2 `2 by A22, A25, EUCLID:56;
then |[0 ,1]| `2 <= p2 `2 by A86, TOPREAL1:10;
hence contradiction by A17, A22, A24, A72, Lm7, XXREAL_0:1; :: thesis: verum

end;

then A87: {|[0 ,1]|} <> (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
A88: (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A19, Lm20, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;

now

assume |[0 ,0 ]| in (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then A89: |[0 ,0 ]| in LSeg p1,|[0 ,1]| by XBOOLE_0:def 4;
p1 `2 <= |[0 ,1]| `2 by A15, A17, EUCLID:56;
hence contradiction by A15, A25, A72, A89, Lm5, TOPREAL1:10; :: thesis: verum

end;

then A90: {|[0 ,0 ]|} <> (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
A91: (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A19, Lm20, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
A92: (LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|) c= {p2}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|) or a in {p2} )
assume A93: a in (LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A94: p in LSeg |[0 ,0 ]|,p2 by A93, XBOOLE_0:def 4;
|[0 ,0 ]| `2 <= p2 `2 by A22, A25, EUCLID:56;
then A95: p `2 <= p2 `2 by A94, TOPREAL1:10;
A96: p in LSeg p2,p1 by A93, XBOOLE_0:def 4;
then p2 `2 <= p `2 by A15, A22, A72, TOPREAL1:10;
then A97: p2 `2 = p `2 by A95, XXREAL_0:1;
p2 `1 <= p `1 by A15, A16, A22, A23, A96, TOPREAL1:9;
then p `1 = 0 by A15, A16, A22, A23, A96, TOPREAL1:9;
then p = |[0 ,(p2 `2 )]| by A97, EUCLID:57
.= p2 by A22, A23, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

A98: (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A3, Lm22, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
take P1 = LSeg p2,p1; :: 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 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg p2,|[0 ,0 ]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p1)); :: 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} )
A99: p2 in LSeg p2,|[0 ,0 ]| by RLTOPSP1:69;
p2 in LSeg p2,p1 by RLTOPSP1:69;
then p2 in (LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|) by A99, XBOOLE_0:def 4;
then A100: {p2} c= (LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|) by ZFMISC_1:37;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:15; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A101: (LSeg |[0 ,1]|,|[1,1]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) = {} \/ {|[1,1]|} by Lm2, TOPREAL1:24, XBOOLE_1:23
.= {|[1,1]|} ;
(LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by Lm4, Lm8, TOPREAL1:18, TOPREAL1:22;
then A102: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|) is_an_arc_of |[0 ,1]|,|[0 ,0 ]| by A101, TOPREAL1:17;
|[0 ,0 ]| in LSeg p2,|[0 ,0 ]| by RLTOPSP1:69;
then |[0 ,0 ]| in (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by Lm21, XBOOLE_0:def 4;
then A103: {|[0 ,0 ]|} c= (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
(LSeg p1,|[0 ,1]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) = ((LSeg |[0 ,1]|,p1) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg |[0 ,1]|,p1) /\ (LSeg |[1,1]|,|[0 ,1]|)) by XBOOLE_1:23
.= (((LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg |[0 ,1]|,p1) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg |[0 ,1]|,p1) /\ (LSeg |[1,1]|,|[0 ,1]|)) by XBOOLE_1:23
.= ({} \/ ((LSeg |[0 ,1]|,p1) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg |[0 ,1]|,p1) /\ (LSeg |[1,1]|,|[0 ,1]|)) by A98, A90, ZFMISC_1:39
.= {|[0 ,1]|} by A14, A10, A12, XBOOLE_0:def 10 ;
then A104: (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p1) is_an_arc_of p1,|[0 ,0 ]| by A102, TOPREAL1:17;
((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p1)) /\ (LSeg |[0 ,0 ]|,p2) = ((LSeg p2,|[0 ,0 ]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p1)) by XBOOLE_1:23
.= (((LSeg p2,|[0 ,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p1)) by XBOOLE_1:23
.= ((((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p1)) by XBOOLE_1:23
.= ((((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {} ) \/ ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p1)) by A79, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {} by A80, A91, A87, ZFMISC_1:39
.= {|[0 ,0 ]|} by A103, A88, XBOOLE_0:def 10 ;
hence P2 is_an_arc_of p1,p2 by A104, TOPREAL1:16; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
((LSeg |[0 ,1]|,p1) \/ (LSeg p1,p2)) \/ (LSeg p2,|[0 ,0 ]|) = LSeg |[0 ,0 ]|,|[0 ,1]| by A3, A19, TOPREAL1:13;
hence R^2-unit_square = (((LSeg p2,p1) \/ (LSeg |[0 ,1]|,p1)) \/ (LSeg p2,|[0 ,0 ]|)) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) by TOPREAL1:def 4, XBOOLE_1:4
.= ((LSeg p2,p1) \/ ((LSeg p2,|[0 ,0 ]|) \/ (LSeg |[0 ,1]|,p1))) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) by XBOOLE_1:4
.= (LSeg p2,p1) \/ (((LSeg p2,|[0 ,0 ]|) \/ (LSeg |[0 ,1]|,p1)) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4 ;
:: thesis: P1 /\ P2 = {p1,p2}
A105: p1 in LSeg |[0 ,1]|,p1 by RLTOPSP1:69;
p1 in LSeg p2,p1 by RLTOPSP1:69;
then p1 in (LSeg p2,p1) /\ (LSeg |[0 ,1]|,p1) by A105, XBOOLE_0:def 4;
then A106: {p1} c= (LSeg p2,p1) /\ (LSeg |[0 ,1]|,p1) by ZFMISC_1:37;
A107: P1 /\ P2 = ((LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|)) \/ ((LSeg p2,p1) /\ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p1))) by XBOOLE_1:23
.= ((LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|)) \/ (((LSeg p2,p1) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p2,p1) /\ (LSeg |[0 ,1]|,p1))) by XBOOLE_1:23
.= ((LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|)) \/ ((((LSeg p2,p1) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p2,p1) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p2,p1) /\ (LSeg |[0 ,1]|,p1))) by XBOOLE_1:23
.= ((LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|)) \/ (((((LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p2,p1) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p2,p1) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p2,p1) /\ (LSeg |[0 ,1]|,p1))) by XBOOLE_1:23
.= {p2} \/ (((((LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p2,p1) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p2,p1) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p2,p1) /\ (LSeg |[0 ,1]|,p1))) by A100, A92, XBOOLE_0:def 10
.= {p2} \/ (((((LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {} ) \/ ((LSeg p2,p1) /\ (LSeg |[1,1]|,|[0 ,1]|))) \/ ((LSeg p2,p1) /\ (LSeg |[0 ,1]|,p1))) by A20, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= {p2} \/ ((((LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p1}) by A106, A73, XBOOLE_0:def 10
.= {p2} \/ (((LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (((LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p1})) by XBOOLE_1:4
.= ({p2} \/ ((LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ (((LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p1}) by XBOOLE_1:4 ;

A108: now

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

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

p2 in LSeg p2,p1 by RLTOPSP1:69;
then (LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) <> {} by A109, Lm21, XBOOLE_0:def 4;
then (LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p2} by A85, A109, ZFMISC_1:39;
hence P1 /\ P2 = {p2} \/ (((LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p1}) by A107; :: thesis: verum

end;

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

now

assume |[0 ,0 ]| in (LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then |[0 ,0 ]| in LSeg p2,p1 by XBOOLE_0:def 4;
then p2 `2 <= |[0 ,0 ]| `2 by A15, A22, A72, TOPREAL1:10;
then |[0 ,0 ]| `2 = p2 `2 by A19, Lm5, Lm7, TOPREAL1:10;
hence contradiction by A22, A23, A110, Lm5, EUCLID:57; :: thesis: verum

end;

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

end;

end;

end;

A111: (LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A3, A19, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;

now

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

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

now

assume |[0 ,1]| in (LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then |[0 ,1]| in LSeg p2,p1 by XBOOLE_0:def 4;
then A113: |[0 ,1]| `2 <= p1 `2 by A15, A22, A72, TOPREAL1:10;
p1 `2 <= |[0 ,1]| `2 by A3, Lm5, Lm7, TOPREAL1:10;
then A114: |[0 ,1]| `2 = p1 `2 by A113, XXREAL_0:1;
p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57
.= |[0 ,1]| by A15, A16, A114, EUCLID:56 ;
hence contradiction by A112; :: thesis: verum

end;

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

end;

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

then |[0 ,1]| in LSeg p2,p1 by RLTOPSP1:69;
then (LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) <> {} by Lm23, XBOOLE_0:def 4;
then (LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) = {p1} by A111, A115, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A108, 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 A116: 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 A117: LSeg |[0 ,1]|,p2 c= LSeg |[0 ,1]|,|[1,1]| by Lm23, TOPREAL1:12;
LSeg p1,|[0 ,1]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, Lm22, TOPREAL1:12;
then A118: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A117, XBOOLE_1:27;
take P1 = (LSeg p1,|[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,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[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} )
A119: |[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
|[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
then A120: |[1,1]| in (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) by Lm27, XBOOLE_0:def 4;
|[0 ,1]| in LSeg p1,|[0 ,1]| by RLTOPSP1:69;
then (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} by A119, XBOOLE_0:def 4;
then A121: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) = {|[0 ,1]|} by A118, TOPREAL1:21, ZFMISC_1:39;
( p1 <> |[0 ,1]| or p2 <> |[0 ,1]| ) by A1;
hence P1 is_an_arc_of p1,p2 by A121, TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A122: LSeg |[0 ,0 ]|,|[0 ,1]| = (LSeg p1,|[0 ,1]|) \/ (LSeg p1,|[0 ,0 ]|) by A3, TOPREAL1:11;
A123: LSeg |[1,0 ]|,|[1,1]| is_an_arc_of |[1,0 ]|,|[1,1]| by Lm9, Lm11, TOPREAL1:15;
LSeg |[0 ,0 ]|,|[1,0 ]| is_an_arc_of |[0 ,0 ]|,|[1,0 ]| by Lm4, Lm8, TOPREAL1:15;
then A124: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[0 ,0 ]|,|[1,1]| by A123, TOPREAL1:5, TOPREAL1:22;
A125: LSeg |[1,1]|,p2 c= LSeg |[0 ,1]|,|[1,1]| by A116, Lm26, TOPREAL1:12;
then A126: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by XBOOLE_1:27;
A127: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A125, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) /\ (LSeg |[1,1]|,p2) = ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2)) by XBOOLE_1:23
.= {|[1,1]|} by A127, A126, A120, TOPREAL1:24, ZFMISC_1:39 ;
then A128: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2) is_an_arc_of |[0 ,0 ]|,p2 by A124, TOPREAL1:16;
A129: (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,1]|,p2) = {p2} by A116, TOPREAL1:14;
A130: LSeg |[0 ,1]|,|[1,1]| = (LSeg |[1,1]|,p2) \/ (LSeg |[0 ,1]|,p2) by A116, TOPREAL1:11;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) c= {|[0 ,1]|} by A4, A125, TOPREAL1:21, XBOOLE_1:27;
then A131: ( (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) = {|[0 ,1]|} or (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) = {} ) by ZFMISC_1:39;
A132: LSeg |[0 ,1]|,p2 c= LSeg |[0 ,1]|,|[1,1]| by A116, Lm23, TOPREAL1:12;
then A133: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by Lm2, XBOOLE_1:3, XBOOLE_1:27;
A134: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) by A116, TOPREAL1:19;

A135: now

A136: p2 `1 <= |[1,1]| `1 by A134, EUCLID:56;
assume A137: |[0 ,1]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) ; :: thesis: contradiction
then A138: |[0 ,1]| in LSeg |[0 ,0 ]|,p1 by XBOOLE_0:def 4;
|[0 ,1]| in LSeg p2,|[1,1]| by A137, XBOOLE_0:def 4;
then A139: |[0 ,1]| `1 = p2 `1 by A134, A136, Lm6, TOPREAL1:9;
|[0 ,0 ]| `2 <= p1 `2 by A15, A18, EUCLID:56;
then |[0 ,1]| `2 <= p1 `2 by A138, TOPREAL1:10;
then |[0 ,1]| `2 = p1 `2 by A15, A17, Lm7, XXREAL_0:1;
then p1 = |[(|[0 ,1]| `1 ),(|[0 ,1]| `2 )]| by A15, A16, Lm6, EUCLID:57
.= p2 by A134, A139, Lm7, EUCLID:57 ;
hence contradiction by A1; :: thesis: verum

end;

(LSeg p1,|[0 ,0 ]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)) = ((LSeg p1,|[0 ,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) by A131, A135, XBOOLE_1:23, ZFMISC_1:37
.= {|[0 ,0 ]|} by A9, A5, A6, TOPREAL1:23, XBOOLE_0:def 10 ;
hence P2 is_an_arc_of p1,p2 by A128, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg |[0 ,1]|,p2) \/ ((LSeg p1,|[0 ,1]|) \/ ((LSeg p1,|[0 ,0 ]|) \/ (((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 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) \/ (LSeg |[0 ,1]|,p2) by A122, XBOOLE_1:4
.= (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)) \/ (LSeg |[0 ,1]|,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 A130, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A140: {p1} = (LSeg p1,|[0 ,1]|) /\ (LSeg p1,|[0 ,0 ]|) by A3, TOPREAL1:14;
A141: P1 /\ P2 = ((LSeg p1,|[0 ,1]|) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by XBOOLE_1:23
.= (((LSeg p1,|[0 ,1]|) /\ (LSeg p1,|[0 ,0 ]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,1]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by A140, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[0 ,0 ]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ ((LSeg |[0 ,1]|,p2) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ (((LSeg |[0 ,1]|,p2) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2})) by A129, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ ((((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})) by A14, A133 ;

A142: now

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

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

then A144: not p2 in LSeg p1,|[0 ,1]| by A13, Lm4, Lm6, Lm10, TOPREAL1:9;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = (LSeg p1,|[0 ,1]|) /\ {p2} by A143, RLTOPSP1:71
.= {} by A144, Lm1 ;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ {p2}) by A141, A143, TOPREAL1:24; :: thesis: verum

end;

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

now

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

end;

then A147: {|[0 ,1]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) c= {|[0 ,1]|} by A13, A125, TOPREAL1:21, XBOOLE_1:27;
then A148: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {} by A147, ZFMISC_1:39;

now

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

end;

then A150: {|[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 A132, TOPREAL1:24, XBOOLE_1:27;
then (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A150, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ {p2}) by A141, A148; :: thesis: verum

end;

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

then p2 in LSeg p1,|[0 ,1]| by RLTOPSP1:69;
then A152: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) <> {} by A151, Lm23, XBOOLE_0:def 4;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) c= {p2} by A13, A151, TOPREAL1:21, XBOOLE_1:27;
then A153: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {p2} by A152, ZFMISC_1:39;
(LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[0 ,1]|} /\ (LSeg |[1,0 ]|,|[1,1]|) by A151, RLTOPSP1:71
.= {} by Lm1, Lm15 ;
hence P1 /\ P2 = (({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2}) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ {p2}) by A141, A153, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ {p2}) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ ({p2} \/ {p2})) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ {p2}) ;
:: thesis: verum

end;

end;

end;

now

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

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

then p1 in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then A155: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) <> {} by A154, Lm22, XBOOLE_0:def 4;
(LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) c= {p1} by A132, A154, TOPREAL1:21, XBOOLE_1:27;
then A156: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = {p1} by A155, ZFMISC_1:39;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p1} /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A154, RLTOPSP1:71
.= {} by A154, Lm1, Lm14 ;
hence P1 /\ P2 = ({p1} \/ {p1}) \/ {p2} by A142, A156, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

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

A158: not |[0 ,0 ]| in LSeg |[0 ,1]|,p2 by A132, Lm5, Lm7, Lm11, TOPREAL1:10;
(LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = (LSeg |[0 ,1]|,p2) /\ {|[0 ,0 ]|} by A157, RLTOPSP1:71
.= {} by A158, Lm1 ;
hence P1 /\ P2 = {p1,p2} by A142, A157, ENUMSET1:41, TOPREAL1:23; :: thesis: verum

end;

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

now

assume |[0 ,1]| in (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) ; :: thesis: contradiction
then A160: |[0 ,1]| in LSeg |[0 ,0 ]|,p1 by XBOOLE_0:def 4;
|[0 ,0 ]| `2 <= p1 `2 by A15, A18, EUCLID:56;
then |[0 ,1]| `2 <= p1 `2 by A160, TOPREAL1:10;
then p1 `2 = 1 by A15, A17, Lm7, XXREAL_0:1;
hence contradiction by A15, A16, A159, EUCLID:57; :: thesis: verum

end;

then A161: {|[0 ,1]|} <> (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) by ZFMISC_1:37;
(LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) c= {|[0 ,1]|} by A4, A132, TOPREAL1:21, XBOOLE_1:27;
then A162: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = {} by A161, ZFMISC_1:39;

now

assume |[0 ,0 ]| in (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then A163: |[0 ,0 ]| in LSeg p1,|[0 ,1]| by XBOOLE_0:def 4;
p1 `2 <= |[0 ,1]| `2 by A15, A17, EUCLID:56;
then p1 `2 = 0 by A15, A18, A163, Lm5, TOPREAL1:10;
hence contradiction by A15, A16, A159, EUCLID:57; :: thesis: verum

end;

then A164: {|[0 ,0 ]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A13, TOPREAL1:23, XBOOLE_1:27;
then (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A164, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A142, A162, ENUMSET1:41; :: thesis: verum

end;

end;

end;

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

end;

suppose A165: 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 A166: LSeg |[0 ,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| by Lm21, TOPREAL1:12;
LSeg p1,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, Lm20, TOPREAL1:12;
then A167: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A166, XBOOLE_1:27;
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,|[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 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A168: |[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then A169: |[1,0 ]| in (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) by Lm25, XBOOLE_0:def 4;
|[0 ,0 ]| in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
then (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} by A168, XBOOLE_0:def 4;
then A170: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|} by A167, TOPREAL1:23, ZFMISC_1:39;
( p1 <> |[0 ,0 ]| or |[0 ,0 ]| <> p2 ) by A1;
hence P1 is_an_arc_of p1,p2 by A170, TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A171: LSeg |[0 ,0 ]|,|[0 ,1]| = (LSeg p1,|[0 ,0 ]|) \/ (LSeg p1,|[0 ,1]|) by A3, TOPREAL1:11;
A172: LSeg |[1,0 ]|,|[1,1]| is_an_arc_of |[1,1]|,|[1,0 ]| by Lm9, Lm11, TOPREAL1:15;
LSeg |[0 ,1]|,|[1,1]| is_an_arc_of |[0 ,1]|,|[1,1]| by Lm6, Lm10, TOPREAL1:15;
then A173: (LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[0 ,1]|,|[1,0 ]| by A172, TOPREAL1:5, TOPREAL1:24;
A174: LSeg |[1,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| by A165, Lm24, TOPREAL1:12;
then A175: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by XBOOLE_1:27;
A176: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A174, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) /\ (LSeg |[1,0 ]|,p2) = ((LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= {|[1,0 ]|} by A176, A175, A169, TOPREAL1:22, ZFMISC_1:39 ;
then A177: ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[0 ,1]|,p2 by A173, TOPREAL1:16;
A178: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,p2) = {p2} by A165, TOPREAL1:14;
A179: LSeg |[0 ,0 ]|,|[1,0 ]| = (LSeg |[1,0 ]|,p2) \/ (LSeg |[0 ,0 ]|,p2) by A165, TOPREAL1:11;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) c= {|[0 ,0 ]|} by A13, A174, TOPREAL1:23, XBOOLE_1:27;
then A180: ( (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {|[0 ,0 ]|} or (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {} ) by ZFMISC_1:39;
A181: LSeg |[0 ,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| by A165, Lm21, TOPREAL1:12;
then A182: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by Lm2, XBOOLE_1:3, XBOOLE_1:27;
A183: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 0 ) by A165, TOPREAL1:19;

A184: now

A185: p2 `1 <= |[1,0 ]| `1 by A183, EUCLID:56;
assume A186: |[0 ,0 ]| in (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) ; :: thesis: contradiction
then A187: |[0 ,0 ]| in LSeg p1,|[0 ,1]| by XBOOLE_0:def 4;
|[0 ,0 ]| in LSeg p2,|[1,0 ]| by A186, XBOOLE_0:def 4;
then A188: |[0 ,0 ]| `1 = p2 `1 by A183, A185, Lm4, TOPREAL1:9;
p1 `2 <= |[0 ,1]| `2 by A15, A17, EUCLID:56;
then |[0 ,0 ]| `2 = p1 `2 by A15, A18, A187, Lm5, TOPREAL1:10;
then p1 = |[(|[0 ,0 ]| `1 ),(|[0 ,0 ]| `2 )]| by A15, A16, Lm4, EUCLID:57
.= p2 by A183, A188, Lm5, EUCLID:57 ;
hence contradiction by A1; :: thesis: verum

end;

(LSeg p1,|[0 ,1]|) /\ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)) = ((LSeg p1,|[0 ,1]|) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[0 ,1]|,p1) /\ (LSeg |[1,0 ]|,|[1,1]|)) by A180, A184, XBOOLE_1:23, ZFMISC_1:37
.= {|[0 ,1]|} by A14, A10, A12, XBOOLE_0:def 10 ;
hence P2 is_an_arc_of p1,p2 by A177, 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,|[0 ,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)))) by XBOOLE_1:4
.= ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2))) \/ (LSeg |[0 ,0 ]|,p2) by A171, XBOOLE_1:4
.= (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ ((((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)) \/ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:4
.= (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg |[1,0 ]|,p2) \/ (LSeg |[0 ,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 A179, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A189: {p1} = (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) by A3, TOPREAL1:14;
A190: P1 /\ P2 = ((LSeg p1,|[0 ,0 ]|) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)))) \/ ((LSeg |[0 ,0 ]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)))) by XBOOLE_1:23
.= (((LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)))) \/ ((LSeg |[0 ,0 ]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,0 ]|) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2)))) \/ ((LSeg |[0 ,0 ]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)))) by A189, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2)))) \/ ((LSeg |[0 ,0 ]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2)))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[0 ,0 ]|,p2) /\ (((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2)))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ (((LSeg |[0 ,0 ]|,p2) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2})) by A178, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2)))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ ((((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2)))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})) by A9, A182 ;

A191: now

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

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

then not p2 in LSeg p1,|[0 ,0 ]| by A4, Lm4, Lm6, Lm8, TOPREAL1:9;
then A193: LSeg p1,|[0 ,0 ]| misses {p2} by ZFMISC_1:56;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) = (LSeg p1,|[0 ,0 ]|) /\ {p2} by A192, RLTOPSP1:71
.= {} by A193, XBOOLE_0:def 7 ;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) by A190, A192, TOPREAL1:22; :: thesis: verum

end;

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

now

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

end;

then A196: {|[0 ,0 ]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {|[0 ,0 ]|} by A4, A174, TOPREAL1:23, XBOOLE_1:27;
then A197: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {} by A196, ZFMISC_1:39;

now

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

end;

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

end;

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

then p2 in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
then A201: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} by A200, Lm21, XBOOLE_0:def 4;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {p2} by A4, A200, TOPREAL1:23, XBOOLE_1:27;
then A202: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {p2} by A201, ZFMISC_1:39;
(LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[0 ,0 ]|} /\ (LSeg |[1,0 ]|,|[1,1]|) by A200, RLTOPSP1:71
.= {} by Lm1, Lm12 ;
hence P1 /\ P2 = (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2}) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) by A190, A202, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ ({p2} \/ {p2})) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) ;
:: thesis: verum

end;

end;

end;

now

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

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

then A204: (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = (LSeg |[0 ,0 ]|,p2) /\ {p1} by RLTOPSP1:71;
not p1 in LSeg |[0 ,0 ]|,p2 by A181, A203, Lm5, Lm7, Lm9, TOPREAL1:10;
then (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A204, Lm1;
hence P1 /\ P2 = {p1,p2} by A191, A203, ENUMSET1:41, TOPREAL1:21; :: thesis: verum

end;

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

|[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
then A206: (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) <> {} by A205, Lm20, XBOOLE_0:def 4;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {p1} /\ (LSeg |[0 ,1]|,|[1,1]|) by A205, RLTOPSP1:71;
then A207: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A205, Lm1, Lm13;
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A165, A205, Lm21, TOPREAL1:12, XBOOLE_1:26;
then (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = {p1} by A205, A206, TOPREAL1:23, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ {p1}) \/ {p2} by A191, A207, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

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

now

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

end;

then A210: {|[0 ,0 ]|} <> (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A13, A181, XBOOLE_1:27;
then A211: (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A210, TOPREAL1:23, ZFMISC_1:39;

now

assume |[0 ,1]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then A212: |[0 ,1]| in LSeg |[0 ,0 ]|,p1 by XBOOLE_0:def 4;
|[0 ,0 ]| `2 <= p1 `2 by A15, A18, EUCLID:56;
then |[0 ,1]| `2 <= p1 `2 by A212, TOPREAL1:10;
then p1 `2 = 1 by A15, A17, Lm7, XXREAL_0:1;
hence contradiction by A15, A16, A208, EUCLID:57; :: thesis: verum

end;

then A213: {|[0 ,1]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A4, TOPREAL1:21, XBOOLE_1:27;
then (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A213, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A191, A211, ENUMSET1:41; :: thesis: verum

end;

end;

end;

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

end;

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

now

let a be set ; :: thesis: ( a in (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) implies a in {p1} )
assume A215: a in (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
a in LSeg p1,|[0 ,1]| by A215, XBOOLE_0:def 4;
then A216: p1 `2 <= p `2 by A15, A17, Lm7, TOPREAL1:10;
A217: a in LSeg |[0 ,0 ]|,p1 by A215, XBOOLE_0:def 4;
then p `2 <= p1 `2 by A15, A18, Lm5, TOPREAL1:10;
then A218: p `2 = p1 `2 by A216, XXREAL_0:1;
p `1 <= p1 `1 by A15, A16, A217, Lm4, TOPREAL1:9;
then p `1 = p1 `1 by A15, A16, A217, Lm4, TOPREAL1:9;
then a = |[(p1 `1 ),(p1 `2 )]| by A218, EUCLID:57
.= p1 by EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

then A219: (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) c= {p1} by TARSKI:def 3;
A220: p2 in LSeg |[1,1]|,p2 by RLTOPSP1:69;
p2 in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then p2 in (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) by A220, XBOOLE_0:def 4;
then A221: {p2} c= (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
A222: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) by A214, TOPREAL1:19;

now

let a be set ; :: thesis: ( a in (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) implies a in {p2} )
assume A223: a in (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A224: a in LSeg |[1,0 ]|,p2 by A223, XBOOLE_0:def 4;
then A225: p2 `1 <= p `1 by A222, Lm8, TOPREAL1:9;
a in LSeg p2,|[1,1]| by A223, XBOOLE_0:def 4;
then A226: p2 `2 <= p `2 by A222, Lm11, TOPREAL1:10;
p `1 <= p2 `1 by A222, A224, Lm8, TOPREAL1:9;
then A227: p `1 = p2 `1 by A225, XXREAL_0:1;
p `2 <= p2 `2 by A222, A224, Lm9, TOPREAL1:10;
then p `2 = p2 `2 by A226, XXREAL_0:1;
then a = |[(p2 `1 ),(p2 `2 )]| by A227, EUCLID:57
.= p2 by EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

then A228: (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) c= {p2} by TARSKI:def 3;
LSeg |[1,0 ]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A214, Lm25, TOPREAL1:12;
then A229: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,0 ]|} by TOPREAL1:22, XBOOLE_1:27;
take P1 = ((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[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 ,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} )
A230: |[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
|[1,0 ]| in LSeg |[0 ,0 ]|,|[1,0 ]| by RLTOPSP1:69;
then (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} by A230, XBOOLE_0:def 4;
then (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} by A229, ZFMISC_1:39;
then A231: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[0 ,0 ]|,p2 by Lm4, Lm8, TOPREAL1:18;
LSeg |[1,0 ]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A214, Lm25, TOPREAL1:12;
then A232: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {} by A4, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg p1,|[0 ,0 ]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,p2)) = ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= {|[0 ,0 ]|} by A5, A6, A232, TOPREAL1:23, XBOOLE_0:def 10 ;
then (LSeg p1,|[0 ,0 ]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,p2)) is_an_arc_of p1,p2 by A231, 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 A233: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} by Lm26, XBOOLE_0:def 4;
A234: LSeg |[1,1]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A214, Lm27, TOPREAL1:12;
then A235: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {} by A13, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= {|[1,1]|} by A234, TOPREAL1:24, XBOOLE_1:27;
then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} by A233, ZFMISC_1:39;
then A236: (LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,1]|,p2) is_an_arc_of |[0 ,1]|,p2 by Lm6, Lm10, TOPREAL1:18;
(LSeg p1,|[0 ,1]|) /\ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,1]|,p2)) = ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)) by XBOOLE_1:23
.= {|[0 ,1]|} by A10, A12, A235, XBOOLE_0:def 10 ;
then (LSeg p1,|[0 ,1]|) \/ ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,1]|,p2)) is_an_arc_of p1,p2 by A236, 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 p1,|[0 ,0 ]|) \/ (LSeg p1,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) by A3, TOPREAL1:11, TOPREAL1:def 4
.= ((LSeg p1,|[0 ,0 ]|) \/ ((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) by XBOOLE_1:4
.= (LSeg p1,|[0 ,0 ]|) \/ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) by XBOOLE_1:4
.= (LSeg p1,|[0 ,0 ]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|))) by XBOOLE_1:4
.= ((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) by XBOOLE_1:4
.= ((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ ((LSeg |[1,1]|,p2) \/ (LSeg |[1,0 ]|,p2))) by A214, TOPREAL1:11
.= ((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg |[1,0 ]|,p2) \/ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A237: p1 in LSeg p1,|[0 ,1]| by RLTOPSP1:69;
p1 in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
then p1 in (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) by A237, XBOOLE_0:def 4;
then {p1} c= (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) by ZFMISC_1:37;
then A238: (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) = {p1} by A219, XBOOLE_0:def 10;
A239: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A4, A234, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A240: LSeg |[1,0 ]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A214, Lm25, TOPREAL1:12;
then A241: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A13, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A242: P1 /\ P2 = (((LSeg p1,|[0 ,0 ]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by XBOOLE_1:23
.= (((LSeg p1,|[0 ,0 ]|) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by XBOOLE_1:23
.= ((((LSeg p1,|[0 ,0 ]|) /\ ((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by XBOOLE_1:23
.= ((((LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by A239, XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ ((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by A238, XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2))) by Lm2, XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2}) by A221, A228, XBOOLE_0:def 10
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ ((((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p2}) by A241 ;

A243: now

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

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

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

end;

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

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

end;

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

now

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

end;

then A248: {|[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 A240, XBOOLE_1:27;
then A249: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A248, TOPREAL1:24, ZFMISC_1:39;

now

assume |[1,0 ]| in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) ; :: thesis: contradiction
then A250: |[1,0 ]| in LSeg p2,|[1,1]| by XBOOLE_0:def 4;
p2 `2 <= |[1,1]| `2 by A222, EUCLID:56;
then p2 `2 = |[1,0 ]| `2 by A222, A250, Lm9, TOPREAL1:10;
then p2 = |[(|[1,0 ]| `1 ),(|[1,0 ]| `2 )]| by A222, Lm8, EUCLID:57
.= |[1,0 ]| by EUCLID:57 ;
hence contradiction by A246; :: thesis: verum

end;

then A251: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) <> {|[1,0 ]|} by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= {|[1,0 ]|} by A234, TOPREAL1:22, XBOOLE_1:27;
then (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A251, ZFMISC_1:39;
hence P1 /\ P2 = (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|))) \/ {p2} by A242, A249; :: thesis: verum

end;

end;

end;

now

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

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

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

end;

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

now

assume |[0 ,1]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) ; :: thesis: contradiction
then A254: |[0 ,1]| in LSeg |[0 ,0 ]|,p1 by XBOOLE_0:def 4;
|[0 ,0 ]| `2 <= p1 `2 by A15, A18, EUCLID:56;
then |[0 ,1]| `2 <= p1 `2 by A254, TOPREAL1:10;
then p1 `2 = |[0 ,1]| `2 by A15, A17, Lm7, XXREAL_0:1;
then p1 = |[(|[0 ,1]| `1 ),(|[0 ,1]| `2 )]| by A15, A16, Lm6, EUCLID:57
.= |[0 ,1]| by EUCLID:57 ;
hence contradiction by A253; :: thesis: verum

end;

then A255: {|[0 ,1]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A4, TOPREAL1:21, XBOOLE_1:27;
then A256: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A255, ZFMISC_1:39;

now

assume |[0 ,0 ]| in (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|) ; :: thesis: contradiction
then |[0 ,0 ]| in LSeg p1,|[0 ,1]| by XBOOLE_0:def 4;
then p1 `2 = |[0 ,0 ]| `2 by A15, A17, A18, Lm5, Lm7, TOPREAL1:10;
then p1 = |[(|[0 ,0 ]| `1 ),(|[0 ,0 ]| `2 )]| by A15, A16, Lm4, EUCLID:57
.= |[0 ,0 ]| by EUCLID:57 ;
hence contradiction by A253; :: thesis: verum

end;

then A257: {|[0 ,0 ]|} <> (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|) by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A13, XBOOLE_1:27;
then (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|) = {} by A257, TOPREAL1:23, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A243, A256, ENUMSET1:41; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

end;