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

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

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

|[0,0]| in LSeg (|[0,0]|,p2) by RLTOPSP1:68;
then A18: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) <> {} by Lm21, XBOOLE_0:def 4;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A17, Lm20, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) = {|[0,0]|} by A18, TOPREAL1:17, ZFMISC_1:33;
then A19: (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2)) is_an_arc_of |[1,0]|,p2 by Lm4, Lm8, TOPREAL1:9, TOPREAL1:10;
A20: LSeg (p2,|[0,0]|) c= LSeg (|[0,0]|,|[0,1]|) by A17, Lm20, TOPREAL1:6;
then A21: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A11, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A22: LSeg (p2,|[0,1]|) c= LSeg (|[0,0]|,|[0,1]|) by A17, Lm22, TOPREAL1:6;
then A23: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A5, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by TOPREAL1:20, XBOOLE_0:def 7;
then A24: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A5, A20, XBOOLE_1:3, XBOOLE_1:27;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by TOPREAL1:20, XBOOLE_0:def 7;
then A25: (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) = {} by A11, A22, XBOOLE_1:3, XBOOLE_1:27;
A26: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,p2)) = {p2} by A17, TOPREAL1:8;
|[0,1]| in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
then A27: |[0,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) by Lm23, XBOOLE_0:def 4;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A17, Lm22, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = {|[0,1]|} by A27, TOPREAL1:15, ZFMISC_1:33;
then A28: (LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2)) is_an_arc_of |[1,1]|,p2 by Lm6, Lm10, TOPREAL1:9, TOPREAL1:10;
take P1 = ((LSeg (p1,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A29: (LSeg (p1,|[1,1]|)) \/ (LSeg (p1,|[1,0]|)) = LSeg (|[1,0]|,|[1,1]|) by A3, TOPREAL1:5;
(LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) = ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= {|[1,1]|} by A8, A6, A23, TOPREAL1:18, ZFMISC_1:33 ;
then (LSeg (p1,|[1,1]|)) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) is_an_arc_of p1,p2 by A28, TOPREAL1:11;
hence P1 is_an_arc_of p1,p2 by XBOOLE_1:4; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A30: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 0 & q `2 <= 1 & q `2 >= 0 ) by A17, TOPREAL1:13;
(LSeg (p1,|[1,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2))) = ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))) by XBOOLE_1:23
.= {|[1,0]|} by A9, A7, A21, TOPREAL1:16, ZFMISC_1:33 ;
then (LSeg (p1,|[1,0]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2))) is_an_arc_of p1,p2 by A19, TOPREAL1:11;
hence P2 is_an_arc_of p1,p2 by XBOOLE_1:4; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus R^2-unit_square = (((LSeg (|[0,0]|,p2)) \/ (LSeg (|[0,1]|,p2))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) by A17, TOPREAL1:5, TOPREAL1:def 2
.= ((LSeg (|[0,0]|,p2)) \/ ((LSeg (|[0,1]|,p2)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:4
.= ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2))) by XBOOLE_1:4
.= ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:4
.= ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (p1,|[1,1]|)) \/ ((LSeg (p1,|[1,0]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,p2))))) by A29, XBOOLE_1:4
.= ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:4
.= ((LSeg (p1,|[1,1]|)) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A31: (LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) = {p1} by A3, TOPREAL1:8;
A32: P1 /\ P2 = (((LSeg (p1,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((LSeg (|[0,1]|,p2)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:23
.= (((LSeg (p1,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2}) by A26, XBOOLE_1:23
.= (((LSeg (p1,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2}) by XBOOLE_1:23
.= (((LSeg (p1,|[1,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by A25, XBOOLE_1:23
.= (((LSeg (p1,|[1,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,|[1,1]|)) /\ ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by XBOOLE_1:23
.= (((LSeg (p1,|[1,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by XBOOLE_1:23
.= ((((LSeg (p1,|[1,1]|)) /\ ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by Lm2, XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by A24, A31, XBOOLE_1:23 ;

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

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

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

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

end;

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

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

end;

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

now :: thesis: not |[1,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))

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

end;

then A38: {|[1,1]|} <> (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) by ZFMISC_1:31;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) c= {|[1,1]|} by A3, Lm25, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
then A39: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) = {} by A38, ZFMISC_1:33;

now :: thesis: not |[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))

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

end;

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

end;

end;

end;

now :: thesis: P1 /\ P2 = {p1,p2}

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

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

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

end;

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

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

end;

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

now :: thesis: not |[0,0]| in (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))

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

end;

then A46: {|[0,0]|} <> (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) by ZFMISC_1:31;
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= {|[0,0]|} by A17, Lm22, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
then A47: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A46, ZFMISC_1:33;

now :: thesis: not |[0,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))

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

end;

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

end;

end;

end;

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

end;

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

then A51: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) by TOPREAL1:13;

now :: thesis: not |[1,1]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2))

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

end;

then A56: {|[1,1]|} <> (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) by ZFMISC_1:31;
A57: LSeg (|[0,0]|,|[0,1]|) is_an_arc_of |[0,0]|,|[0,1]| by Lm5, Lm7, TOPREAL1:9;
LSeg (|[0,0]|,|[1,0]|) is_an_arc_of |[1,0]|,|[0,0]| by Lm4, Lm8, TOPREAL1:9;
then A58: (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)) is_an_arc_of |[1,0]|,|[0,1]| by A57, TOPREAL1:2, TOPREAL1:17;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by TOPREAL1:20, XBOOLE_0:def 7;
then A59: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A5, XBOOLE_1:3, XBOOLE_1:26;
take P1 = (LSeg (p1,|[1,1]|)) \/ (LSeg (|[1,1]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A60: (LSeg (p1,|[1,1]|)) \/ (LSeg (p1,|[1,0]|)) = LSeg (|[1,0]|,|[1,1]|) by A3, TOPREAL1:5;
|[0,1]| in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
then A61: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) <> {} by Lm22, XBOOLE_0:def 4;
A62: |[1,1]| in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
|[1,1]| in LSeg (p1,|[1,1]|) by RLTOPSP1:68;
then A63: |[1,1]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) by A62, XBOOLE_0:def 4;
A64: LSeg (|[1,1]|,p2) c= LSeg (|[0,1]|,|[1,1]|) by A50, Lm26, TOPREAL1:6;
then (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A5, XBOOLE_1:27;
then A65: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) = {|[1,1]|} by A63, TOPREAL1:18, ZFMISC_1:33;
( p1 <> |[1,1]| or |[1,1]| <> p2 ) by A1;
hence P1 is_an_arc_of p1,p2 by A65, TOPREAL1:12; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A66: {p1} = (LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[1,0]|)) by A3, TOPREAL1:8;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
then A67: (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A64, XBOOLE_1:3, XBOOLE_1:26;
A68: LSeg (p2,|[0,1]|) c= LSeg (|[0,1]|,|[1,1]|) by A50, Lm23, TOPREAL1:6;
then A69: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) c= {|[0,1]|} by TOPREAL1:15, XBOOLE_1:27;
A70: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A68, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[0,1]|,p2)) = ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= {|[0,1]|} by A70, A69, A61, ZFMISC_1:33 ;
then A71: ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)) is_an_arc_of |[1,0]|,p2 by A58, TOPREAL1:10;
A72: {p2} = (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,1]|,p2)) by A50, TOPREAL1:8;
A73: (LSeg (|[0,1]|,p2)) \/ (LSeg (|[1,1]|,p2)) = LSeg (|[0,1]|,|[1,1]|) by A50, TOPREAL1:5;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A11, A68, XBOOLE_1:27;
then A74: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A56, TOPREAL1:18, ZFMISC_1:33;
(LSeg (p1,|[1,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) = ((LSeg (p1,|[1,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[1,0]|,p1)) /\ (LSeg (|[0,0]|,|[0,1]|))) by A74, XBOOLE_1:23
.= {|[1,0]|} by A9, A7, A12, TOPREAL1:16, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A71, TOPREAL1:11; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg (|[1,1]|,p2)) \/ ((LSeg (p1,|[1,1]|)) \/ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) by XBOOLE_1:4
.= (LSeg (|[1,1]|,p2)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) by A60, XBOOLE_1:4
.= (LSeg (|[1,1]|,p2)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ (LSeg (|[0,1]|,p2))) by XBOOLE_1:4
.= (LSeg (|[1,1]|,p2)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) by XBOOLE_1:4
.= (LSeg (|[1,1]|,p2)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2)))) by XBOOLE_1:4
.= (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:4
.= R^2-unit_square by A73, TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A75: P1 /\ P2 = ((LSeg (p1,|[1,1]|)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) by XBOOLE_1:23
.= (((LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) by A66, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[1,1]|,p2)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))))) by A59, XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ (((LSeg (|[1,1]|,p2)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2})) by A72, XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ ((((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})) by A67 ;

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

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

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

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

end;

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

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

end;

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

now :: thesis: not |[1,1]| in (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[1,0]|))

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

end;

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

now :: thesis: not |[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))

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

end;

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

end;

end;

end;

now :: thesis: P1 /\ P2 = {p1,p2}

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

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

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

end;

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

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

end;

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

now :: thesis: not |[0,1]| in (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))

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

end;

then A96: {|[0,1]|} <> (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
(LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A50, Lm26, TOPREAL1:6, XBOOLE_1:26;
then A97: (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A96, TOPREAL1:15, ZFMISC_1:33;

now :: thesis: not |[1,1]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))

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

end;

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

end;

end;

end;

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

end;

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

then A101: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 0 ) by TOPREAL1:13;

now :: thesis: not |[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))

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

end;

then A106: {|[1,0]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) by ZFMISC_1:31;
A107: LSeg (|[0,0]|,|[0,1]|) is_an_arc_of |[0,1]|,|[0,0]| by Lm5, Lm7, TOPREAL1:9;
LSeg (|[0,1]|,|[1,1]|) is_an_arc_of |[1,1]|,|[0,1]| by Lm6, Lm10, TOPREAL1:9;
then A108: (LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)) is_an_arc_of |[1,1]|,|[0,0]| by A107, TOPREAL1:2, TOPREAL1:15;
take P1 = (LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A109: (LSeg (p1,|[1,0]|)) \/ (LSeg (p1,|[1,1]|)) = LSeg (|[1,0]|,|[1,1]|) by A3, TOPREAL1:5;
|[0,0]| in LSeg (|[0,0]|,p2) by RLTOPSP1:68;
then A110: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) <> {} by Lm20, XBOOLE_0:def 4;
A111: |[1,0]| in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
|[1,0]| in LSeg (p1,|[1,0]|) by RLTOPSP1:68;
then A112: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) <> {} by A111, XBOOLE_0:def 4;
A113: LSeg (p2,|[1,0]|) c= LSeg (|[0,0]|,|[1,0]|) by A100, Lm24, TOPREAL1:6;
then (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A11, XBOOLE_1:27;
then A114: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) = {|[1,0]|} by A112, TOPREAL1:16, ZFMISC_1:33;
( p1 <> |[1,0]| or p2 <> |[1,0]| ) by A1;
hence P1 is_an_arc_of p1,p2 by A114, TOPREAL1:12; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A115: (LSeg (p1,|[1,0]|)) /\ (LSeg (p1,|[1,1]|)) = {p1} by A3, TOPREAL1:8;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
then A116: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A113, XBOOLE_1:3, XBOOLE_1:26;
A117: LSeg (p2,|[0,0]|) c= LSeg (|[0,0]|,|[1,0]|) by A100, Lm21, TOPREAL1:6;
then A118: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) c= {|[0,0]|} by TOPREAL1:17, XBOOLE_1:27;
A119: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A117, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[0,0]|,p2)) = ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))) by XBOOLE_1:23
.= {|[0,0]|} by A119, A118, A110, ZFMISC_1:33 ;
then A120: ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)) is_an_arc_of |[1,1]|,p2 by A108, TOPREAL1:10;
A121: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,p2)) = {p2} by A100, TOPREAL1:8;
A122: (LSeg (|[0,0]|,p2)) \/ (LSeg (|[1,0]|,p2)) = LSeg (|[0,0]|,|[1,0]|) by A100, TOPREAL1:5;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A5, A117, XBOOLE_1:27;
then A123: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A106, TOPREAL1:16, ZFMISC_1:33;
(LSeg (p1,|[1,1]|)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))) = ((LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) by A123, XBOOLE_1:23
.= {|[1,1]|} by A8, A6, A10, TOPREAL1:18, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A120, TOPREAL1:11; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg (|[1,0]|,p2)) \/ ((LSeg (p1,|[1,0]|)) \/ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))) by XBOOLE_1:4
.= (LSeg (|[1,0]|,p2)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2)))) by A109, XBOOLE_1:4
.= ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))) \/ (LSeg (|[1,0]|,p2)) by XBOOLE_1:4
.= (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|)) by A122, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A124: P1 /\ P2 = ((LSeg (p1,|[1,0]|)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) by XBOOLE_1:23
.= (((LSeg (p1,|[1,0]|)) /\ (LSeg (p1,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) by A115, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,0]|,p1)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) by A12, XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ (((LSeg (|[1,0]|,p2)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2})) by A121, XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ ((((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})) by A116 ;

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

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

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

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

end;

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

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

end;

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

now :: thesis: not |[1,0]| in (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[1,1]|))

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

end;

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

now :: thesis: not |[1,1]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))

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

end;

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

end;

end;

end;

now :: thesis: P1 /\ P2 = {p1,p2}

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

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

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

end;

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

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

end;

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

now :: thesis: not |[0,0]| in (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))

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

end;

then A144: {|[0,0]|} <> (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
(LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A100, Lm24, TOPREAL1:6, XBOOLE_1:26;
then A145: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A144, TOPREAL1:17, ZFMISC_1:33;

now :: thesis: not |[1,0]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))

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

end;

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

end;

end;

end;

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

end;

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

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

now :: thesis: ex P1 being Element of K19( the carrier of (TOP-REAL 2)) ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )

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

suppose A156: p `2 < q `2 ; :: thesis: ex P1 being Element of K19( the carrier of (TOP-REAL 2)) ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )

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

proof

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

end;

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

A165: now :: thesis: not (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) <> {}

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

end;

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

now :: thesis: not |[1,1]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))

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

end;

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

now :: thesis: not |[1,0]| in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))

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

end;

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

proof

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

end;

A187: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A3, Lm25, TOPREAL1:6, XBOOLE_1:26;
|[1,1]| in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
then A188: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) <> {} by Lm26, XBOOLE_0:def 4;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[1,1]|} by A148, Lm27, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
then A189: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) = {|[1,1]|} by A188, ZFMISC_1:33;
take P1 = LSeg (p1,p2); :: thesis: ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[1,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A190: p1 in LSeg (p1,|[1,0]|) by RLTOPSP1:68;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:9; :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A191: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by TOPREAL1:20, XBOOLE_0:def 7;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) c= (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A148, Lm27, TOPREAL1:6, XBOOLE_1:26;
then A192: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A191, XBOOLE_1:3;
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (LSeg (|[1,1]|,p2)) = (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= (((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)))) \/ {|[1,1]|} by A189, XBOOLE_1:23
.= {|[1,1]|} by A178, A192 ;
then A193: (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)) is_an_arc_of |[1,0]|,p2 by A171, TOPREAL1:10;
(LSeg (p1,|[1,0]|)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) = ((LSeg (p1,|[1,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[1,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) by A165, XBOOLE_1:23
.= ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) by A174, XBOOLE_1:23
.= {|[1,0]|} by A187, A164, A175, TOPREAL1:16, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A193, TOPREAL1:11; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) \/ ((LSeg (p1,|[1,0]|)) \/ (LSeg (p1,p2))) by XBOOLE_1:4
.= (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (((LSeg (|[1,0]|,p1)) \/ (LSeg (p1,p2))) \/ (LSeg (p2,|[1,1]|))) by XBOOLE_1:4
.= (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|)) by A3, A148, TOPREAL1:7
.= ((LSeg (|[0,0]|,|[1,0]|)) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ (LSeg (|[1,0]|,|[1,1]|)) by XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A194: p2 in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then p2 in (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) by A194, XBOOLE_0:def 4;
then {p2} c= (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) by ZFMISC_1:31;
then A195: (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) = {p2} by A157, XBOOLE_0:def 10;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then p1 in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) by A190, XBOOLE_0:def 4;
then {p1} c= (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) = {p1} by A180, XBOOLE_0:def 10;
then A196: P1 /\ P2 = {p1} \/ ((LSeg (p1,p2)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2}) by A195, XBOOLE_1:23
.= {p1} \/ ((((LSeg (p1,p2)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})) by A179, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:4 ;
A197: (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A3, A148, TOPREAL1:6, XBOOLE_1:26;

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

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

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

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

end;

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

now :: thesis: not |[1,0]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))

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

end;

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

end;

end;

end;

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

now :: thesis: P1 /\ P2 = {p1,p2}

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

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

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

end;

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

now :: thesis: not |[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))

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

end;

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

end;

end;

end;

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

end;

suppose A204: q `2 < p `2 ; :: thesis: ex P1 being Element of K19( the carrier of (TOP-REAL 2)) ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) or a in {p2} )
assume A206: a in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A207: p in LSeg (|[1,0]|,p2) by A206, XBOOLE_0:def 4;
|[1,0]| `2 <= p2 `2 by A151, A154, EUCLID:52;
then A208: p `2 <= p2 `2 by A207, TOPREAL1:4;
A209: p in LSeg (p2,p1) by A206, XBOOLE_0:def 4;
then A210: p2 `1 <= p `1 by A13, A14, A151, A152, TOPREAL1:3;
p2 `2 <= p `2 by A13, A151, A204, A209, TOPREAL1:4;
then A211: p2 `2 = p `2 by A208, XXREAL_0:1;
p `1 <= p1 `1 by A13, A14, A151, A152, A209, TOPREAL1:3;
then p `1 = 1 by A13, A14, A151, A152, A210, XXREAL_0:1;
then p = |[1,(p2 `2)]| by A211, EUCLID:53
.= p2 by A151, A152, EUCLID:53 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

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

A213: now :: thesis: not (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) <> {}

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

end;

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

now :: thesis: not |[1,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))

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

end;

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

now :: thesis: not |[1,0]| in (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))

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

end;

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

proof

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

end;

A235: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A3, Lm27, TOPREAL1:6, XBOOLE_1:26;
|[1,0]| in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
then A236: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) <> {} by Lm24, XBOOLE_0:def 4;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[1,0]|} by A148, Lm25, TOPREAL1:6, TOPREAL1:16, XBOOLE_1:26;
then A237: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) = {|[1,0]|} by A236, ZFMISC_1:33;
take P1 = LSeg (p1,p2); :: thesis: ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[1,1]|)) \/ ((((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A238: p1 in LSeg (p1,|[1,1]|) by RLTOPSP1:68;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:9; :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A239: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by TOPREAL1:20, XBOOLE_0:def 7;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) c= (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A148, Lm25, TOPREAL1:6, XBOOLE_1:26;
then A240: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A239, XBOOLE_1:3;
(((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) /\ (LSeg (|[1,0]|,p2)) = (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= (((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)))) \/ {|[1,0]|} by A237, XBOOLE_1:23
.= {|[1,0]|} by A222, A240 ;
then A241: (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2)) is_an_arc_of |[1,1]|,p2 by A219, TOPREAL1:10;
(LSeg (p1,|[1,1]|)) /\ ((((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))) = ((LSeg (p1,|[1,1]|)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) by A213, XBOOLE_1:23
.= ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) by A226, XBOOLE_1:23
.= {|[1,1]|} by A235, A212, A223, TOPREAL1:18, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A241, TOPREAL1:11; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = ((((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))) \/ ((LSeg (p1,|[1,1]|)) \/ (LSeg (p1,p2))) by XBOOLE_1:4
.= (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[1,0]|,p2)) \/ ((LSeg (p1,p2)) \/ (LSeg (p1,|[1,1]|)))) by XBOOLE_1:4
.= (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|)) by A3, A148, TOPREAL1:7
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A242: p2 in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then p2 in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) by A242, XBOOLE_0:def 4;
then {p2} c= (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) by ZFMISC_1:31;
then A243: (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) = {p2} by A205, XBOOLE_0:def 10;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then p1 in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) by A238, XBOOLE_0:def 4;
then {p1} c= (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) = {p1} by A228, XBOOLE_0:def 10;
then A244: P1 /\ P2 = {p1} \/ ((LSeg (p1,p2)) /\ ((((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2)))) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2}) by A243, XBOOLE_1:23
.= {p1} \/ ((((LSeg (p1,p2)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})) by A227, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by XBOOLE_1:4 ;
A245: (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A3, A148, TOPREAL1:6, XBOOLE_1:26;

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

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

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

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

end;

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

now :: thesis: not |[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))

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

end;

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

end;

end;

end;

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

now :: thesis: P1 /\ P2 = {p1,p2}

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

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

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

end;

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

now :: thesis: not |[1,0]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))

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

end;

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

end;

end;

end;

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

end;

end;

end;

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

end;

end;