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: ( 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 = 0 & p `2 <= 1 & p `2 >= 0 ) by A3, TOPREAL1:19;
A7: LSeg |[0 ,0 ]|,p1 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, Lm13, TOPREAL1:12;
A8: LSeg p1,|[0 ,1]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, Lm15, TOPREAL1:12;
A9: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by TOPREAL1:26, XBOOLE_0:def 7;
then A10: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A7, XBOOLE_1:3, XBOOLE_1:26;
|[0 ,0 ]| in LSeg p1,|[0 ,0 ]| by RLTOPSP1:69;
then |[0 ,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by Lm14, XBOOLE_0:def 4;
then A11: {|[0 ,0 ]|} c= (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
A12: ( (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[0 ,0 ]|} ) by A3, Lm13, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
then A13: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[0 ,0 ]|} by A11, XBOOLE_0:def 10;
A14: (LSeg |[0 ,1]|,p1) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A8, A9, 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 Lm16, XBOOLE_0:def 4;
then A15: {|[0 ,1]|} c= (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
A16: (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A3, Lm15, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;

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

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

then consider q being Point of (TOP-REAL 2) such that
A18: q = p2 and
A19: ( q `1 = 0 & q `2 <= 1 & q `2 >= 0 ) by TOPREAL1:19;
A20: LSeg p2,p1 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, A17, TOPREAL1:12;
A21: ( p = |[(p `1 ),(p `2 )]| & q = |[(q `1 ),(q `2 )]| ) by EUCLID:57;

now

per cases ( p `2 < q `2 or p `2 > q `2 ) by A1, A5, A6, A18, A19, A21, XXREAL_0:1;

case A22: 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} )

A23: LSeg |[0 ,1]|,p2 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A17, Lm15, TOPREAL1:12;
A24: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A17, Lm15, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
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));

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 A18, A19, EUCLID:56, XBOOLE_0:def 4;
hence contradiction by A6, A18, A22, Lm4, TOPREAL1:10; :: thesis: verum

end;

then {|[0 ,0 ]|} <> (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
then A25: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A24, ZFMISC_1:39;

A26: now

assume A27: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2) <> {} ; :: thesis: contradiction
consider a being Element of (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,p2);
reconsider p = a as Point of (TOP-REAL 2) by A27, TARSKI:def 3;
( p in LSeg |[0 ,0 ]|,p1 & p in LSeg p2,|[0 ,1]| & |[0 ,0 ]| `2 <= p1 `2 & p2 `2 <= |[0 ,1]| `2 ) by A5, A6, A18, A19, A27, EUCLID:56, XBOOLE_0:def 4;
then ( p `2 <= p1 `2 & p2 `2 <= p `2 ) by TOPREAL1:10;
hence contradiction by A5, A18, A22, 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 Lm16, XBOOLE_0:def 4;
then A28: {|[0 ,1]|} c= (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
A29: ( (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {|[0 ,1]|} ) by A17, Lm15, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
A30: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A3, Lm13, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;

now

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

end;

then A31: {|[0 ,1]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
A32: ((LSeg |[0 ,1]|,p2) \/ (LSeg p2,p1)) \/ (LSeg p1,|[0 ,0 ]|) = LSeg |[0 ,0 ]|,|[0 ,1]| by A3, A17, TOPREAL1:13;
A33: LSeg p1,p2 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A3, A17, TOPREAL1:12;
( p1 in LSeg p1,p2 & p1 in LSeg p1,|[0 ,0 ]| ) by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) by XBOOLE_0:def 4;
then A34: {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) by ZFMISC_1:37;
(LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) c= {p1}

proof

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

end;

then A36: (LSeg p1,p2) /\ (LSeg p1,|[0 ,0 ]|) = {p1} by A34, XBOOLE_0:def 10;
( p2 in LSeg p1,p2 & p2 in LSeg |[0 ,1]|,p2 ) by RLTOPSP1:69;
then p2 in (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) by XBOOLE_0:def 4;
then A37: {p2} c= (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
(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 A38: a in (LSeg p1,p2) /\ (LSeg |[0 ,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,|[0 ,1]| & p1 `2 <= p2 `2 & p1 `1 <= p2 `1 & p2 `2 <= |[0 ,1]| `2 ) by A5, A6, A18, A19, A22, A38, EUCLID:56, XBOOLE_0:def 4;
then ( p1 `1 <= p `1 & p `1 <= p2 `1 & p2 `2 <= p `2 & p `2 <= p2 `2 ) by TOPREAL1:9, TOPREAL1:10;
then ( p2 `2 = p `2 & p `1 = 0 ) by A5, A6, A18, A19, XXREAL_0:1;
then p = |[0 ,(p2 `2 )]| by EUCLID:57
.= p2 by A18, A19, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

then A39: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) = {p2} by A37, 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} )
A40: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[0 ,0 ]|,|[1,1]| by Lm4, TOPREAL1:18, TOPREAL1:22;
((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]|} ;
then A41: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|) is_an_arc_of |[0 ,0 ]|,|[0 ,1]| by A40, 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 A25, XBOOLE_1:23
.= {} \/ ((LSeg |[0 ,1]|,p2) /\ (LSeg |[1,1]|,|[0 ,1]|)) by A23, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= {|[0 ,1]|} by A28, A29, XBOOLE_0:def 10 ;
then A42: (((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 A41, 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 A10, A13, A26, A30, A31, 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 A42, 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} )
thus 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 A32, 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}
A43: (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 A36, 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 A33, 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 A39, 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 ;
A44: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A3, A17, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;

A45: now

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

suppose A46: 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 Lm14, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p1} by A44, A46, 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 A43; :: thesis: verum

end;

suppose A47: 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 & p1 `2 <= p2 `2 & |[0 ,0 ]| `2 <= |[0 ,1]| `2 ) by A5, A18, A22, Lm4, XBOOLE_0:def 4;
then ( |[0 ,0 ]| `2 <= p1 `2 & p1 `2 <= |[0 ,0 ]| `2 ) by A3, TOPREAL1:10;
then |[0 ,0 ]| `2 = p1 `2 by XXREAL_0:1;
hence contradiction by A5, A6, A47, Lm4, 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 A43; :: thesis: verum

end;

end;

end;

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

now

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

suppose A49: 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 & p1 `2 <= p2 `2 & |[0 ,0 ]| `2 <= |[0 ,1]| `2 ) by A5, A18, A22, Lm4, XBOOLE_0:def 4;
then ( |[0 ,1]| `2 <= p2 `2 & p2 `2 <= |[0 ,1]| `2 ) by A17, TOPREAL1:10;
then A50: |[0 ,1]| `2 = p2 `2 by XXREAL_0:1;
p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57
.= |[0 ,1]| by A18, A19, A50, EUCLID:56 ;
hence contradiction by A49; :: 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 A48, 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 A45, ENUMSET1:41; :: thesis: verum

end;

suppose A51: 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 Lm16, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {p2} by A48, A51, 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 A45, 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 A52: 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} )

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} )
A53: (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A3, Lm15, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;

now

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

end;

then A54: {|[0 ,0 ]|} <> (LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
A55: LSeg p2,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A17, Lm13, TOPREAL1:12;

A56: now

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

end;

|[0 ,0 ]| in LSeg p2,|[0 ,0 ]| by RLTOPSP1:69;
then |[0 ,0 ]| in (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by Lm14, XBOOLE_0:def 4;
then A58: {|[0 ,0 ]|} c= (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
A59: (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A17, Lm13, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
A60: (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A17, Lm13, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;

now

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

end;

then A61: {|[0 ,1]|} <> (LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
A62: ((LSeg |[0 ,1]|,p1) \/ (LSeg p1,p2)) \/ (LSeg p2,|[0 ,0 ]|) = LSeg |[0 ,0 ]|,|[0 ,1]| by A3, A17, TOPREAL1:13;
( p2 in LSeg p2,p1 & p2 in LSeg p2,|[0 ,0 ]| ) by RLTOPSP1:69;
then p2 in (LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|) by XBOOLE_0:def 4;
then A63: {p2} c= (LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|) by ZFMISC_1:37;
A64: (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 A65: a in (LSeg p2,p1) /\ (LSeg p2,|[0 ,0 ]|) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
( p in LSeg p2,p1 & p in LSeg |[0 ,0 ]|,p2 & p2 `2 <= p1 `2 & p2 `1 <= p1 `1 & |[0 ,0 ]| `2 <= p2 `2 ) by A5, A6, A18, A19, A52, A65, EUCLID:56, XBOOLE_0:def 4;
then ( p2 `1 <= p `1 & p `1 <= p1 `1 & p2 `2 <= p `2 & p `2 <= p2 `2 ) by TOPREAL1:9, TOPREAL1:10;
then ( p2 `2 = p `2 & p `1 = 0 ) by A5, A6, A18, A19, XXREAL_0:1;
then p = |[0 ,(p2 `2 )]| by EUCLID:57
.= p2 by A18, A19, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

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

end;

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} )
A69: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by Lm4, TOPREAL1:18, TOPREAL1:22;
(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]|} ;
then A70: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,|[0 ,1]|) is_an_arc_of |[0 ,1]|,|[0 ,0 ]| by A69, TOPREAL1:17;
(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 A53, A54, ZFMISC_1:39
.= {|[0 ,1]|} by A14, A15, A16, XBOOLE_0:def 10 ;
then A71: (((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 A70, 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 A55, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= ((LSeg p2,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {} by A56, A60, A61, ZFMISC_1:39
.= {|[0 ,0 ]|} by A58, A59, XBOOLE_0:def 10 ;
hence P2 is_an_arc_of p1,p2 by A71, TOPREAL1:16; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus 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 A62, 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}
A72: 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 A63, A64, 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 A66, A67, 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 ;
A73: (LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A3, A17, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;

A74: now

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

suppose A75: 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 A75, Lm14, XBOOLE_0:def 4;
then (LSeg p2,p1) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p2} by A73, A75, ZFMISC_1:39;
hence P1 /\ P2 = {p2} \/ (((LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p1}) by A72; :: thesis: verum

end;

suppose A76: 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 & p2 `2 <= p1 `2 & |[0 ,0 ]| `2 <= |[0 ,1]| `2 ) by A5, A18, A52, Lm4, XBOOLE_0:def 4;
then ( |[0 ,0 ]| `2 <= p2 `2 & p2 `2 <= |[0 ,0 ]| `2 ) by A17, TOPREAL1:10;
then |[0 ,0 ]| `2 = p2 `2 by XXREAL_0:1;
hence contradiction by A18, A19, A76, Lm4, 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 A73, ZFMISC_1:39;
hence P1 /\ P2 = {p2} \/ (((LSeg p2,p1) /\ (LSeg |[0 ,1]|,|[1,1]|)) \/ {p1}) by A72; :: thesis: verum

end;

end;

end;

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

now

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

suppose A78: 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 & p2 `2 <= p1 `2 & |[0 ,0 ]| `2 <= |[0 ,1]| `2 ) by A5, A18, A52, Lm4, XBOOLE_0:def 4;
then ( |[0 ,1]| `2 <= p1 `2 & p1 `2 <= |[0 ,1]| `2 ) by A3, TOPREAL1:10;
then A79: |[0 ,1]| `2 = p1 `2 by XXREAL_0:1;
p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57
.= |[0 ,1]| by A5, A6, A79, EUCLID:56 ;
hence contradiction by A78; :: 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 A77, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A74, ENUMSET1:41; :: thesis: verum

end;

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

A90: now

assume |[0 ,1]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) ; :: thesis: contradiction
then ( |[0 ,1]| in LSeg |[0 ,0 ]|,p1 & |[0 ,1]| in LSeg p2,|[1,1]| & |[0 ,0 ]| `2 <= p1 `2 & p2 `1 <= |[1,1]| `1 ) by A5, A6, A82, EUCLID:56, XBOOLE_0:def 4;
then ( |[0 ,1]| `2 <= p1 `2 & p2 `1 <= |[0 ,1]| `1 ) by TOPREAL1:9, TOPREAL1:10;
then A91: ( |[0 ,1]| `2 = p1 `2 & |[0 ,1]| `2 = p2 `2 & |[0 ,1]| `1 = p1 `1 & |[0 ,1]| `1 = p2 `1 ) by A5, A6, A82, Lm4, XXREAL_0:1;
then p1 = |[(|[0 ,1]| `1 ),(|[0 ,1]| `2 )]| by EUCLID:57
.= p2 by A91, 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 A89, A90, XBOOLE_1:23, ZFMISC_1:37
.= {|[0 ,0 ]|} by A10, A11, A12, XBOOLE_0:def 10 ;
hence P2 is_an_arc_of p1,p2 by A88, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A92: LSeg |[0 ,0 ]|,|[0 ,1]| = (LSeg p1,|[0 ,1]|) \/ (LSeg p1,|[0 ,0 ]|) by A3, TOPREAL1:11;
A93: LSeg |[0 ,1]|,|[1,1]| = (LSeg |[1,1]|,p2) \/ (LSeg |[0 ,1]|,p2) by A81, TOPREAL1:11;
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 A92, 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 A93, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A94: LSeg |[0 ,1]|,p2 c= LSeg |[0 ,1]|,|[1,1]| by A81, Lm16, TOPREAL1:12;
A95: {p1} = (LSeg p1,|[0 ,1]|) /\ (LSeg p1,|[0 ,0 ]|) by A3, TOPREAL1:14;
A96: (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,1]|,p2) = {p2} by A81, TOPREAL1:14;
A97: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A94, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A98: 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 A95, 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 A96, 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, A97 ;

A99: now

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

suppose A100: 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 A101: not p2 in LSeg p1,|[0 ,1]| by A8, Lm4, TOPREAL1:9;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = (LSeg p1,|[0 ,1]|) /\ {p2} by A100, RLTOPSP1:71
.= {} by A101, Lm1 ;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ {p2}) by A98, A100, TOPREAL1:24; :: thesis: verum

end;

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

A103: (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,1]|} by A94, TOPREAL1:24, XBOOLE_1:27;

now

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

end;

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

now

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

end;

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

end;

suppose A106: 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 A107: (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[0 ,1]|} /\ (LSeg |[1,0 ]|,|[1,1]|) by RLTOPSP1:71
.= {} by Lm1, Lm8 ;
A108: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) c= {p2} by A8, A106, TOPREAL1:21, XBOOLE_1:27;
p2 in LSeg p1,|[0 ,1]| by A106, RLTOPSP1:69;
then (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) <> {} by A106, Lm16, XBOOLE_0:def 4;
then (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {p2} by A108, ZFMISC_1:39;
hence P1 /\ P2 = (({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2}) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|)) \/ {p2}) by A98, A107, 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 A109: p1 = |[0 ,1]| ; :: thesis: P1 /\ P2 = {p1,p2}

then A110: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {p1} /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by RLTOPSP1:71
.= {} by A109, Lm1, Lm7 ;
( (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & p1 in LSeg |[0 ,1]|,p2 ) by A94, A109, RLTOPSP1:69, XBOOLE_1:27;
then ( (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) c= {p1} & (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) <> {} ) by A109, Lm15, TOPREAL1:21, XBOOLE_0:def 4;
then (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = {p1} by ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ {p1}) \/ {p2} by A99, A110, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

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

A112: not |[0 ,0 ]| in LSeg |[0 ,1]|,p2 by A94, Lm4, TOPREAL1:10;
(LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) = (LSeg |[0 ,1]|,p2) /\ {|[0 ,0 ]|} by A111, RLTOPSP1:71
.= {} by A112, Lm1 ;
hence P1 /\ P2 = {p1,p2} by A99, A111, ENUMSET1:41, TOPREAL1:23; :: thesis: verum

end;

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

A114: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A8, TOPREAL1:23, XBOOLE_1:27;

now

assume |[0 ,0 ]| in (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ; :: thesis: contradiction
then ( |[0 ,0 ]| in LSeg p1,|[0 ,1]| & p1 `2 <= |[0 ,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, A113, EUCLID:57; :: thesis: verum

end;

then {|[0 ,0 ]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by ZFMISC_1:37;
then A115: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A114, ZFMISC_1:39;
A116: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[0 ,0 ]|) c= {|[0 ,1]|} by A7, A94, TOPREAL1:21, XBOOLE_1:27;

now

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

end;

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

end;

end;

end;

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

end;

suppose A117: 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 A118: 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,|[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} )
( |[0 ,0 ]| in LSeg p1,|[0 ,0 ]| & |[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 ) by RLTOPSP1:69;
then ( LSeg p1,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[0 ,1]| & LSeg |[0 ,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| & |[0 ,0 ]| in (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) ) by A3, A117, Lm13, Lm14, TOPREAL1:12, XBOOLE_0:def 4;
then ( (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[0 ,0 ]|} & (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} ) by TOPREAL1:23, XBOOLE_1:27;
then ( (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|} & ( p1 <> |[0 ,0 ]| or |[0 ,0 ]| <> p2 ) ) by A1, ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
( LSeg |[0 ,1]|,|[1,1]| is_an_arc_of |[0 ,1]|,|[1,1]| & LSeg |[1,0 ]|,|[1,1]| is_an_arc_of |[1,1]|,|[1,0 ]| ) by Lm4, TOPREAL1:15;
then A119: (LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[0 ,1]|,|[1,0 ]| by TOPREAL1:5, TOPREAL1:24;
A120: LSeg |[1,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| by A117, Lm17, TOPREAL1:12;
then A121: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by Lm2, XBOOLE_1:3, XBOOLE_1:26;
|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then A122: ( (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & |[1,0 ]| in (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) ) by A120, Lm18, XBOOLE_0:def 4, XBOOLE_1:27;
((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 A121, A122, TOPREAL1:22, ZFMISC_1:39 ;
then A123: ((LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[0 ,1]|,p2 by A119, TOPREAL1:16;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) c= {|[0 ,0 ]|} by A8, A120, TOPREAL1:23, XBOOLE_1:27;
then A124: ( (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {|[0 ,0 ]|} or (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {} ) by ZFMISC_1:39;

A125: now

assume |[0 ,0 ]| in (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) ; :: thesis: contradiction
then ( |[0 ,0 ]| in LSeg p1,|[0 ,1]| & |[0 ,0 ]| in LSeg p2,|[1,0 ]| & p1 `2 <= |[0 ,1]| `2 & p2 `1 <= |[1,0 ]| `1 ) by A5, A6, A118, EUCLID:56, XBOOLE_0:def 4;
then A126: ( |[0 ,0 ]| `2 = p1 `2 & |[0 ,0 ]| `2 = p2 `2 & |[0 ,0 ]| `1 = p1 `1 & |[0 ,0 ]| `1 = p2 `1 ) by A5, A6, A118, Lm4, TOPREAL1:9, TOPREAL1:10;
then p1 = |[(|[0 ,0 ]| `1 ),(|[0 ,0 ]| `2 )]| by EUCLID:57
.= p2 by A126, 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 A124, A125, XBOOLE_1:23, ZFMISC_1:37
.= {|[0 ,1]|} by A14, A15, A16, XBOOLE_0:def 10 ;
hence P2 is_an_arc_of p1,p2 by A123, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A127: LSeg |[0 ,0 ]|,|[0 ,1]| = (LSeg p1,|[0 ,0 ]|) \/ (LSeg p1,|[0 ,1]|) by A3, TOPREAL1:11;
A128: LSeg |[0 ,0 ]|,|[1,0 ]| = (LSeg |[1,0 ]|,p2) \/ (LSeg |[0 ,0 ]|,p2) by A117, TOPREAL1:11;
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 A127, 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 A128, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A129: LSeg |[0 ,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| by A117, Lm14, TOPREAL1:12;
A130: {p1} = (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) by A3, TOPREAL1:14;
A131: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,p2) = {p2} by A117, TOPREAL1:14;
A132: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A129, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A133: 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 A130, 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 A131, 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 A10, A132 ;

A134: now

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

suppose A135: 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 A7, Lm4, TOPREAL1:9;
then A136: LSeg p1,|[0 ,0 ]| misses {p2} by ZFMISC_1:56;
(LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) = (LSeg p1,|[0 ,0 ]|) /\ {p2} by A135, RLTOPSP1:71
.= {} by A136, 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 A133, A135, TOPREAL1:22; :: thesis: verum

end;

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

A138: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,0 ]|} by A129, TOPREAL1:22, XBOOLE_1:27;

now

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

end;

then {|[1,0 ]|} <> (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
then A139: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A138, ZFMISC_1:39;
A140: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {|[0 ,0 ]|} by A7, A120, TOPREAL1:23, XBOOLE_1:27;

now

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

end;

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

end;

suppose A141: 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 A142: (LSeg |[0 ,0 ]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[0 ,0 ]|} /\ (LSeg |[1,0 ]|,|[1,1]|) by RLTOPSP1:71
.= {} by Lm1, Lm5 ;
A143: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {p2} by A7, A141, TOPREAL1:23, XBOOLE_1:27;
p2 in LSeg p1,|[0 ,0 ]| by A141, RLTOPSP1:69;
then (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} by A141, Lm14, XBOOLE_0:def 4;
then (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {p2} by A143, ZFMISC_1:39;
hence P1 /\ P2 = (({p1} \/ ((LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|))) \/ {p2}) \/ (((LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) by A133, A142, 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 A144: p1 = |[0 ,1]| ; :: thesis: P1 /\ P2 = {p1,p2}

then A145: (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = (LSeg |[0 ,0 ]|,p2) /\ {p1} by RLTOPSP1:71;
not p1 in LSeg |[0 ,0 ]|,p2 by A129, A144, Lm4, TOPREAL1:10;
then (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A145, Lm1;
hence P1 /\ P2 = {p1,p2} by A134, A144, ENUMSET1:41, TOPREAL1:21; :: thesis: verum

end;

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

then (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {p1} /\ (LSeg |[0 ,1]|,|[1,1]|) by RLTOPSP1:71;
then A147: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A146, Lm1, Lm6;
A148: (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A117, A146, Lm14, TOPREAL1:12, XBOOLE_1:26;
|[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
then (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) <> {} by A146, Lm13, XBOOLE_0:def 4;
then (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = {p1} by A146, A148, TOPREAL1:23, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ {p1}) \/ {p2} by A134, A147, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:41 ;
:: thesis: verum

end;

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

A150: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A7, TOPREAL1:21, XBOOLE_1:27;

now

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

end;

then {|[0 ,1]|} <> (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
then A151: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A150, ZFMISC_1:39;
A152: (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A8, A129, XBOOLE_1:27;

now

assume |[0 ,0 ]| in (LSeg |[0 ,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) ; :: thesis: contradiction
then ( |[0 ,0 ]| in LSeg p1,|[0 ,1]| & p1 `2 <= |[0 ,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, A149, EUCLID:57; :: thesis: verum

end;

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

end;

end;

end;

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

end;

suppose A153: 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 A154: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) by TOPREAL1:19;
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} )
( LSeg |[1,0 ]|,p2 c= LSeg |[1,0 ]|,|[1,1]| & |[1,0 ]| in LSeg |[0 ,0 ]|,|[1,0 ]| & |[1,0 ]| in LSeg |[1,0 ]|,p2 ) by A153, Lm18, RLTOPSP1:69, TOPREAL1:12;
then ( (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,0 ]|} & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} ) by TOPREAL1:22, XBOOLE_0:def 4, XBOOLE_1:27;
then (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} by ZFMISC_1:39;
then A155: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[0 ,0 ]|,p2 by Lm4, TOPREAL1:18;
LSeg |[1,0 ]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A153, Lm18, TOPREAL1:12;
then A156: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {} by A7, 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 A11, A12, A156, 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 A155, 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} )
A157: LSeg |[1,1]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A153, Lm20, TOPREAL1:12;
then ( (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) & |[1,1]| in LSeg |[1,1]|,p2 ) by RLTOPSP1:69, XBOOLE_1:27;
then ( (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= {|[1,1]|} & (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} ) by Lm19, TOPREAL1:24, XBOOLE_0:def 4;
then (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} by ZFMISC_1:39;
then A158: (LSeg |[0 ,1]|,|[1,1]|) \/ (LSeg |[1,1]|,p2) is_an_arc_of |[0 ,1]|,p2 by Lm4, TOPREAL1:18;
A159: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {} by A8, A157, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(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 A15, A16, A159, 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 A158, 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 A153, 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}
( p1 in LSeg p1,|[0 ,0 ]| & p1 in LSeg p1,|[0 ,1]| ) by RLTOPSP1:69;
then p1 in (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) by XBOOLE_0:def 4;
then A160: {p1} c= (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) by ZFMISC_1:37;

now

let a be set ; :: thesis: ( a in (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) implies a in {p1} )
assume A161: a in (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) ; :: thesis: a in {p1}
then A162: ( a in LSeg |[0 ,0 ]|,p1 & a in LSeg p1,|[0 ,1]| ) by XBOOLE_0:def 4;
reconsider p = a as Point of (TOP-REAL 2) by A161;
( p `1 <= p1 `1 & p1 `1 <= p `1 & p `2 <= p1 `2 & p1 `2 <= p `2 ) by A5, A6, A162, Lm4, TOPREAL1:9, TOPREAL1:10;
then ( p `1 = p1 `1 & p `2 = p1 `2 ) by XXREAL_0:1;
then a = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57
.= p1 by EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

then (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) c= {p1} by TARSKI:def 3;
then A163: (LSeg p1,|[0 ,0 ]|) /\ (LSeg p1,|[0 ,1]|) = {p1} by A160, XBOOLE_0:def 10;
A164: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A7, A157, Lm3, XBOOLE_1:3, XBOOLE_1:27;
( p2 in LSeg |[1,0 ]|,p2 & p2 in LSeg |[1,1]|,p2 ) by RLTOPSP1:69;
then p2 in (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) by XBOOLE_0:def 4;
then A165: {p2} c= (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;

now

let a be set ; :: thesis: ( a in (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) implies a in {p2} )
assume A166: a in (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) ; :: thesis: a in {p2}
then A167: ( a in LSeg |[1,0 ]|,p2 & a in LSeg p2,|[1,1]| ) by XBOOLE_0:def 4;
reconsider p = a as Point of (TOP-REAL 2) by A166;
( p `2 <= p2 `2 & p2 `2 <= p `2 & p `1 <= p2 `1 & p2 `1 <= p `1 ) by A154, A167, Lm4, TOPREAL1:9, TOPREAL1:10;
then ( p `2 = p2 `2 & p `1 = p2 `1 ) by XXREAL_0:1;
then a = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57
.= p2 by EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

then A168: (LSeg |[1,0 ]|,p2) /\ (LSeg |[1,1]|,p2) c= {p2} by TARSKI:def 3;
A169: LSeg |[1,0 ]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A153, Lm18, TOPREAL1:12;
then A170: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A8, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A171: 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 A164, 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 A163, 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 A165, A168, 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 A170 ;

A172: now

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

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

end;

suppose A174: 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, Lm10 ;
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 A171, A174, 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 A175: ( 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}

A176: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= {|[1,0 ]|} by A157, TOPREAL1:22, XBOOLE_1:27;

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 A154, EUCLID:56, XBOOLE_0:def 4;
then ( p2 `2 = |[1,0 ]| `2 & p2 `1 = |[1,0 ]| `1 ) by A154, Lm4, TOPREAL1:10;
then p2 = |[(|[1,0 ]| `1 ),(|[1,0 ]| `2 )]| by EUCLID:57
.= |[1,0 ]| by EUCLID:57 ;
hence contradiction by A175; :: thesis: verum

end;

then (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) <> {|[1,0 ]|} by ZFMISC_1:37;
then A177: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A176, ZFMISC_1:39;
A178: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A169, XBOOLE_1:27;

now

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

end;

then {|[1,1]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) by ZFMISC_1:37;
then (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by A178, TOPREAL1:24, 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 A171, A177; :: thesis: verum

end;

end;

end;

now

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

suppose A179: 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, Lm7 ;
hence P1 /\ P2 = {p1,p2} by A172, A179, ENUMSET1:41, TOPREAL1:21; :: thesis: verum

end;

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

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

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 & p1 `1 = |[0 ,0 ]| `1 ) by A5, A6, Lm4, TOPREAL1:10;
then p1 = |[(|[0 ,0 ]| `1 ),(|[0 ,0 ]| `2 )]| by EUCLID:57
.= |[0 ,0 ]| by EUCLID:57 ;
hence contradiction by A180; :: thesis: verum

end;

then {|[0 ,0 ]|} <> (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|) by ZFMISC_1:37;
then A182: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg p1,|[0 ,1]|) = {} by A181, TOPREAL1:23, ZFMISC_1:39;
A183: (LSeg p1,|[0 ,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) c= {|[0 ,1]|} by A7, TOPREAL1:21, XBOOLE_1:27;

now

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

end;

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

end;

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

end;

end;

end;

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

end;

end;