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

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

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

A19: LSeg (|[0,1]|,|[1,1]|) is_an_arc_of |[1,1]|,|[0,1]| by Lm6, Lm10, TOPREAL1:9;
LSeg (|[1,0]|,|[1,1]|) is_an_arc_of |[1,0]|,|[1,1]| by Lm9, Lm11, TOPREAL1:9;
then A20: (LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is_an_arc_of |[1,0]|,|[0,1]| by A19, TOPREAL1:2, TOPREAL1:18;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
then A21: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A10, XBOOLE_1:3, XBOOLE_1:26;
take P1 = (LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[1,0]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A22: (LSeg (p1,|[0,0]|)) \/ (LSeg (p1,|[1,0]|)) = LSeg (|[0,0]|,|[1,0]|) by A3, TOPREAL1:5;
|[0,1]| in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
then A23: |[0,1]| in (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) by Lm23, XBOOLE_0:def 4;
A24: |[0,0]| in LSeg (|[0,0]|,p2) by RLTOPSP1:68;
|[0,0]| in LSeg (p1,|[0,0]|) by RLTOPSP1:68;
then A25: |[0,0]| in (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,p2)) by A24, XBOOLE_0:def 4;
A26: LSeg (|[0,0]|,p2) c= LSeg (|[0,0]|,|[0,1]|) by A18, Lm20, TOPREAL1:6;
then (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A10, XBOOLE_1:27;
then A27: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,p2)) = {|[0,0]|} by A25, TOPREAL1:17, ZFMISC_1:33;
A28: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 0 & q `2 <= 1 & q `2 >= 0 ) by A18, TOPREAL1:13;

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

A29: p2 `2 <= |[0,1]| `2 by A28, EUCLID:52;
assume A30: |[0,0]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) ; :: thesis: contradiction
then A31: |[0,0]| in LSeg (p1,|[1,0]|) by XBOOLE_0:def 4;
|[0,0]| in LSeg (p2,|[0,1]|) by A30, XBOOLE_0:def 4;
then A32: 0 = p2 `2 by A28, A29, Lm5, TOPREAL1:4;
p1 `1 <= |[1,0]| `1 by A14, A15, EUCLID:52;
then 0 = p1 `1 by A14, A16, A31, Lm4, TOPREAL1:3;
then p1 = |[0,0]| by A14, A17, EUCLID:53
.= p2 by A28, A32, EUCLID:53 ;
hence contradiction by A1; :: thesis: verum

end;

then A33: {|[0,0]|} <> (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) by ZFMISC_1:31;
( p1 <> |[0,0]| or |[0,0]| <> p2 ) by A1;
hence P1 is_an_arc_of p1,p2 by A27, TOPREAL1:12; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A34: {p1} = (LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[1,0]|)) by A3, TOPREAL1:8;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by TOPREAL1:20, XBOOLE_0:def 7;
then A35: (LSeg (|[0,0]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by A26, XBOOLE_1:3, XBOOLE_1:26;
A36: LSeg (p2,|[0,1]|) c= LSeg (|[0,0]|,|[0,1]|) by A18, Lm22, TOPREAL1:6;
then A37: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by XBOOLE_1:27;
A38: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A36, Lm3, XBOOLE_1:3, XBOOLE_1:26;
((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (LSeg (|[0,1]|,p2)) = ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= {|[0,1]|} by A38, A37, A23, TOPREAL1:15, ZFMISC_1:33 ;
then A39: ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2)) is_an_arc_of |[1,0]|,p2 by A20, TOPREAL1:10;
A40: {p2} = (LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,p2)) by A18, TOPREAL1:8;
A41: (LSeg (|[0,1]|,p2)) \/ (LSeg (|[0,0]|,p2)) = LSeg (|[0,0]|,|[0,1]|) by A18, TOPREAL1:5;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A12, A36, XBOOLE_1:27;
then A42: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A33, TOPREAL1:17, ZFMISC_1:33;
(LSeg (p1,|[1,0]|)) /\ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))) = ((LSeg (p1,|[1,0]|)) /\ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[1,0]|,p1)) /\ (LSeg (|[0,1]|,|[1,1]|))) by A42, XBOOLE_1:23
.= {|[1,0]|} by A13, A5, A7, TOPREAL1:16, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A39, TOPREAL1:11; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg (|[0,0]|,p2)) \/ ((LSeg (p1,|[0,0]|)) \/ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))))) by XBOOLE_1:4
.= (LSeg (|[0,0]|,p2)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2)))) by A22, XBOOLE_1:4
.= (LSeg (|[0,0]|,p2)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ (LSeg (|[0,1]|,p2))) by XBOOLE_1:4
.= (LSeg (|[0,0]|,p2)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))) by XBOOLE_1:4
.= (LSeg (|[0,0]|,p2)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2)))) by XBOOLE_1:4
.= (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ (LSeg (|[0,0]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:4
.= R^2-unit_square by A41, TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A43: P1 /\ P2 = ((LSeg (p1,|[0,0]|)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[0,0]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))))) by XBOOLE_1:23
.= (((LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[0,0]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,0]|)) /\ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[0,0]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))))) by A34, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))))) \/ ((LSeg (|[0,0]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,0]|,p2)) /\ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,1]|,p2))))) by A21, XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ (((LSeg (|[0,0]|,p2)) /\ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2})) by A40, XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ ((((LSeg (|[0,0]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})) by A35 ;

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

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

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

A46: p1 in LSeg (p1,|[1,0]|) by RLTOPSP1:68;
p1 in LSeg (|[0,0]|,p2) by A45, RLTOPSP1:68;
then A47: (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|)) <> {} by A46, XBOOLE_0:def 4;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[0,0]|} /\ (LSeg (|[1,0]|,|[1,1]|)) by A45, RLTOPSP1:70;
then A48: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by Lm1, Lm12;
(LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|)) c= {p1} by A18, A45, Lm20, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
then (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|)) = {p1} by A47, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by A43, A48, XBOOLE_1:4
.= (({p1} \/ {p1}) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) ;
:: thesis: verum

end;

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

then A50: (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|)) = (LSeg (|[0,0]|,p2)) /\ {|[1,0]|} by RLTOPSP1:70;
not |[1,0]| in LSeg (|[0,0]|,p2) by A26, Lm4, Lm6, Lm8, TOPREAL1:3;
then (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|)) = {} by A50, Lm1;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by A43, A49, TOPREAL1:16, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) ;
:: thesis: verum

end;

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

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

assume |[0,0]| in (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|)) ; :: thesis: contradiction
then A52: |[0,0]| in LSeg (p1,|[1,0]|) by XBOOLE_0:def 4;
p1 `1 <= |[1,0]| `1 by A14, A15, EUCLID:52;
then 0 = p1 `1 by A14, A16, A52, Lm4, TOPREAL1:3;
hence contradiction by A14, A17, A51, EUCLID:53; :: thesis: verum

end;

then A53: {|[0,0]|} <> (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|)) by ZFMISC_1:31;
(LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|)) c= {|[0,0]|} by A12, A26, TOPREAL1:17, XBOOLE_1:27;
then A54: (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[1,0]|)) = {} by A53, ZFMISC_1:33;

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

assume |[1,0]| in (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; :: thesis: contradiction
then A55: |[1,0]| in LSeg (|[0,0]|,p1) by XBOOLE_0:def 4;
|[0,0]| `1 <= p1 `1 by A14, A16, EUCLID:52;
then |[1,0]| `1 <= p1 `1 by A55, TOPREAL1:3;
then p1 `1 = 1 by A14, A15, Lm8, XXREAL_0:1;
hence contradiction by A14, A17, A51, EUCLID:53; :: thesis: verum

end;

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

end;

end;

end;

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

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

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

|[0,0]| in LSeg (p1,|[0,0]|) by RLTOPSP1:68;
then A58: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) <> {} by A57, Lm20, XBOOLE_0:def 4;
(LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {|[0,0]|} /\ (LSeg (|[0,1]|,|[1,1]|)) by A57, RLTOPSP1:70;
then A59: (LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by Lm1, Lm13;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A10, A36, XBOOLE_1:27;
then (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) = {p2} by A57, A58, TOPREAL1:17, ZFMISC_1:33;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A44, A59, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:1 ;
:: thesis: P1 /\ P2 = {p1,p2}
hence P1 /\ P2 = {p1,p2} ; :: thesis: verum

end;

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

then A61: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) = (LSeg (p1,|[0,0]|)) /\ {|[0,1]|} by RLTOPSP1:70;
not |[0,1]| in LSeg (p1,|[0,0]|) by A10, Lm5, Lm7, Lm9, TOPREAL1:4;
then A62: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A61, Lm1;
hence P1 /\ P2 = {p1,p2} by A44, A60, ENUMSET1:1, TOPREAL1:15; :: thesis: P1 /\ P2 = {p1,p2}
thus P1 /\ P2 = {p1,p2} by A44, A60, A62, ENUMSET1:1, TOPREAL1:15; :: thesis: verum

end;

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

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

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

end;

then A65: {|[0,1]|} <> (LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) by ZFMISC_1:31;
(LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= {|[0,1]|} by A18, Lm20, TOPREAL1:6, TOPREAL1:15, XBOOLE_1:26;
then A66: (LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A65, ZFMISC_1:33;

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

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

end;

then A68: {|[0,0]|} <> (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) by ZFMISC_1:31;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A10, A36, XBOOLE_1:27;
then A69: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A68, TOPREAL1:17, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A44, A66, ENUMSET1:1; :: thesis: P1 /\ P2 = {p1,p2}
thus P1 /\ P2 = {p1,p2} by A44, A69, A66, ENUMSET1:1; :: thesis: verum

end;

end;

end;

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

end;

suppose A70: 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 A71: LSeg (p2,|[1,1]|) c= LSeg (|[0,1]|,|[1,1]|) by Lm26, TOPREAL1:6;
then A72: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A12, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A73: LSeg (p2,|[0,1]|) c= LSeg (|[0,1]|,|[1,1]|) by A70, Lm23, TOPREAL1:6;
then A74: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A10, Lm2, XBOOLE_1:3, XBOOLE_1:27;
take P1 = ((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,|[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,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
|[0,1]| in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
then A75: (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 A70, Lm23, TOPREAL1:6, TOPREAL1:15, XBOOLE_1:26;
then (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) = {|[0,1]|} by A75, ZFMISC_1:33;
then A76: (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2)) is_an_arc_of |[0,0]|,p2 by Lm5, Lm7, TOPREAL1:12;
(LSeg (p1,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) = ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= {|[0,0]|} by A8, A6, A74, TOPREAL1:17, ZFMISC_1:33 ;
then (LSeg (p1,|[0,0]|)) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) is_an_arc_of p1,p2 by A76, TOPREAL1:11;
hence P1 is_an_arc_of p1,p2 by XBOOLE_1:4; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
|[1,1]| in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
then A77: (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 A70, Lm26, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) = {|[1,1]|} by A77, TOPREAL1:18, ZFMISC_1:33;
then A78: (LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,1]|,p2)) is_an_arc_of |[1,0]|,p2 by Lm9, Lm11, TOPREAL1:12;
(LSeg (p1,|[1,0]|)) /\ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,1]|,p2))) = ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= {|[1,0]|} by A5, A7, A72, TOPREAL1:16, ZFMISC_1:33 ;
then (LSeg (p1,|[1,0]|)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,1]|,p2))) is_an_arc_of p1,p2 by A78, TOPREAL1:11;
hence P2 is_an_arc_of p1,p2 by XBOOLE_1:4; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus R^2-unit_square = ((LSeg (|[0,0]|,|[0,1]|)) \/ ((LSeg (|[0,1]|,p2)) \/ (LSeg (|[1,1]|,p2)))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) by A70, TOPREAL1:5, TOPREAL1:def 2
.= (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:4
.= ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) by XBOOLE_1:4
.= ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:4
.= ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ (((LSeg (p1,|[0,0]|)) \/ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,1]|,p2)))) by A3, TOPREAL1:5
.= ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (p1,|[0,0]|)) \/ ((LSeg (p1,|[1,0]|)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:4
.= ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:4
.= ((LSeg (p1,|[0,0]|)) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A79: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) by A70, TOPREAL1:13;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
then A80: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A10, A71, XBOOLE_1:3, XBOOLE_1:27;
A81: (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,0]|)) = {} by A12, A73, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A82: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,1]|,p2)) = {p2} by A70, TOPREAL1:8;
A83: P1 /\ P2 = (((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) \/ ((LSeg (|[0,1]|,p2)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:23
.= (((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2}) by A82, XBOOLE_1:23
.= (((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) \/ ((((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2}) by XBOOLE_1:23
.= (((LSeg (p1,|[0,0]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by A81, XBOOLE_1:23
.= ((((LSeg (p1,|[0,0]|)) /\ ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by A9, A80, XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,|[0,1]|)) /\ ((LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (p1,|[1,0]|))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by Lm3 ;

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

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

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

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

end;

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

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

end;

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

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

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

end;

then A89: {|[0,0]|} <> (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (p1,|[1,0]|)) by ZFMISC_1:31;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (p1,|[1,0]|)) c= {|[0,0]|} by A3, Lm24, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
then A90: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (p1,|[1,0]|)) = {} by A89, ZFMISC_1:33;

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

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

end;

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

end;

end;

end;

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

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

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

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

end;

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

then (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = (LSeg (|[0,0]|,|[0,1]|)) /\ {|[1,1]|} by RLTOPSP1:70;
then (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = {} by Lm1, Lm18;
hence P1 /\ P2 = {p1,p2} by A84, A94, ENUMSET1:1, TOPREAL1:18; :: thesis: verum

end;

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

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

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

end;

then A97: {|[1,1]|} <> (LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) by ZFMISC_1:31;
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {|[1,1]|} by A70, Lm23, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
then A98: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by A97, ZFMISC_1:33;

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

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

end;

then A100: {|[0,1]|} <> (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) by ZFMISC_1:31;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[0,1]|} by A70, Lm26, TOPREAL1:6, TOPREAL1:15, XBOOLE_1:26;
then (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A100, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A84, A98, ENUMSET1:1; :: thesis: verum

end;

end;

end;

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

end;

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

A102: p = |[(p `1),(p `2)]| by EUCLID:53;
A103: LSeg (p1,p2) c= LSeg (|[0,0]|,|[1,0]|) by A3, A101, TOPREAL1:6;
consider q being Point of (TOP-REAL 2) such that
A104: q = p2 and
A105: q `1 <= 1 and
A106: q `1 >= 0 and
A107: q `2 = 0 by A101, TOPREAL1:13;
A108: q = |[(q `1),(q `2)]| by EUCLID:53;

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

per cases ( p `1 < q `1 or q `1 < p `1 ) by A1, A14, A17, A104, A107, A102, A108, XXREAL_0:1;

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

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

assume |[1,0]| in (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; :: thesis: contradiction
then A110: |[1,0]| in LSeg (|[0,0]|,p1) by XBOOLE_0:def 4;
|[0,0]| `1 <= p1 `1 by A14, A16, EUCLID:52;
then |[1,0]| `1 <= p1 `1 by A110, TOPREAL1:3;
hence contradiction by A14, A15, A105, A109, Lm8, XXREAL_0:1; :: thesis: verum

end;

then A111: {|[1,0]|} <> (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {|[1,0]|} by A3, Lm21, TOPREAL1:6, TOPREAL1:16, XBOOLE_1:26;
then A112: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by A111, ZFMISC_1:33;
|[0,0]| in LSeg (p1,|[0,0]|) by RLTOPSP1:68;
then A113: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) <> {} by Lm20, XBOOLE_0:def 4;

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

assume |[0,0]| in (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) ; :: thesis: contradiction
then A114: |[0,0]| in LSeg (p2,|[1,0]|) by XBOOLE_0:def 4;
p2 `1 <= |[1,0]| `1 by A104, A105, EUCLID:52;
hence contradiction by A16, A104, A109, A114, Lm4, TOPREAL1:3; :: thesis: verum

end;

then A115: {|[0,0]|} <> (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) by ZFMISC_1:31;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[0,0]|} by A101, Lm24, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
then A116: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A115, ZFMISC_1:33;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
then A117: (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A103, XBOOLE_1:3, XBOOLE_1:26;
A118: (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) c= {p1}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) or a in {p1} )
assume A119: a in (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A120: p in LSeg (|[0,0]|,p1) by A119, XBOOLE_0:def 4;
|[0,0]| `1 <= p1 `1 by A14, A16, EUCLID:52;
then A121: p `1 <= p1 `1 by A120, TOPREAL1:3;
A122: p in LSeg (p1,p2) by A119, XBOOLE_0:def 4;
then p1 `1 <= p `1 by A14, A104, A109, TOPREAL1:3;
then A123: p1 `1 = p `1 by A121, XXREAL_0:1;
p1 `2 <= p `2 by A14, A17, A104, A107, A122, TOPREAL1:4;
then p `2 = 0 by A14, A17, A104, A107, A122, TOPREAL1:4;
then p = |[(p1 `1),0]| by A123, EUCLID:53
.= p1 by A14, A17, EUCLID:53 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

A124: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, Lm21, TOPREAL1:6, XBOOLE_1:26;
take P1 = LSeg (p1,p2); :: thesis: ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A125: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A101, Lm24, TOPREAL1:6, XBOOLE_1:26;
then A126: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A125, XBOOLE_1:3;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:9; :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A127: ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (LSeg (|[1,0]|,|[1,1]|)) = ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:23
.= {|[1,1]|} by Lm3, TOPREAL1:18 ;
A128: (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) c= {p2}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) or a in {p2} )
assume A129: a in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A130: p in LSeg (p2,|[1,0]|) by A129, XBOOLE_0:def 4;
p2 `1 <= |[1,0]| `1 by A104, A105, EUCLID:52;
then A131: p2 `1 <= p `1 by A130, TOPREAL1:3;
A132: p in LSeg (p1,p2) by A129, XBOOLE_0:def 4;
then p `1 <= p2 `1 by A14, A104, A109, TOPREAL1:3;
then A133: p2 `1 = p `1 by A131, XXREAL_0:1;
p1 `2 <= p `2 by A14, A17, A104, A107, A132, TOPREAL1:4;
then p `2 = 0 by A14, A17, A104, A107, A132, TOPREAL1:4;
then p = |[(p2 `1),0]| by A133, EUCLID:53
.= p2 by A104, A107, EUCLID:53 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

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

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

set a = the Element of (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2));
assume A136: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) <> {} ; :: thesis: contradiction
then reconsider p = the Element of (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) as Point of (TOP-REAL 2) by TARSKI:def 3;
A137: p in LSeg (|[0,0]|,p1) by A136, XBOOLE_0:def 4;
A138: p in LSeg (p2,|[1,0]|) by A136, XBOOLE_0:def 4;
p2 `1 <= |[1,0]| `1 by A104, A105, EUCLID:52;
then A139: p2 `1 <= p `1 by A138, TOPREAL1:3;
|[0,0]| `1 <= p1 `1 by A14, A16, EUCLID:52;
then p `1 <= p1 `1 by A137, TOPREAL1:3;
hence contradiction by A14, A104, A109, A139, XXREAL_0:2; :: thesis: verum

end;

|[1,0]| in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
then A140: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) <> {} by Lm25, XBOOLE_0:def 4;
(LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A101, Lm24, TOPREAL1:6, XBOOLE_1:26;
then A141: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) = {|[1,0]|} by A140, TOPREAL1:16, ZFMISC_1:33;
(LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is_an_arc_of |[0,0]|,|[1,1]| by Lm5, Lm7, TOPREAL1:9, TOPREAL1:10, TOPREAL1:15;
then A142: ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|)) is_an_arc_of |[0,0]|,|[1,0]| by A127, TOPREAL1:10;
(((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) /\ (LSeg (|[1,0]|,p2)) = (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= (((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)))) \/ {|[1,0]|} by A141, XBOOLE_1:23
.= {|[1,0]|} by A116, A126 ;
then A143: (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2)) is_an_arc_of |[0,0]|,p2 by A142, TOPREAL1:10;
(LSeg (p1,|[0,0]|)) /\ ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))) = ((LSeg (p1,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) by A135, XBOOLE_1:23
.= ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) by A112, XBOOLE_1:23
.= {|[0,0]|} by A134, A124, A113, TOPREAL1:17, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A143, TOPREAL1:11; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A144: p1 in LSeg (p1,|[0,0]|) by RLTOPSP1:68;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then p1 in (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) by A144, XBOOLE_0:def 4;
then {p1} c= (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) by ZFMISC_1:31;
then A145: (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) = {p1} by A118, XBOOLE_0:def 10;
thus P1 \/ P2 = ((LSeg (|[0,0]|,p1)) \/ (LSeg (p1,p2))) \/ ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))) by XBOOLE_1:4
.= (((LSeg (|[0,0]|,p1)) \/ (LSeg (p1,p2))) \/ (LSeg (p2,|[1,0]|))) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:4
.= (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|)) by A3, A101, TOPREAL1:7
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A146: p2 in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then p2 in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) by A146, XBOOLE_0:def 4;
then {p2} c= (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) by ZFMISC_1:31;
then A147: (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,p2)) = {p2} by A128, XBOOLE_0:def 10;
A148: P1 /\ P2 = ((LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|))) \/ ((LSeg (p1,p2)) /\ ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2)))) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2}) by A145, A147, XBOOLE_1:23
.= {p1} \/ ((((LSeg (p1,p2)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((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,1]|,|[1,1]|)))) \/ ((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 A117, 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 ;

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

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

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

p1 in LSeg (p1,p2) by RLTOPSP1:68;
then A151: (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) <> {} by A150, Lm20, XBOOLE_0:def 4;
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, A101, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {p1} by A150, A151, TOPREAL1:17, ZFMISC_1:33;
hence P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by A148; :: thesis: verum

end;

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

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

assume |[0,0]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) ; :: thesis: contradiction
then |[0,0]| in LSeg (p1,p2) by XBOOLE_0:def 4;
then p1 `1 = 0 by A14, A16, A104, A109, Lm4, TOPREAL1:3;
hence contradiction by A14, A17, A152, EUCLID:53; :: thesis: verum

end;

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

end;

end;

end;

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

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

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

p2 in LSeg (p1,p2) by RLTOPSP1:68;
then A155: (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) <> {} by A154, Lm25, XBOOLE_0:def 4;
(LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {p2} by A3, A101, A154, TOPREAL1:6, TOPREAL1:16, XBOOLE_1:26;
then (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {p2} by A155, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A149, ENUMSET1:1; :: thesis: verum

end;

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

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

assume |[1,0]| in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; :: thesis: contradiction
then |[1,0]| in LSeg (p1,p2) by XBOOLE_0:def 4;
then |[1,0]| `1 <= p2 `1 by A14, A104, A109, TOPREAL1:3;
then p2 `1 = 1 by A104, A105, Lm8, XXREAL_0:1;
hence contradiction by A104, A107, A156, EUCLID:53; :: thesis: verum

end;

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

end;

end;

end;

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

end;

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

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

proof

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

end;

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

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

assume |[1,0]| in (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) ; :: thesis: contradiction
then A166: |[1,0]| in LSeg (|[0,0]|,p2) by XBOOLE_0:def 4;
|[0,0]| `1 <= p2 `1 by A104, A106, EUCLID:52;
then |[1,0]| `1 <= p2 `1 by A166, TOPREAL1:3;
hence contradiction by A15, A104, A105, A158, Lm8, XXREAL_0:1; :: thesis: verum

end;

then A167: {|[1,0]|} <> (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) by ZFMISC_1:31;
(LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A101, Lm21, TOPREAL1:6, XBOOLE_1:26;
then A168: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A167, TOPREAL1:16, ZFMISC_1:33;
A169: ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (LSeg (|[0,0]|,|[0,1]|)) = ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) by XBOOLE_1:23
.= {|[0,1]|} by Lm3, TOPREAL1:15 ;
(LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is_an_arc_of |[1,0]|,|[0,1]| by Lm9, Lm11, TOPREAL1:9, TOPREAL1:10, TOPREAL1:18;
then A170: ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|)) is_an_arc_of |[1,0]|,|[0,0]| by A169, TOPREAL1:10;

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

assume |[0,0]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) ; :: thesis: contradiction
then A171: |[0,0]| in LSeg (p1,|[1,0]|) by XBOOLE_0:def 4;
p1 `1 <= |[1,0]| `1 by A14, A15, EUCLID:52;
hence contradiction by A14, A106, A158, A171, Lm4, TOPREAL1:3; :: thesis: verum

end;

then A172: {|[0,0]|} <> (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, Lm24, TOPREAL1:6, XBOOLE_1:26;
then A173: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A172, TOPREAL1:17, ZFMISC_1:33;
|[0,0]| in LSeg (|[0,0]|,p2) by RLTOPSP1:68;
then A174: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) <> {} by Lm20, XBOOLE_0:def 4;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) c= {|[0,0]|} by A101, Lm21, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
then A175: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) = {|[0,0]|} by A174, ZFMISC_1:33;
A176: (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) c= {p1}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) or a in {p1} )
assume A177: a in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A178: p in LSeg (p1,|[1,0]|) by A177, XBOOLE_0:def 4;
p1 `1 <= |[1,0]| `1 by A14, A15, EUCLID:52;
then A179: p1 `1 <= p `1 by A178, TOPREAL1:3;
A180: p in LSeg (p2,p1) by A177, XBOOLE_0:def 4;
then p `1 <= p1 `1 by A14, A104, A158, TOPREAL1:3;
then A181: p1 `1 = p `1 by A179, XXREAL_0:1;
p2 `2 <= p `2 by A14, A17, A104, A107, A180, TOPREAL1:4;
then p `2 = 0 by A14, A17, A104, A107, A180, TOPREAL1:4;
then p = |[(p1 `1),0]| by A181, EUCLID:53
.= p1 by A14, A17, EUCLID:53 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

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

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

set a = the Element of (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2));
assume A184: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) <> {} ; :: thesis: contradiction
then reconsider p = the Element of (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) as Point of (TOP-REAL 2) by TARSKI:def 3;
A185: p in LSeg (p1,|[1,0]|) by A184, XBOOLE_0:def 4;
A186: p in LSeg (|[0,0]|,p2) by A184, XBOOLE_0:def 4;
|[0,0]| `1 <= p2 `1 by A104, A106, EUCLID:52;
then A187: p `1 <= p2 `1 by A186, TOPREAL1:3;
p1 `1 <= |[1,0]| `1 by A14, A15, EUCLID:52;
then p1 `1 <= p `1 by A185, TOPREAL1:3;
hence contradiction by A14, A104, A158, A187, XXREAL_0:2; :: thesis: verum

end;

take P1 = LSeg (p1,p2); :: thesis: ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[1,0]|)) \/ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A188: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A101, Lm21, TOPREAL1:6, XBOOLE_1:26;
then A189: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A188, XBOOLE_1:3;
A190: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {|[1,0]|} by A3, Lm24, TOPREAL1:6, TOPREAL1:16, XBOOLE_1:26;
(((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[0,0]|,p2)) = (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (LSeg (|[0,0]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))) by XBOOLE_1:23
.= (((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ {|[0,0]|} by A175, XBOOLE_1:23
.= {|[0,0]|} by A168, A189 ;
then A191: (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)) is_an_arc_of |[1,0]|,p2 by A170, TOPREAL1:10;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:9; :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A192: p2 in LSeg (|[0,0]|,p2) by RLTOPSP1:68;
(LSeg (p1,|[1,0]|)) /\ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))) = ((LSeg (p1,|[1,0]|)) /\ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[1,0]|)) /\ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) by A183, XBOOLE_1:23
.= ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) by A173, XBOOLE_1:23
.= {|[1,0]|} by A182, A190, A165, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A191, TOPREAL1:11; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A193: p1 in LSeg (p1,|[1,0]|) by RLTOPSP1:68;
thus P1 \/ P2 = ((LSeg (p2,p1)) \/ (LSeg (p1,|[1,0]|))) \/ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))) by XBOOLE_1:4
.= ((LSeg (|[0,0]|,p2)) \/ ((LSeg (p2,p1)) \/ (LSeg (p1,|[1,0]|)))) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) by XBOOLE_1:4
.= (LSeg (|[0,0]|,|[1,0]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) by A3, A101, TOPREAL1:7
.= (LSeg (|[0,0]|,|[1,0]|)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) by XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
then A194: (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A103, XBOOLE_1:3, XBOOLE_1:26;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then p2 in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,p2)) by A192, XBOOLE_0:def 4;
then {p2} c= (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,p2)) by ZFMISC_1:31;
then A195: (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,p2)) = {p2} by A159, XBOOLE_0:def 10;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then p1 in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) by A193, XBOOLE_0:def 4;
then {p1} c= (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (p1,|[1,0]|)) = {p1} by A176, XBOOLE_0:def 10;
then A196: P1 /\ P2 = {p1} \/ ((LSeg (p1,p2)) /\ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}) by A195, XBOOLE_1:23
.= {p1} \/ ((((LSeg (p1,p2)) /\ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((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,1]|,|[1,1]|)))) \/ ((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 A194, 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 ;

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

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

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

p2 in LSeg (p1,p2) by RLTOPSP1:68;
then A199: (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) <> {} by A198, Lm20, XBOOLE_0:def 4;
(LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, A101, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {p2} by A198, A199, TOPREAL1:17, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2} by A196; :: thesis: verum

end;

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

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

assume |[0,0]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) ; :: thesis: contradiction
then |[0,0]| in LSeg (p2,p1) by XBOOLE_0:def 4;
then p2 `1 = 0 by A14, A104, A106, A158, Lm4, TOPREAL1:3;
hence contradiction by A104, A107, A200, EUCLID:53; :: thesis: verum

end;

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

end;

end;

end;

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

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

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

p1 in LSeg (p1,p2) by RLTOPSP1:68;
then A203: (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) <> {} by A202, Lm25, XBOOLE_0:def 4;
(LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {p1} by A3, A101, A202, TOPREAL1:6, TOPREAL1:16, XBOOLE_1:26;
then (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {p1} by A203, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A197, ENUMSET1:1; :: thesis: verum

end;

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

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

assume |[1,0]| in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; :: thesis: contradiction
then |[1,0]| in LSeg (p2,p1) by XBOOLE_0:def 4;
then |[1,0]| `1 <= p1 `1 by A14, A104, A158, TOPREAL1:3;
then p1 `1 = 1 by A14, A15, Lm8, XXREAL_0:1;
hence contradiction by A14, A17, A204, EUCLID:53; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;

end;

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

end;

suppose A206: 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 A207: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) by TOPREAL1:13;

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

assume A208: |[1,0]| in (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) ; :: thesis: contradiction
then A209: |[1,0]| in LSeg (|[0,0]|,p1) by XBOOLE_0:def 4;
|[0,0]| `1 <= p1 `1 by A14, A16, EUCLID:52;
then |[1,0]| `1 <= p1 `1 by A209, TOPREAL1:3;
then 1 = p1 `1 by A14, A15, Lm8, XXREAL_0:1;
then A210: p1 = |[1,0]| by A14, A17, EUCLID:53;
A211: p2 `2 <= |[1,1]| `2 by A207, EUCLID:52;
|[1,0]| in LSeg (p2,|[1,1]|) by A208, XBOOLE_0:def 4;
then 0 = p2 `2 by A207, A211, Lm9, TOPREAL1:4;
hence contradiction by A1, A207, A210, EUCLID:53; :: thesis: verum

end;

then A212: {|[1,0]|} <> (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) by ZFMISC_1:31;
A213: LSeg (|[0,1]|,|[1,1]|) is_an_arc_of |[0,1]|,|[1,1]| by Lm6, Lm10, TOPREAL1:9;
LSeg (|[0,0]|,|[0,1]|) is_an_arc_of |[0,0]|,|[0,1]| by Lm5, Lm7, TOPREAL1:9;
then A214: (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) is_an_arc_of |[0,0]|,|[1,1]| by A213, TOPREAL1:2, TOPREAL1:15;
take P1 = (LSeg (p1,|[1,0]|)) \/ (LSeg (|[1,0]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A215: LSeg (|[0,0]|,|[1,0]|) = (LSeg (p1,|[1,0]|)) \/ (LSeg (p1,|[0,0]|)) by A3, TOPREAL1:5;
|[1,1]| in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
then A216: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) <> {} by Lm26, XBOOLE_0:def 4;
A217: |[1,0]| in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
|[1,0]| in LSeg (p1,|[1,0]|) by RLTOPSP1:68;
then A218: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) <> {} by A217, XBOOLE_0:def 4;
A219: LSeg (p2,|[1,0]|) c= LSeg (|[1,0]|,|[1,1]|) by A206, Lm25, TOPREAL1:6;
then (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A12, XBOOLE_1:27;
then A220: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) = {|[1,0]|} by A218, TOPREAL1:16, ZFMISC_1:33;
( p1 <> |[1,0]| or p2 <> |[1,0]| ) by A1;
hence P1 is_an_arc_of p1,p2 by A220, TOPREAL1:12; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A221: (LSeg (p1,|[1,0]|)) /\ (LSeg (p1,|[0,0]|)) = {p1} by A3, TOPREAL1:8;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by TOPREAL1:20, XBOOLE_0:def 7;
then A222: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A219, XBOOLE_1:3, XBOOLE_1:26;
A223: LSeg (p2,|[1,1]|) c= LSeg (|[1,0]|,|[1,1]|) by A206, Lm27, TOPREAL1:6;
then A224: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[1,1]|} by TOPREAL1:18, XBOOLE_1:27;
A225: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A223, Lm3, XBOOLE_1:3, XBOOLE_1:26;
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) /\ (LSeg (|[1,1]|,p2)) = ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= {|[1,1]|} by A225, A224, A216, ZFMISC_1:33 ;
then A226: ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)) is_an_arc_of |[0,0]|,p2 by A214, TOPREAL1:10;
A227: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[1,1]|,p2)) = {p2} by A206, TOPREAL1:8;
A228: LSeg (|[1,0]|,|[1,1]|) = (LSeg (|[1,1]|,p2)) \/ (LSeg (|[1,0]|,p2)) by A206, TOPREAL1:5;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[1,0]|} by A10, A223, TOPREAL1:16, XBOOLE_1:27;
then A229: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A212, ZFMISC_1:33;
(LSeg (p1,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) = ((LSeg (p1,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) by A229, XBOOLE_1:23
.= {|[0,0]|} by A8, A6, A11, TOPREAL1:17, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A226, TOPREAL1:11; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg (|[1,0]|,p2)) \/ ((LSeg (p1,|[1,0]|)) \/ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:4
.= (LSeg (|[1,0]|,p2)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by A215, XBOOLE_1:4
.= ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,1]|,p2))) \/ (LSeg (|[1,0]|,p2)) by XBOOLE_1:4
.= (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|)) by A228, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A230: P1 /\ P2 = ((LSeg (p1,|[1,0]|)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:23
.= (((LSeg (p1,|[1,0]|)) /\ (LSeg (p1,|[0,0]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by A221, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (|[1,0]|,p1)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by A13, XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ (((LSeg (|[1,0]|,p2)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2})) by A227, XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ ((((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})) by A222 ;

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

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

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

then A233: (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|)) = (LSeg (|[1,0]|,p2)) /\ {|[0,0]|} by RLTOPSP1:70;
not |[0,0]| in LSeg (|[1,0]|,p2) by A219, Lm4, Lm8, Lm10, TOPREAL1:3;
then (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|)) = {} by A233, Lm1;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by A230, A232, TOPREAL1:17, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) ;
:: thesis: verum

end;

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

A235: p1 in LSeg (p1,|[0,0]|) by RLTOPSP1:68;
p1 in LSeg (|[1,0]|,p2) by A234, RLTOPSP1:68;
then A236: {} <> (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|)) by A235, XBOOLE_0:def 4;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {|[1,0]|} /\ (LSeg (|[0,0]|,|[0,1]|)) by A234, RLTOPSP1:70;
then A237: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by Lm1, Lm16;
(LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A10, A219, XBOOLE_1:27;
then (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|)) = {p1} by A234, A236, TOPREAL1:16, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by A230, A237, XBOOLE_1:4
.= (({p1} \/ {p1}) \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) ;
:: thesis: verum

end;

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

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

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

end;

then A240: {|[1,0]|} <> (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|)) by ZFMISC_1:31;
(LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A10, A219, XBOOLE_1:27;
then A241: (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,0]|)) = {} by A240, TOPREAL1:16, ZFMISC_1:33;

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

assume |[0,0]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) ; :: thesis: contradiction
then A242: |[0,0]| in LSeg (p1,|[1,0]|) by XBOOLE_0:def 4;
p1 `1 <= |[1,0]| `1 by A14, A15, EUCLID:52;
then p1 `1 = 0 by A14, A16, A242, Lm4, TOPREAL1:3;
hence contradiction by A14, A17, A238, EUCLID:53; :: thesis: verum

end;

then A243: {|[0,0]|} <> (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, Lm24, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (p1,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A243, TOPREAL1:17, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by A230, A241; :: thesis: verum

end;

end;

end;

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

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

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

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

end;

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

then A248: (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) = (LSeg (p1,|[1,0]|)) /\ {|[1,1]|} by RLTOPSP1:70;
not |[1,1]| in LSeg (p1,|[1,0]|) by A12, Lm5, Lm9, Lm11, TOPREAL1:4;
then (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A248, Lm1;
hence P1 /\ P2 = {p1,p2} by A231, A247, ENUMSET1:1, TOPREAL1:18; :: thesis: verum

end;

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

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

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

end;

then A251: {|[1,1]|} <> (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) by ZFMISC_1:31;
(LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A206, Lm25, TOPREAL1:6, XBOOLE_1:26;
then A252: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A251, TOPREAL1:18, ZFMISC_1:33;

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

assume |[1,0]| in (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) ; :: thesis: contradiction
then A253: |[1,0]| in LSeg (p2,|[1,1]|) by XBOOLE_0:def 4;
p2 `2 <= |[1,1]| `2 by A207, EUCLID:52;
then p2 `2 = 0 by A207, A253, Lm9, TOPREAL1:4;
hence contradiction by A207, A249, EUCLID:53; :: thesis: verum

end;

then A254: {|[1,0]|} <> (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) by ZFMISC_1:31;
(LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[1,0]|} by A12, A223, TOPREAL1:16, XBOOLE_1:27;
then (LSeg (p1,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A254, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A231, A252, ENUMSET1:1; :: thesis: verum

end;

end;

end;

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

end;

end;