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

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

suppose 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 A18: LSeg |[0 ,1]|,p2 c= LSeg |[0 ,0 ]|,|[0 ,1]| by Lm22, TOPREAL1:12;
LSeg p1,|[0 ,1]| c= LSeg |[0 ,1]|,|[1,1]| by A3, Lm23, TOPREAL1:12;
then A19: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A18, XBOOLE_1:27;
take P1 = (LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,p2); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,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} )
A20: |[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
|[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
then A21: {} <> (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) by Lm21, XBOOLE_0:def 4;
|[0 ,1]| in LSeg p1,|[0 ,1]| by RLTOPSP1:69;
then (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} by A20, XBOOLE_0:def 4;
then A22: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) = {|[0 ,1]|} by A19, TOPREAL1:21, ZFMISC_1:39;
( p1 <> |[0 ,1]| or p2 <> |[0 ,1]| ) by A1;
hence P1 is_an_arc_of p1,p2 by A22, TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A23: (LSeg p1,|[0 ,1]|) \/ (LSeg p1,|[1,1]|) = LSeg |[0 ,1]|,|[1,1]| by A3, TOPREAL1:11;
A24: LSeg |[1,0 ]|,|[1,1]| is_an_arc_of |[1,1]|,|[1,0 ]| by Lm9, Lm11, TOPREAL1:15;
LSeg |[0 ,0 ]|,|[1,0 ]| is_an_arc_of |[1,0 ]|,|[0 ,0 ]| by Lm4, Lm8, TOPREAL1:15;
then A25: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by A24, TOPREAL1:5, TOPREAL1:22;
A26: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= {|[0 ,0 ]|} by A17, Lm20, TOPREAL1:12, TOPREAL1:23, XBOOLE_1:26;
A27: (LSeg |[0 ,0 ]|,p2) \/ (LSeg |[0 ,1]|,p2) = LSeg |[0 ,0 ]|,|[0 ,1]| by A17, TOPREAL1:11;
A28: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A17, TOPREAL1:14;
A29: LSeg |[0 ,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[0 ,1]| by A17, Lm20, TOPREAL1:12;
then A30: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by Lm3, XBOOLE_1:3, XBOOLE_1:27;
A31: ex q2 being Point of (TOP-REAL 2) st
( q2 = p2 & q2 `1 = 0 & q2 `2 <= 1 & q2 `2 >= 0 ) by A17, TOPREAL1:19;

A32: now

A33: |[0 ,0 ]| `2 <= p2 `2 by A31, EUCLID:56;
assume A34: |[0 ,1]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) ; :: thesis: contradiction
then A35: |[0 ,1]| in LSeg p1,|[1,1]| by XBOOLE_0:def 4;
|[0 ,1]| in LSeg |[0 ,0 ]|,p2 by A34, XBOOLE_0:def 4;
then |[0 ,1]| `2 <= p2 `2 by A33, TOPREAL1:10;
then A36: |[0 ,1]| `2 = p2 `2 by A31, Lm7, XXREAL_0:1;
p1 `1 <= |[1,1]| `1 by A13, A14, EUCLID:56;
then |[0 ,1]| `1 = p1 `1 by A13, A15, A35, Lm6, TOPREAL1:9;
then p1 = |[(|[0 ,1]| `1 ),(|[0 ,1]| `2 )]| by A13, A16, Lm7, EUCLID:57
.= p2 by A31, A36, Lm6, EUCLID:57 ;
hence contradiction by A1; :: thesis: verum

end;

((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) /\ (LSeg |[0 ,0 ]|,p2) = ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2)) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:23
.= {|[0 ,0 ]|} by A26, A21, A30, ZFMISC_1:39 ;
then A37: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2) is_an_arc_of |[1,1]|,p2 by A25, TOPREAL1:16;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A8, A29, XBOOLE_1:27;
then A38: ( (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,1]|} or (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} ) by TOPREAL1:21, ZFMISC_1:39;
A39: LSeg p2,|[0 ,1]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A17, Lm22, TOPREAL1:12;
then A40: (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg p1,|[1,1]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2)) = ((LSeg p1,|[1,1]|) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) by A38, A32, XBOOLE_1:23, ZFMISC_1:37
.= {|[1,1]|} by A9, A6, A10, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A37, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg |[0 ,1]|,p2) \/ ((LSeg p1,|[0 ,1]|) \/ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by XBOOLE_1:4
.= (LSeg |[0 ,1]|,p2) \/ ((LSeg |[0 ,1]|,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) by A23, XBOOLE_1:4
.= (LSeg |[0 ,1]|,p2) \/ (((LSeg |[0 ,1]|,|[1,1]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:4
.= ((LSeg |[0 ,0 ]|,p2) \/ (LSeg |[0 ,1]|,p2)) \/ ((LSeg |[0 ,1]|,|[1,1]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) by XBOOLE_1:4
.= R^2-unit_square by A27, TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A41: {p1} = (LSeg p1,|[0 ,1]|) /\ (LSeg p1,|[1,1]|) by A3, TOPREAL1:14;
A42: P1 /\ P2 = ((LSeg p1,|[0 ,1]|) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by XBOOLE_1:23
.= (((LSeg p1,|[0 ,1]|) /\ (LSeg p1,|[1,1]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,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 |[0 ,0 ]|,p2)))) \/ ((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by A41, 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 |[0 ,0 ]|,p2)))) \/ ((LSeg |[0 ,1]|,p2) /\ ((LSeg p1,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,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 |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|)) \/ ((LSeg |[0 ,1]|,p2) /\ (((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|)) \/ (((LSeg |[0 ,1]|,p2) /\ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2})) by A12, A28, XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|)) \/ ((((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 |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|)) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2})) by A40 ;

A43: now

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

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

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

end;

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

then A48: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|) = (LSeg |[0 ,1]|,p2) /\ {p1} by RLTOPSP1:71;
not p1 in LSeg |[0 ,1]|,p2 by A31, A47, Lm6, Lm10, TOPREAL1:9;
then (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|) = {} by A48, Lm1;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A42, A47, TOPREAL1:24, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) ;
:: thesis: verum

end;

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

now

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

end;

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

now

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

end;

then A54: {|[1,1]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,1]|} by A11, TOPREAL1:24, XBOOLE_1:27;
then (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A54, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A42, A52; :: thesis: verum

end;

end;

end;

now

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

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

now

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

end;

then A57: {|[0 ,1]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A11, A29, XBOOLE_1:27;
then A58: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A57, TOPREAL1:21, ZFMISC_1:39;

now

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

end;

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

end;

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

then A62: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) = (LSeg p1,|[0 ,1]|) /\ {|[0 ,0 ]|} by RLTOPSP1:71;
not |[0 ,0 ]| in LSeg p1,|[0 ,1]| by A11, Lm5, Lm7, Lm11, TOPREAL1:10;
then (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A62, Lm1;
hence P1 /\ P2 = {p1,p2} by A43, A61, ENUMSET1:41, TOPREAL1:23; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

A67: q1 = |[(q1 `1 ),(q1 `2 )]| by EUCLID:57;
A68: LSeg p1,p2 c= LSeg |[0 ,1]|,|[1,1]| by A3, A66, TOPREAL1:12;
consider q being Point of (TOP-REAL 2) such that
A69: q = p2 and
A70: q `1 <= 1 and
A71: q `1 >= 0 and
A72: q `2 = 1 by A66, TOPREAL1:19;
A73: q = |[(q `1 ),(q `2 )]| by EUCLID:57;

now

per cases ( q1 `1 < q `1 or q `1 < q1 `1 ) by A1, A13, A16, A69, A72, A67, A73, XXREAL_0:1;

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

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

proof

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

end;

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

A83: now

consider a being Element of (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2);
assume A84: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) <> {} ; :: thesis: contradiction
then reconsider p = a as Point of (TOP-REAL 2) by TARSKI:def 3;
A85: p in LSeg |[0 ,1]|,p1 by A84, XBOOLE_0:def 4;
A86: p in LSeg p2,|[1,1]| by A84, XBOOLE_0:def 4;
p2 `1 <= |[1,1]| `1 by A69, A70, EUCLID:56;
then A87: p2 `1 <= p `1 by A86, TOPREAL1:9;
|[0 ,1]| `1 <= p1 `1 by A13, A15, EUCLID:56;
then p `1 <= p1 `1 by A85, TOPREAL1:9;
hence contradiction by A13, A69, A74, A87, XXREAL_0:2; :: thesis: verum

end;

A88: ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) /\ (LSeg |[1,0 ]|,|[1,1]|) = ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) by XBOOLE_1:23
.= {|[1,0 ]|} by Lm3, TOPREAL1:22 ;
(LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) is_an_arc_of |[0 ,1]|,|[1,0 ]| by Lm5, Lm7, TOPREAL1:15, TOPREAL1:16, TOPREAL1:23;
then A89: ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[0 ,1]|,|[1,1]| by A88, TOPREAL1:16;
A90: (LSeg p1,p2) /\ (LSeg p1,|[0 ,1]|) c= {p1}

proof

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

end;

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

now

assume |[1,1]| in (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: contradiction
then A98: |[1,1]| in LSeg |[0 ,1]|,p1 by XBOOLE_0:def 4;
|[0 ,1]| `1 <= p1 `1 by A13, A15, EUCLID:56;
then |[1,1]| `1 <= p1 `1 by A98, TOPREAL1:9;
hence contradiction by A13, A14, A70, A74, Lm10, XXREAL_0:1; :: thesis: verum

end;

then A99: {|[1,1]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,1]|} by A3, Lm23, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;
then A100: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A99, ZFMISC_1:39;
|[0 ,1]| in LSeg p1,|[0 ,1]| by RLTOPSP1:69;
then A101: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {} by Lm22, XBOOLE_0:def 4;

now

assume |[0 ,1]| in (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) ; :: thesis: contradiction
then A102: |[0 ,1]| in LSeg p2,|[1,1]| by XBOOLE_0:def 4;
p2 `1 <= |[1,1]| `1 by A69, A70, EUCLID:56;
hence contradiction by A15, A69, A74, A102, Lm6, TOPREAL1:9; :: thesis: verum

end;

then A103: {|[0 ,1]|} <> (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) c= {|[0 ,1]|} by A66, Lm26, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
then A104: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {} by A103, ZFMISC_1:39;
take P1 = LSeg p1,p2; :: thesis: ex P2 being Element of K21(the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg p1,|[0 ,1]|) \/ ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (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 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A105: p1 in LSeg p1,|[0 ,1]| by RLTOPSP1:69;
A106: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, Lm23, TOPREAL1:12, XBOOLE_1:26;
|[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
then A107: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} by Lm27, XBOOLE_0:def 4;
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A66, Lm26, TOPREAL1:12, XBOOLE_1:26;
then A108: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} by A107, TOPREAL1:24, ZFMISC_1:39;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:15; :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A109: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A66, Lm26, TOPREAL1:12, XBOOLE_1:26;
then A110: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by A109, XBOOLE_1:3;
(((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) /\ (LSeg |[1,1]|,p2) = (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) /\ (LSeg |[1,1]|,p2)) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2)) by XBOOLE_1:23
.= (((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2))) \/ {|[1,1]|} by A108, XBOOLE_1:23
.= {|[1,1]|} by A104, A110 ;
then A111: (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2) is_an_arc_of |[0 ,1]|,p2 by A89, TOPREAL1:16;
(LSeg p1,|[0 ,1]|) /\ ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)) = ((LSeg p1,|[0 ,1]|) /\ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,1]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[0 ,1]|) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) by A83, XBOOLE_1:23
.= ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) by A100, XBOOLE_1:23
.= {|[0 ,1]|} by A82, A106, A101, TOPREAL1:21, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A111, TOPREAL1:17; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = ((LSeg |[0 ,1]|,p1) \/ (LSeg p1,p2)) \/ ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2)) by XBOOLE_1:4
.= (((LSeg |[0 ,1]|,p1) \/ (LSeg p1,p2)) \/ (LSeg p2,|[1,1]|)) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) by XBOOLE_1:4
.= (LSeg |[0 ,1]|,|[1,1]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) by A3, A66, TOPREAL1:13
.= (LSeg |[0 ,1]|,|[1,1]|) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) by XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A112: p2 in LSeg |[1,1]|,p2 by RLTOPSP1:69;
p2 in LSeg p1,p2 by RLTOPSP1:69;
then p2 in (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) by A112, XBOOLE_0:def 4;
then {p2} c= (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
then A113: (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) = {p2} by A75, XBOOLE_0:def 10;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A114: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A68, XBOOLE_1:3, XBOOLE_1:26;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[0 ,1]|) by A105, XBOOLE_0:def 4;
then {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[0 ,1]|) by ZFMISC_1:37;
then A115: (LSeg p1,p2) /\ (LSeg p1,|[0 ,1]|) = {p1} by A90, XBOOLE_0:def 10;
A116: P1 /\ P2 = ((LSeg p1,p2) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg p1,p2) /\ ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,1]|,p2))) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}) by A115, A113, XBOOLE_1:23
.= {p1} \/ ((((LSeg p1,p2) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2})) by A114, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by XBOOLE_1:4 ;

A117: now

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

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

p1 in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {} by A118, Lm22, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {p1} by A97, A118, TOPREAL1:21, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by A116; :: thesis: verum

end;

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

now

assume |[0 ,1]| in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) ; :: thesis: contradiction
then |[0 ,1]| in LSeg p1,p2 by XBOOLE_0:def 4;
then p1 `1 = 0 by A13, A15, A69, A74, Lm6, TOPREAL1:9;
hence contradiction by A13, A16, A119, EUCLID:57; :: thesis: verum

end;

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

end;

end;

end;

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

now

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

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

p2 in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {} by A121, Lm27, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {p2} by A120, A121, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A117, ENUMSET1:41; :: thesis: verum

end;

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

now

assume |[1,1]| in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: contradiction
then |[1,1]| in LSeg p1,p2 by XBOOLE_0:def 4;
then |[1,1]| `1 <= p2 `1 by A13, A69, A74, TOPREAL1:9;
then p2 `1 = 1 by A69, A70, Lm10, XXREAL_0:1;
hence contradiction by A69, A72, A122, EUCLID:57; :: thesis: verum

end;

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

end;

end;

end;

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

end;

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

A124: (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 A125: a in (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A126: p in LSeg |[0 ,1]|,p2 by A125, XBOOLE_0:def 4;
|[0 ,1]| `1 <= p2 `1 by A69, A71, EUCLID:56;
then A127: p `1 <= p2 `1 by A126, TOPREAL1:9;
A128: p in LSeg p2,p1 by A125, XBOOLE_0:def 4;
then A129: p `2 <= p1 `2 by A13, A16, A69, A72, TOPREAL1:10;
p2 `1 <= p `1 by A13, A69, A123, A128, TOPREAL1:9;
then A130: p2 `1 = p `1 by A127, XXREAL_0:1;
p2 `2 <= p `2 by A13, A16, A69, A72, A128, TOPREAL1:10;
then p `2 = 1 by A13, A16, A69, A72, A129, XXREAL_0:1;
then p = |[(p2 `1 ),1]| by A130, EUCLID:57
.= p2 by A69, A72, EUCLID:57 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

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

A132: now

consider a being Element of (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2);
assume A133: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} ; :: thesis: contradiction
then reconsider p = a as Point of (TOP-REAL 2) by TARSKI:def 3;
A134: p in LSeg p1,|[1,1]| by A133, XBOOLE_0:def 4;
A135: p in LSeg |[0 ,1]|,p2 by A133, XBOOLE_0:def 4;
|[0 ,1]| `1 <= p2 `1 by A69, A71, EUCLID:56;
then A136: p `1 <= p2 `1 by A135, TOPREAL1:9;
p1 `1 <= |[1,1]| `1 by A13, A14, EUCLID:56;
then p1 `1 <= p `1 by A134, TOPREAL1:9;
hence contradiction by A13, A69, A123, A136, XXREAL_0:2; :: thesis: verum

end;

A137: ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by XBOOLE_1:23
.= {|[0 ,0 ]|} by Lm3, TOPREAL1:23 ;
(LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by Lm9, Lm11, TOPREAL1:15, TOPREAL1:16, TOPREAL1:22;
then A138: ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,1]|,|[0 ,1]| by A137, TOPREAL1:16;

now

assume |[1,1]| in (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) ; :: thesis: contradiction
then A139: |[1,1]| in LSeg |[0 ,1]|,p2 by XBOOLE_0:def 4;
|[0 ,1]| `1 <= p2 `1 by A69, A71, EUCLID:56;
then |[1,1]| `1 <= p2 `1 by A139, TOPREAL1:9;
hence contradiction by A14, A69, A70, A123, Lm10, XXREAL_0:1; :: thesis: verum

end;

then A140: {|[1,1]|} <> (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A66, Lm23, TOPREAL1:12, XBOOLE_1:26;
then A141: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {} by A140, TOPREAL1:24, ZFMISC_1:39;
|[1,1]| in LSeg p1,|[1,1]| by RLTOPSP1:69;
then A142: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {} by Lm27, XBOOLE_0:def 4;

now

assume |[0 ,1]| in (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) ; :: thesis: contradiction
then A143: |[0 ,1]| in LSeg p1,|[1,1]| by XBOOLE_0:def 4;
p1 `1 <= |[1,1]| `1 by A13, A14, EUCLID:56;
hence contradiction by A13, A71, A123, A143, Lm6, TOPREAL1:9; :: thesis: verum

end;

then A144: {|[0 ,1]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by ZFMISC_1:37;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, Lm26, TOPREAL1:12, XBOOLE_1:26;
then A145: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A144, TOPREAL1:21, ZFMISC_1:39;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
then A146: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by A68, XBOOLE_1:3, XBOOLE_1:26;
A147: (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) c= {p1}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) or a in {p1} )
assume A148: a in (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A149: p in LSeg p1,|[1,1]| by A148, XBOOLE_0:def 4;
p1 `1 <= |[1,1]| `1 by A13, A14, EUCLID:56;
then A150: p1 `1 <= p `1 by A149, TOPREAL1:9;
A151: p in LSeg p2,p1 by A148, XBOOLE_0:def 4;
then A152: p `2 <= p1 `2 by A13, A16, A69, A72, TOPREAL1:10;
p `1 <= p1 `1 by A13, A69, A123, A151, TOPREAL1:9;
then A153: p1 `1 = p `1 by A150, XXREAL_0:1;
p2 `2 <= p `2 by A13, A16, A69, A72, A151, TOPREAL1:10;
then p `2 = 1 by A13, A16, A69, A72, A152, XXREAL_0:1;
then p = |[(p1 `1 ),1]| by A153, EUCLID:57
.= p1 by A13, A16, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

A154: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,1]|} by A3, Lm26, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;
|[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then A155: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} by Lm22, XBOOLE_0:def 4;
(LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) c= {|[0 ,1]|} by A66, Lm23, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
then A156: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) = {|[0 ,1]|} by A155, ZFMISC_1:39;
take P1 = LSeg p1,p2; :: thesis: ex P2 being Element of K21(the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg p1,|[1,1]|) \/ ((((LSeg |[1,0 ]|,|[1,1]|) \/ (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 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A157: p1 in LSeg p1,|[1,1]| by RLTOPSP1:69;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:15; :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A158: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} by TOPREAL1:25, XBOOLE_0:def 7;
(LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A66, Lm23, TOPREAL1:12, XBOOLE_1:26;
then A159: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by A158, XBOOLE_1:3;
(((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) /\ (LSeg |[0 ,1]|,p2) = (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) /\ (LSeg |[0 ,1]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= (((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2))) \/ {|[0 ,1]|} by A156, XBOOLE_1:23
.= {|[0 ,1]|} by A141, A159 ;
then A160: (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2) is_an_arc_of |[1,1]|,p2 by A138, TOPREAL1:16;
(LSeg p1,|[1,1]|) /\ ((((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)) = ((LSeg p1,|[1,1]|) /\ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[1,1]|) /\ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A132, XBOOLE_1:23
.= ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) by A145, XBOOLE_1:23
.= {|[1,1]|} by A131, A154, A142, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A160, TOPREAL1:17; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = ((LSeg p2,p1) \/ (LSeg p1,|[1,1]|)) \/ ((((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2)) by XBOOLE_1:4
.= ((LSeg |[0 ,1]|,p2) \/ ((LSeg p2,p1) \/ (LSeg p1,|[1,1]|))) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by XBOOLE_1:4
.= (LSeg |[0 ,1]|,|[1,1]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by A3, A66, TOPREAL1:13
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A161: p2 in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
p2 in LSeg p1,p2 by RLTOPSP1:69;
then p2 in (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) by A161, XBOOLE_0:def 4;
then {p2} c= (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
then A162: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) = {p2} by A124, XBOOLE_0:def 10;
p1 in LSeg p1,p2 by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) by A157, XBOOLE_0:def 4;
then {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) = {p1} by A147, XBOOLE_0:def 10;
then A163: P1 /\ P2 = {p1} \/ ((LSeg p1,p2) /\ ((((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,1]|,p2))) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) by A162, XBOOLE_1:23
.= {p1} \/ ((((LSeg p1,p2) /\ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2})) by A146, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ (((LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by XBOOLE_1:4 ;
A164: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, A66, TOPREAL1:12, XBOOLE_1:26;

A165: now

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

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

p2 in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {} by A166, Lm22, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {p2} by A164, A166, TOPREAL1:21, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2} by A163; :: thesis: verum

end;

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

now

assume |[0 ,1]| in (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) ; :: thesis: contradiction
then |[0 ,1]| in LSeg p2,p1 by XBOOLE_0:def 4;
then p2 `1 = 0 by A13, A69, A71, A123, Lm6, TOPREAL1:9;
hence contradiction by A69, A72, A167, EUCLID:57; :: thesis: verum

end;

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

end;

end;

end;

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

now

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

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

p1 in LSeg p1,p2 by RLTOPSP1:69;
then (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {} by A169, Lm27, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {p1} by A168, A169, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A165, ENUMSET1:41; :: thesis: verum

end;

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

now

assume |[1,1]| in (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) ; :: thesis: contradiction
then |[1,1]| in LSeg p2,p1 by XBOOLE_0:def 4;
then |[1,1]| `1 <= p1 `1 by A13, A69, A123, TOPREAL1:9;
then p1 `1 = 1 by A13, A14, Lm10, XXREAL_0:1;
hence contradiction by A13, A16, A170, EUCLID:57; :: thesis: verum

end;

then {|[1,1]|} <> (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
then (LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A168, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A165, 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 A171: 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} )

|[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 by RLTOPSP1:69;
then A172: (LSeg |[0 ,1]|,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} by Lm20, XBOOLE_0:def 4;
LSeg |[0 ,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| by A171, Lm21, TOPREAL1:12;
then (LSeg |[0 ,1]|,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= {|[0 ,0 ]|} by TOPREAL1:23, XBOOLE_1:27;
then (LSeg |[0 ,1]|,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|} by A172, ZFMISC_1:39;
then A173: (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,p2) is_an_arc_of |[0 ,1]|,p2 by Lm5, Lm7, TOPREAL1:18;
LSeg p2,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[1,0 ]| by A171, Lm21, TOPREAL1:12;
then A174: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A11, Lm2, XBOOLE_1:3, XBOOLE_1:27;
|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then A175: |[1,0 ]| in (LSeg |[1,1]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) by Lm25, XBOOLE_0:def 4;
LSeg |[1,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| by A171, Lm24, TOPREAL1:12;
then (LSeg |[1,1]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by XBOOLE_1:27;
then (LSeg |[1,1]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} by A175, TOPREAL1:22, ZFMISC_1:39;
then A176: (LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[1,1]|,p2 by Lm9, Lm11, TOPREAL1:18;
take P1 = ((LSeg p1,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (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 ,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} )
A177: (LSeg p1,|[1,1]|) \/ (LSeg p1,|[0 ,1]|) = LSeg |[0 ,1]|,|[1,1]| by A3, TOPREAL1:11;
A178: LSeg p2,|[1,0 ]| c= LSeg |[0 ,0 ]|,|[1,0 ]| by A171, Lm24, TOPREAL1:12;
then A179: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A8, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A180: (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A171, Lm21, TOPREAL1:12, XBOOLE_1:26;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) by A3, Lm26, TOPREAL1:12, XBOOLE_1:26;
then A181: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A180, Lm2, XBOOLE_1:1, XBOOLE_1:3;
A182: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A11, A178, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A183: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A171, TOPREAL1:14;
(LSeg p1,|[1,1]|) /\ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2)) = ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= {|[1,1]|} by A6, A10, A179, ZFMISC_1:39 ;
then (LSeg p1,|[1,1]|) \/ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2)) is_an_arc_of p1,p2 by A176, 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} )
A184: ex q2 being Point of (TOP-REAL 2) st
( q2 = p2 & q2 `1 <= 1 & q2 `1 >= 0 & q2 `2 = 0 ) by A171, TOPREAL1:19;
(LSeg p1,|[0 ,1]|) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,p2)) = ((LSeg |[0 ,1]|,p1) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2)) by XBOOLE_1:23
.= {|[0 ,1]|} by A7, A5, A174, TOPREAL1:21, ZFMISC_1:39 ;
then (LSeg p1,|[0 ,1]|) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,p2)) is_an_arc_of p1,p2 by A173, 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} )
(LSeg |[1,0 ]|,p2) \/ (LSeg |[0 ,0 ]|,p2) = LSeg |[0 ,0 ]|,|[1,0 ]| by A171, TOPREAL1:11;
hence R^2-unit_square = (LSeg |[0 ,1]|,|[1,1]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ ((LSeg |[1,0 ]|,p2) \/ (LSeg |[0 ,0 ]|,p2))) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by TOPREAL1:def 4, XBOOLE_1:4
.= (LSeg |[0 ,1]|,|[1,1]|) \/ ((((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2)) \/ (LSeg |[0 ,0 ]|,p2)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) by XBOOLE_1:4
.= (LSeg |[0 ,1]|,|[1,1]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:4
.= (LSeg p1,|[1,1]|) \/ ((((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,p2))) \/ (LSeg p1,|[0 ,1]|)) by A177, XBOOLE_1:4
.= (LSeg p1,|[1,1]|) \/ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2)) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,p2)) \/ (LSeg p1,|[0 ,1]|))) by XBOOLE_1:4
.= ((LSeg p1,|[1,1]|) \/ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2))) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,p2)) \/ (LSeg p1,|[0 ,1]|)) by XBOOLE_1:4
.= (((LSeg p1,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[1,0 ]|,p2)) \/ ((LSeg p1,|[0 ,1]|) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4 ;
:: thesis: P1 /\ P2 = {p1,p2}
A185: (LSeg p1,|[1,1]|) /\ (LSeg p1,|[0 ,1]|) = {p1} by A3, TOPREAL1:14;
A186: P1 /\ P2 = (((LSeg p1,|[1,1]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:23
.= (((LSeg p1,|[1,1]|) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:23
.= ((((LSeg p1,|[1,1]|) /\ ((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:23
.= ((((LSeg p1,|[1,1]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) by A181, XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (((LSeg |[1,0 ]|,|[1,1]|) /\ ((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) by A185, XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ ((LSeg |[1,0 ]|,p2) /\ (((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ (LSeg |[0 ,0 ]|,p2))) by XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) by A183, Lm3, XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ ((((LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A182 ;

A187: now

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

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

then (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg p1,|[0 ,1]|) = (LSeg |[1,0 ]|,|[1,1]|) /\ {|[0 ,1]|} by RLTOPSP1:71
.= {} by Lm1, Lm15 ;
hence P1 /\ P2 = ({p1} \/ ((LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2))) \/ (((LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ {p2}) by A186, A188, TOPREAL1:21; :: thesis: verum

end;

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

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

end;

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

now

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

end;

then A192: {|[1,1]|} <> (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg p1,|[0 ,1]|) by ZFMISC_1:37;
(LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg p1,|[0 ,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, Lm23, TOPREAL1:12, XBOOLE_1:26;
then A193: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg p1,|[0 ,1]|) = {} by A192, TOPREAL1:24, ZFMISC_1:39;

now

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

end;

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

end;

end;

end;

now

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

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

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

end;

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

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

end;

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

now

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

end;

then A200: {|[0 ,0 ]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by ZFMISC_1:37;
(LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A171, Lm24, TOPREAL1:12, XBOOLE_1:26;
then A201: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A200, TOPREAL1:23, ZFMISC_1:39;

now

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

end;

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

end;

end;

end;

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

end;

suppose A204: 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 A205: LSeg |[1,1]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by Lm27, TOPREAL1:12;
LSeg p1,|[1,1]| c= LSeg |[0 ,1]|,|[1,1]| by A3, Lm26, TOPREAL1:12;
then A206: (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by A205, XBOOLE_1:27;
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,|[0 ,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 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A207: |[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then A208: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} by Lm24, XBOOLE_0:def 4;
|[1,1]| in LSeg p1,|[1,1]| by RLTOPSP1:69;
then (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} by A207, XBOOLE_0:def 4;
then A209: (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} by A206, TOPREAL1:24, ZFMISC_1:39;
( p1 <> |[1,1]| or |[1,1]| <> p2 ) by A1;
hence P1 is_an_arc_of p1,p2 by A209, TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A210: LSeg |[0 ,1]|,|[1,1]| = (LSeg p1,|[1,1]|) \/ (LSeg p1,|[0 ,1]|) by A3, TOPREAL1:11;
A211: LSeg |[0 ,0 ]|,|[1,0 ]| is_an_arc_of |[0 ,0 ]|,|[1,0 ]| by Lm4, Lm8, TOPREAL1:15;
LSeg |[0 ,0 ]|,|[0 ,1]| is_an_arc_of |[0 ,1]|,|[0 ,0 ]| by Lm5, Lm7, TOPREAL1:15;
then A212: (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) is_an_arc_of |[0 ,1]|,|[1,0 ]| by A211, TOPREAL1:5, TOPREAL1:23;
A213: (LSeg |[1,1]|,p2) /\ (LSeg |[1,0 ]|,p2) = {p2} by A204, TOPREAL1:14;
A214: LSeg |[1,0 ]|,|[1,1]| = (LSeg |[1,0 ]|,p2) \/ (LSeg |[1,1]|,p2) by A204, TOPREAL1:11;
A215: LSeg |[1,0 ]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A204, Lm25, TOPREAL1:12;
then A216: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,0 ]|} by TOPREAL1:22, XBOOLE_1:27;
A217: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) by A204, TOPREAL1:19;

now

A218: |[1,0 ]| `2 <= p2 `2 by A217, EUCLID:56;
assume A219: |[1,1]| in (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) ; :: thesis: contradiction
then A220: |[1,1]| in LSeg |[0 ,1]|,p1 by XBOOLE_0:def 4;
|[1,1]| in LSeg |[1,0 ]|,p2 by A219, XBOOLE_0:def 4;
then |[1,1]| `2 <= p2 `2 by A218, TOPREAL1:10;
then A221: |[1,1]| `2 = p2 `2 by A217, Lm11, XXREAL_0:1;
|[0 ,1]| `1 <= p1 `1 by A13, A15, EUCLID:56;
then |[1,1]| `1 <= p1 `1 by A220, TOPREAL1:9;
then |[1,1]| `1 = p1 `1 by A13, A14, Lm10, XXREAL_0:1;
then p1 = |[(|[1,1]| `1 ),(|[1,1]| `2 )]| by A13, A16, Lm11, EUCLID:57
.= p2 by A217, A221, Lm10, EUCLID:57 ;
hence contradiction by A1; :: thesis: verum

end;

then A222: {|[1,1]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
A223: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A215, Lm3, XBOOLE_1:3, XBOOLE_1:26;
((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) /\ (LSeg |[1,0 ]|,p2) = ((LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2)) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= {|[1,0 ]|} by A223, A216, A208, ZFMISC_1:39 ;
then A224: ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[0 ,1]|,p2 by A212, TOPREAL1:16;
A225: LSeg p2,|[1,1]| c= LSeg |[1,0 ]|,|[1,1]| by A204, Lm27, TOPREAL1:12;
then A226: (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,1]|} by A11, A215, TOPREAL1:24, XBOOLE_1:27;
then A227: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A222, ZFMISC_1:39;
(LSeg p1,|[0 ,1]|) /\ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)) = ((LSeg p1,|[0 ,1]|) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2)) by XBOOLE_1:23
.= ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) by A227, XBOOLE_1:23
.= {|[0 ,1]|} by A12, A7, A5, TOPREAL1:21, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A224, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg |[1,1]|,p2) \/ ((LSeg p1,|[1,1]|) \/ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,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 |[1,1]|,p2) by A210, XBOOLE_1:4
.= (LSeg |[0 ,1]|,|[1,1]|) \/ ((((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)) \/ (LSeg |[1,1]|,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 |[1,1]|,p2))) by XBOOLE_1:4
.= (LSeg |[0 ,1]|,|[1,1]|) \/ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|))) by A214, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A228: {p1} = (LSeg p1,|[1,1]|) /\ (LSeg p1,|[0 ,1]|) by A3, TOPREAL1:14;
A229: P1 /\ P2 = ((LSeg p1,|[1,1]|) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)))) \/ ((LSeg |[1,1]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)))) by XBOOLE_1:23
.= (((LSeg p1,|[1,1]|) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)))) \/ ((LSeg |[1,1]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,1]|) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)))) \/ ((LSeg |[1,1]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)))) by A228, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)))) \/ ((LSeg |[1,1]|,p2) /\ ((LSeg p1,|[0 ,1]|) \/ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ ((LSeg |[1,1]|,p2) /\ (((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2)))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ (((LSeg |[1,1]|,p2) /\ ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2})) by A213, XBOOLE_1:23
.= ({p1} \/ ((((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ ((((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2)))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ (((LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2})) by A9, A226 ;

A230: now

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

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

then A232: not p2 in LSeg p1,|[1,1]| by A8, Lm7, Lm9, Lm11, TOPREAL1:10;
(LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = (LSeg p1,|[1,1]|) /\ {p2} by A231, RLTOPSP1:71
.= {} by A232, Lm1 ;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) by A229, A231, TOPREAL1:22; :: thesis: verum

end;

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

then p2 in LSeg p1,|[1,1]| by RLTOPSP1:69;
then A234: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) <> {} by A233, Lm27, XBOOLE_0:def 4;
(LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= {p2} by A8, A233, TOPREAL1:24, XBOOLE_1:27;
then A235: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {p2} by A234, ZFMISC_1:39;
(LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[1,1]|} /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A233, RLTOPSP1:71
.= {} by Lm1, Lm19 ;
hence P1 /\ P2 = (({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) by A229, A235, XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ ((((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ ({p2} \/ {p2})) by XBOOLE_1:4
.= ({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) ;
:: thesis: verum

end;

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

now

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

end;

then A238: {|[1,1]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
(LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,1]|} by A8, A215, TOPREAL1:24, XBOOLE_1:27;
then A239: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A238, ZFMISC_1:39;

now

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

end;

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

end;

end;

end;

now

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

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

then A243: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|) = (LSeg |[1,1]|,p2) /\ {p1} by RLTOPSP1:71;
not p1 in LSeg |[1,1]|,p2 by A225, A242, Lm6, Lm8, Lm10, TOPREAL1:9;
then (LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A243, Lm1;
hence P1 /\ P2 = {p1,p2} by A230, A242, ENUMSET1:41, TOPREAL1:21; :: thesis: verum

end;

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

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

end;

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

now

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

end;

then A249: {|[1,1]|} <> (LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|) by ZFMISC_1:37;
(LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A11, A225, XBOOLE_1:27;
then A250: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A249, TOPREAL1:24, ZFMISC_1:39;

now

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

end;

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

end;

end;

end;

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

end;

end;