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

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

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

then A16: ex q2 being Point of (TOP-REAL 2) st
( q2 = p2 & q2 `1 = 0 & q2 `2 <= 1 & q2 `2 >= 0 ) by TOPREAL1:19;
A17: ( p1 <> |[0 ,1]| or p2 <> |[0 ,1]| ) by A1;
take P1 = (LSeg p1,|[0 ,1]|) \/ (LSeg |[0 ,1]|,p2); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg p1,|[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} )
( |[0 ,1]| in LSeg p1,|[0 ,1]| & |[0 ,1]| in LSeg |[0 ,1]|,p2 ) by RLTOPSP1:69;
then ( LSeg p1,|[0 ,1]| c= LSeg |[0 ,1]|,|[1,1]| & LSeg |[0 ,1]|,p2 c= LSeg |[0 ,0 ]|,|[0 ,1]| & |[0 ,1]| in (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) ) by A3, A15, Lm15, Lm16, TOPREAL1:12, XBOOLE_0:def 4;
then ( (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) & (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} ) by XBOOLE_1:27;
then (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) = {|[0 ,1]|} by TOPREAL1:21, ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by A17, TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
( LSeg |[0 ,0 ]|,|[1,0 ]| is_an_arc_of |[1,0 ]|,|[0 ,0 ]| & LSeg |[1,0 ]|,|[1,1]| is_an_arc_of |[1,1]|,|[1,0 ]| ) by Lm4, TOPREAL1:15;
then A18: (LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by TOPREAL1:5, TOPREAL1:22;
A19: ( LSeg |[0 ,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[0 ,1]| & |[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 ) by A15, Lm13, RLTOPSP1:69, TOPREAL1:12;
then A20: ( (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= {|[0 ,0 ]|} & {} <> (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) ) by Lm14, TOPREAL1:23, XBOOLE_0:def 4, XBOOLE_1:26;
A21: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A19, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A22: LSeg p2,|[0 ,1]| c= LSeg |[0 ,0 ]|,|[0 ,1]| by A15, Lm15, TOPREAL1:12;
((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 A20, A21, ZFMISC_1:39 ;
then A23: ((LSeg |[0 ,0 ]|,|[1,0 ]|) \/ (LSeg |[1,0 ]|,|[1,1]|)) \/ (LSeg |[0 ,0 ]|,p2) is_an_arc_of |[1,1]|,p2 by A18, TOPREAL1:16;
(LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A8, A19, XBOOLE_1:27;
then A24: ( (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;

A25: now

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

end;

(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 A24, A25, XBOOLE_1:23, ZFMISC_1:37
.= {|[1,1]|} by A12, A13, A14, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A23, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A27: (LSeg p1,|[0 ,1]|) \/ (LSeg p1,|[1,1]|) = LSeg |[0 ,1]|,|[1,1]| by A3, TOPREAL1:11;
A28: (LSeg |[0 ,0 ]|,p2) \/ (LSeg |[0 ,1]|,p2) = LSeg |[0 ,0 ]|,|[0 ,1]| by A15, TOPREAL1:11;
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 A27, 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 A28, TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A29: {p1} = (LSeg p1,|[0 ,1]|) /\ (LSeg p1,|[1,1]|) by A3, TOPREAL1:14;
A30: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A15, TOPREAL1:14;
A31: (LSeg |[0 ,1]|,p2) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A22, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A32: 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 A29, 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 A9, A30, 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 A31 ;

A33: now

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

suppose A34: 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 (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {p1} /\ (LSeg |[1,0 ]|,|[1,1]|) by RLTOPSP1:71;
then A35: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A34, Lm1, Lm8;
A36: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|) c= {p1} by A22, A34, TOPREAL1:21, XBOOLE_1:27;
p1 in LSeg |[0 ,1]|,p2 by A34, RLTOPSP1:69;
then (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|) <> {} by A34, Lm16, XBOOLE_0:def 4;
then (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|) = {p1} by A36, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ({p1} \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2)))) \/ (((LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ {p2}) by A32, A35, 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 A37: 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 A38: (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|) = (LSeg |[0 ,1]|,p2) /\ {p1} by RLTOPSP1:71;
not p1 in LSeg |[0 ,1]|,p2 by A16, A37, Lm4, TOPREAL1:9;
then (LSeg |[0 ,1]|,p2) /\ (LSeg p1,|[1,1]|) = {} by A38, 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 A32, A37, 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 A39: ( 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})

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

now

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

end;

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

now

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

end;

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

end;

end;

end;

now

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

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

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

now

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

end;

then {|[0 ,1]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
then A45: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A44, TOPREAL1:21, ZFMISC_1:39;
A46: (LSeg |[0 ,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= {|[0 ,0 ]|} by A22, TOPREAL1:23, XBOOLE_1:27;

now

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

end;

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

end;

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

then A48: (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 A7, Lm4, TOPREAL1:10;
then (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A48, Lm1;
hence P1 /\ P2 = {p1,p2} by A33, A47, ENUMSET1:41, TOPREAL1:23; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

suppose A52: 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 consider q being Point of (TOP-REAL 2) such that
A53: q = p2 and
A54: ( q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) by TOPREAL1:19;
A55: ( q1 = |[(q1 `1 ),(q1 `2 )]| & q = |[(q `1 ),(q `2 )]| ) by EUCLID:57;
A56: LSeg p2,|[1,1]| c= LSeg |[0 ,1]|,|[1,1]| by A52, Lm19, TOPREAL1:12;
A57: LSeg p2,|[0 ,1]| c= LSeg |[0 ,1]|,|[1,1]| by A52, Lm16, TOPREAL1:12;
A58: LSeg p1,p2 c= LSeg |[0 ,1]|,|[1,1]| by A3, A52, TOPREAL1:12;

now

per cases ( q1 `1 < q `1 or q `1 < q1 `1 ) by A1, A5, A6, A53, A54, A55, XXREAL_0:1;

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

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

A60: now

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

end;

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

now

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

end;

then {|[1,1]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) by ZFMISC_1:37;
then A63: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {} by A62, ZFMISC_1:39;
( (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} ) by A7, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A64: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by XBOOLE_1:3;
A65: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, Lm16, TOPREAL1:12, XBOOLE_1:26;
|[0 ,1]| in LSeg p1,|[0 ,1]| by RLTOPSP1:69;
then A66: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) <> {} by Lm15, XBOOLE_0:def 4;
A67: (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 A60, XBOOLE_1:23
.= ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|)) \/ ((LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) by A63, XBOOLE_1:23
.= {|[0 ,1]|} by A64, A65, A66, TOPREAL1:21, ZFMISC_1:39 ;
A68: (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) is_an_arc_of |[0 ,1]|,|[1,0 ]| by Lm4, TOPREAL1:15, TOPREAL1:16, TOPREAL1:23;
((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 ;
then A69: ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,|[1,1]|) is_an_arc_of |[0 ,1]|,|[1,1]| by A68, TOPREAL1:16;
A70: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A52, Lm19, TOPREAL1:12, XBOOLE_1:26;
|[1,1]| in LSeg |[1,1]|,p2 by RLTOPSP1:69;
then (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} by Lm20, XBOOLE_0:def 4;
then A71: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} by A70, TOPREAL1:24, ZFMISC_1:39;
A72: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) c= {|[0 ,1]|} by A52, Lm19, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;

now

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

end;

then {|[0 ,1]|} <> (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) by ZFMISC_1:37;
then A73: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,1]|,p2) = {} by A72, ZFMISC_1:39;
( (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} ) by A56, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A74: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,1]|,p2) = {} by 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 A71, XBOOLE_1:23
.= {|[1,1]|} by A73, A74 ;
then (((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 A69, TOPREAL1:16;
hence P2 is_an_arc_of p1,p2 by A67, 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, A52, 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}
( p1 in LSeg p1,p2 & p1 in LSeg p1,|[0 ,1]| ) by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[0 ,1]|) by XBOOLE_0:def 4;
then A75: {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[0 ,1]|) by ZFMISC_1:37;
(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 A76: a in (LSeg p1,p2) /\ (LSeg p1,|[0 ,1]|) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
( p in LSeg p1,p2 & p in LSeg |[0 ,1]|,p1 & p1 `2 <= p2 `2 & p1 `1 <= p2 `1 & |[0 ,1]| `1 <= p1 `1 ) by A5, A6, A53, A54, A59, A76, EUCLID:56, XBOOLE_0:def 4;
then ( p1 `2 <= p `2 & p `2 <= p2 `2 & p1 `1 <= p `1 & p `1 <= p1 `1 ) by TOPREAL1:9, TOPREAL1:10;
then ( p1 `1 = p `1 & p `2 = 1 ) by A5, A6, A53, A54, XXREAL_0:1;
then p = |[(p1 `1 ),1]| by EUCLID:57
.= p1 by A5, A6, EUCLID:57 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

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

proof

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

end;

then A80: (LSeg p1,p2) /\ (LSeg |[1,1]|,p2) = {p2} by A78, XBOOLE_0:def 10;
( (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} ) by A58, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A81: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by XBOOLE_1:3;
A82: 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 A77, A80, 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 A81, 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 ;
A83: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, A52, TOPREAL1:12, XBOOLE_1:26;

A84: now

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

suppose A85: 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 A85, Lm15, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {p1} by A83, A85, TOPREAL1:21, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by A82; :: thesis: verum

end;

suppose A86: 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 & p1 `1 <= p2 `1 ) by A5, A53, A59, XBOOLE_0:def 4;
then p1 `1 = 0 by A5, A6, Lm4, TOPREAL1:9;
hence contradiction by A5, A6, A86, 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 A83, TOPREAL1:21, ZFMISC_1:39;
hence P1 /\ P2 = {p1} \/ (((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ {p2}) by A82; :: thesis: verum

end;

end;

end;

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

now

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

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

end;

suppose A89: 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 & p1 `1 <= p2 `1 ) by A5, A53, A59, XBOOLE_0:def 4;
then |[1,1]| `1 <= p2 `1 by TOPREAL1:9;
then p2 `1 = 1 by A53, A54, Lm4, XXREAL_0:1;
hence contradiction by A53, A54, A89, 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 A87, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A84, ENUMSET1:41; :: thesis: verum

end;

end;

end;

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

end;

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

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

A91: now

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

end;

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

now

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

end;

then {|[0 ,1]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by ZFMISC_1:37;
then A94: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A93, TOPREAL1:21, ZFMISC_1:39;
( (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} ) by A8, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A95: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by XBOOLE_1:3;
A96: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) c= {|[1,1]|} by A3, Lm19, TOPREAL1:12, TOPREAL1:24, XBOOLE_1:26;
|[1,1]| in LSeg p1,|[1,1]| by RLTOPSP1:69;
then A97: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) <> {} by Lm20, XBOOLE_0:def 4;
A98: (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 A91, XBOOLE_1:23
.= ((LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|)) \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|)) by A94, XBOOLE_1:23
.= {|[1,1]|} by A95, A96, A97, ZFMISC_1:39 ;
A99: (LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) is_an_arc_of |[1,1]|,|[0 ,0 ]| by Lm4, TOPREAL1:15, TOPREAL1:16, TOPREAL1:22;
((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 ;
then A100: ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|) is_an_arc_of |[1,1]|,|[0 ,1]| by A99, TOPREAL1:16;
A101: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) c= {|[0 ,1]|} by A52, Lm16, TOPREAL1:12, TOPREAL1:21, XBOOLE_1:26;
|[0 ,1]| in LSeg |[0 ,1]|,p2 by RLTOPSP1:69;
then (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) <> {} by Lm15, XBOOLE_0:def 4;
then A102: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[0 ,1]|,p2) = {|[0 ,1]|} by A101, ZFMISC_1:39;
A103: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A52, Lm16, TOPREAL1:12, XBOOLE_1:26;

now

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

end;

then {|[1,1]|} <> (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) by ZFMISC_1:37;
then A104: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,p2) = {} by A103, TOPREAL1:24, ZFMISC_1:39;
( (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} ) by A57, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A105: (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,p2) = {} by 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 A102, XBOOLE_1:23
.= {|[0 ,1]|} by A104, A105 ;
then (((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 A100, TOPREAL1:16;
hence P2 is_an_arc_of p1,p2 by A98, 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, A52, TOPREAL1:13
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
( p1 in LSeg p1,p2 & p1 in LSeg p1,|[1,1]| ) by RLTOPSP1:69;
then p1 in (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) by XBOOLE_0:def 4;
then A106: {p1} c= (LSeg p1,p2) /\ (LSeg p1,|[1,1]|) by ZFMISC_1:37;
(LSeg p1,p2) /\ (LSeg p1,|[1,1]|) c= {p1}

proof

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

end;

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

proof

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

end;

then A111: (LSeg p1,p2) /\ (LSeg |[0 ,1]|,p2) = {p2} by A109, XBOOLE_0:def 10;
( (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,1]|,|[1,1]|) = {} ) by A58, TOPREAL1:25, XBOOLE_0:def 7, XBOOLE_1:26;
then A112: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {} by XBOOLE_1:3;
A113: 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 A108, XBOOLE_1:23
.= {p1} \/ (((LSeg p1,p2) /\ (((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) by A111, 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 A112, 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 ;
A114: (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A3, A52, TOPREAL1:12, XBOOLE_1:26;

A115: now

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

suppose A116: 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 A116, Lm15, XBOOLE_0:def 4;
then (LSeg p1,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {p2} by A114, A116, TOPREAL1:21, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2} by A113; :: thesis: verum

end;

suppose A117: 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 & p2 `1 <= p1 `1 ) by A5, A53, A90, XBOOLE_0:def 4;
then p2 `1 = 0 by A53, A54, Lm4, TOPREAL1:9;
hence contradiction by A53, A54, A117, 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 A114, TOPREAL1:21, ZFMISC_1:39;
hence P1 /\ P2 = ({p1} \/ ((LSeg p1,p2) /\ (LSeg |[1,0 ]|,|[1,1]|))) \/ {p2} by A113; :: thesis: verum

end;

end;

end;

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

now

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

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

end;

suppose A120: 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 & p2 `1 <= p1 `1 ) by A5, A53, A90, XBOOLE_0:def 4;
then |[1,1]| `1 <= p1 `1 by TOPREAL1:9;
then p1 `1 = 1 by A5, A6, Lm4, XXREAL_0:1;
hence contradiction by A5, A6, A120, 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 A118, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A115, 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 A121: 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 A122: ex q2 being Point of (TOP-REAL 2) st
( q2 = p2 & q2 `1 <= 1 & q2 `1 >= 0 & q2 `2 = 0 ) by TOPREAL1:19;
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} )
( LSeg |[1,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| & |[1,0 ]| in LSeg |[1,0 ]|,p2 ) by A121, Lm17, RLTOPSP1:69, TOPREAL1:12;
then ( (LSeg |[1,1]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) & |[1,0 ]| in (LSeg |[1,1]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) ) by Lm18, XBOOLE_0:def 4, XBOOLE_1:27;
then (LSeg |[1,1]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) = {|[1,0 ]|} by TOPREAL1:22, ZFMISC_1:39;
then A123: (LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[1,1]|,p2 by Lm4, TOPREAL1:18;
A124: LSeg p2,|[1,0 ]| c= LSeg |[0 ,0 ]|,|[1,0 ]| by A121, Lm17, TOPREAL1:12;
then A125: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A8, Lm2, XBOOLE_1:3, XBOOLE_1:27;
(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 A13, A14, A125, ZFMISC_1:39 ;
then (LSeg p1,|[1,1]|) \/ ((LSeg |[1,0 ]|,|[1,1]|) \/ (LSeg |[1,0 ]|,p2)) is_an_arc_of p1,p2 by A123, TOPREAL1:17;
hence P1 is_an_arc_of p1,p2 by XBOOLE_1:4; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
( LSeg |[0 ,0 ]|,p2 c= LSeg |[0 ,0 ]|,|[1,0 ]| & |[0 ,0 ]| in LSeg |[0 ,0 ]|,p2 ) by A121, Lm14, RLTOPSP1:69, TOPREAL1:12;
then ( (LSeg |[0 ,1]|,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) c= {|[0 ,0 ]|} & (LSeg |[0 ,1]|,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) <> {} ) by Lm13, TOPREAL1:23, XBOOLE_0:def 4, XBOOLE_1:27;
then (LSeg |[0 ,1]|,|[0 ,0 ]|) /\ (LSeg |[0 ,0 ]|,p2) = {|[0 ,0 ]|} by ZFMISC_1:39;
then A126: (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,p2) is_an_arc_of |[0 ,1]|,p2 by Lm4, TOPREAL1:18;
LSeg p2,|[0 ,0 ]| c= LSeg |[0 ,0 ]|,|[1,0 ]| by A121, Lm14, TOPREAL1:12;
then A127: (LSeg p1,|[0 ,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A7, Lm2, XBOOLE_1:3, XBOOLE_1:27;
(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 A10, A11, A127, 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 A126, 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} )
A128: (LSeg |[1,0 ]|,p2) \/ (LSeg |[0 ,0 ]|,p2) = LSeg |[0 ,0 ]|,|[1,0 ]| by A121, TOPREAL1:11;
A129: (LSeg p1,|[1,1]|) \/ (LSeg p1,|[0 ,1]|) = LSeg |[0 ,1]|,|[1,1]| by A3, TOPREAL1:11;
thus 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 A128, 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 A129, 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}
( (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) & (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) ) by A3, A121, Lm14, Lm19, TOPREAL1:12, XBOOLE_1:26;
then A130: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by Lm2, XBOOLE_1:1, XBOOLE_1:3;
A131: (LSeg p1,|[1,1]|) /\ (LSeg p1,|[0 ,1]|) = {p1} by A3, TOPREAL1:14;
A132: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,p2) = {p2} by A121, TOPREAL1:14;
A133: (LSeg |[1,0 ]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A7, A124, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A134: 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 A130, 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 A131, 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 A132, 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 A133 ;

A135: now

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

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

end;

suppose A137: 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, Lm11 ;
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 A134, A137, 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 A138: ( 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})

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

now

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

end;

then {|[0 ,1]|} <> (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by ZFMISC_1:37;
then A140: (LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A139, TOPREAL1:21, ZFMISC_1:39;
A141: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg p1,|[0 ,1]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,1]|,|[1,1]|) by A3, Lm16, TOPREAL1:12, XBOOLE_1:26;

now

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

end;

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

end;

end;

end;

now

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

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

end;

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

end;

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

A145: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A121, Lm14, TOPREAL1:12, XBOOLE_1:26;

now

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

end;

then {|[1,0 ]|} <> (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) by ZFMISC_1:37;
then A146: (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,p2) = {} by A145, TOPREAL1:22, ZFMISC_1:39;
A147: (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) c= (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by A121, Lm17, TOPREAL1:12, XBOOLE_1:26;

now

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

end;

then {|[0 ,0 ]|} <> (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) by ZFMISC_1:37;
then (LSeg |[1,0 ]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A147, TOPREAL1:23, ZFMISC_1:39;
hence P1 /\ P2 = {p1,p2} by A135, A146, ENUMSET1:41; :: 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} )

then A149: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) by TOPREAL1:19;
take P1 = (LSeg p1,|[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} )
( |[1,1]| in LSeg p1,|[1,1]| & |[1,1]| in LSeg |[1,1]|,p2 ) by RLTOPSP1:69;
then ( LSeg p1,|[1,1]| c= LSeg |[0 ,1]|,|[1,1]| & LSeg |[1,1]|,p2 c= LSeg |[1,0 ]|,|[1,1]| & |[1,1]| in (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) ) by A3, A148, Lm19, Lm20, TOPREAL1:12, XBOOLE_0:def 4;
then ( (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) c= (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) & (LSeg |[0 ,1]|,|[1,1]|) /\ (LSeg |[1,0 ]|,|[1,1]|) = {|[1,1]|} & (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) <> {} ) by TOPREAL1:24, XBOOLE_1:27;
then ( (LSeg p1,|[1,1]|) /\ (LSeg |[1,1]|,p2) = {|[1,1]|} & ( p1 <> |[1,1]| or |[1,1]| <> p2 ) ) by A1, ZFMISC_1:39;
hence P1 is_an_arc_of p1,p2 by TOPREAL1:18; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
( LSeg |[0 ,0 ]|,|[0 ,1]| is_an_arc_of |[0 ,1]|,|[0 ,0 ]| & LSeg |[0 ,0 ]|,|[1,0 ]| is_an_arc_of |[0 ,0 ]|,|[1,0 ]| ) by Lm4, TOPREAL1:15;
then A150: (LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|) is_an_arc_of |[0 ,1]|,|[1,0 ]| by TOPREAL1:5, TOPREAL1:23;
A151: LSeg |[1,0 ]|,p2 c= LSeg |[1,0 ]|,|[1,1]| by A148, Lm18, TOPREAL1:12;
then A152: (LSeg |[0 ,0 ]|,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by Lm3, XBOOLE_1:3, XBOOLE_1:26;
|[1,0 ]| in LSeg |[1,0 ]|,p2 by RLTOPSP1:69;
then A153: ( (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,0 ]|} & (LSeg |[0 ,0 ]|,|[1,0 ]|) /\ (LSeg |[1,0 ]|,p2) <> {} ) by A151, Lm17, TOPREAL1:22, XBOOLE_0:def 4, XBOOLE_1:27;
((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 A152, A153, ZFMISC_1:39 ;
then A154: ((LSeg |[0 ,0 ]|,|[0 ,1]|) \/ (LSeg |[0 ,0 ]|,|[1,0 ]|)) \/ (LSeg |[1,0 ]|,p2) is_an_arc_of |[0 ,1]|,p2 by A150, TOPREAL1:16;
A155: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) c= {|[1,1]|} by A7, A151, TOPREAL1:24, XBOOLE_1:27;

now

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

end;

then {|[1,1]|} <> (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) by ZFMISC_1:37;
then A157: (LSeg p1,|[0 ,1]|) /\ (LSeg |[1,0 ]|,p2) = {} by A155, 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 A157, XBOOLE_1:23
.= {|[0 ,1]|} by A9, A10, A11, TOPREAL1:21, ZFMISC_1:39 ;
hence P2 is_an_arc_of p1,p2 by A154, TOPREAL1:17; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A158: LSeg |[0 ,1]|,|[1,1]| = (LSeg p1,|[1,1]|) \/ (LSeg p1,|[0 ,1]|) by A3, TOPREAL1:11;
A159: LSeg |[1,0 ]|,|[1,1]| = (LSeg |[1,0 ]|,p2) \/ (LSeg |[1,1]|,p2) by A148, TOPREAL1:11;
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 A158, 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 A159, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 4, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A160: LSeg p2,|[1,1]| c= LSeg |[1,0 ]|,|[1,1]| by A148, Lm20, TOPREAL1:12;
A161: {p1} = (LSeg p1,|[1,1]|) /\ (LSeg p1,|[0 ,1]|) by A3, TOPREAL1:14;
A162: (LSeg |[1,1]|,p2) /\ (LSeg |[1,0 ]|,p2) = {p2} by A148, TOPREAL1:14;
A163: (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|) = {} by A160, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A164: 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 A161, 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 A162, 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 A12, A163 ;

A165: now

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

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

end;

suppose A168: 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 A169: (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) = {|[1,1]|} /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by RLTOPSP1:71
.= {} by Lm1, Lm12 ;
A170: (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) c= {p2} by A8, A168, TOPREAL1:24, XBOOLE_1:27;
p2 in LSeg p1,|[1,1]| by A168, RLTOPSP1:69;
then (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) <> {} by A168, Lm20, XBOOLE_0:def 4;
then (LSeg p1,|[1,1]|) /\ (LSeg |[1,0 ]|,p2) = {p2} by A170, ZFMISC_1:39;
hence P1 /\ P2 = (({p1} \/ ((LSeg p1,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[0 ,1]|))) \/ {p2}) \/ (((LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|)) \/ {p2}) by A164, A169, 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 A171: ( 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})

A172: (LSeg |[1,1]|,p2) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) c= (LSeg |[1,0 ]|,|[1,1]|) /\ (LSeg |[0 ,0 ]|,|[1,0 ]|) by A160, XBOOLE_1:27;

now

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

end;

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

now

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

end;

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

end;

end;

end;

now

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

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

then A176: (LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|) = (LSeg |[1,1]|,p2) /\ {p1} by RLTOPSP1:71;
not p1 in LSeg |[1,1]|,p2 by A160, A175, Lm4, TOPREAL1:9;
then (LSeg |[1,1]|,p2) /\ (LSeg p1,|[0 ,1]|) = {} by A176, Lm1;
hence P1 /\ P2 = {p1,p2} by A165, A175, ENUMSET1:41, TOPREAL1:21; :: thesis: verum

end;

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

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

end;

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

A181: (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;

now

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

end;

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

now

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

end;

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

end;

end;

end;

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

end;

end;