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

suppose A19: 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 A20: LSeg (p2,p1) c= LSeg (|[0,0]|,|[0,1]|) by A3, TOPREAL1:6;
A21: p = |[(p `1),(p `2)]| by EUCLID:53;
consider q being Point of (TOP-REAL 2) such that
A22: q = p2 and
A23: q `1 = 0 and
A24: q `2 <= 1 and
A25: q `2 >= 0 by A19, TOPREAL1:13;
A26: q = |[(q `1),(q `2)]| by EUCLID:53;

now :: thesis: ( ( p `2 < q `2 & LSeg (p1,p2) is_an_arc_of p1,p2 & (LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) is_an_arc_of p1,p2 & R^2-unit_square = (LSeg (p1,p2)) \/ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) & (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1,p2} ) or ( p `2 > q `2 & 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 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) ) )

per cases ( p `2 < q `2 or p `2 > q `2 ) by A1, A15, A16, A22, A23, A21, A26, XXREAL_0:1;

case A27: p `2 < q `2 ; :: thesis: ( LSeg (p1,p2) is_an_arc_of p1,p2 & (LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) is_an_arc_of p1,p2 & R^2-unit_square = (LSeg (p1,p2)) \/ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) & (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1,p2} )

A28: (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 A29: a in (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A30: p in LSeg (|[0,0]|,p1) by A29, XBOOLE_0:def 4;
|[0,0]| `2 <= p1 `2 by A15, A18, EUCLID:52;
then A31: p `2 <= p1 `2 by A30, TOPREAL1:4;
A32: p in LSeg (p1,p2) by A29, XBOOLE_0:def 4;
then p1 `2 <= p `2 by A15, A22, A27, TOPREAL1:4;
then A33: p1 `2 = p `2 by A31, XXREAL_0:1;
p1 `1 <= p `1 by A15, A16, A22, A23, A32, TOPREAL1:3;
then p `1 = 0 by A15, A16, A22, A23, A32, TOPREAL1:3;
then p = |[0,(p1 `2)]| by A33, EUCLID:53
.= p1 by A15, A16, EUCLID:53 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

A34: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A19, Lm22, TOPREAL1:6, XBOOLE_1:26;

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

set a = the Element of (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2));
assume A36: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) <> {} ; :: thesis: contradiction
then reconsider p = the Element of (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2)) as Point of (TOP-REAL 2) by TARSKI:def 3;
A37: p in LSeg (|[0,0]|,p1) by A36, XBOOLE_0:def 4;
A38: p in LSeg (p2,|[0,1]|) by A36, XBOOLE_0:def 4;
p2 `2 <= |[0,1]| `2 by A22, A24, EUCLID:52;
then A39: p2 `2 <= p `2 by A38, TOPREAL1:4;
|[0,0]| `2 <= p1 `2 by A15, A18, EUCLID:52;
then p `2 <= p1 `2 by A37, TOPREAL1:4;
hence contradiction by A15, A22, A27, A39, XXREAL_0:2; :: thesis: verum

end;

|[0,1]| in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
then |[0,1]| in (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) by Lm23, XBOOLE_0:def 4;
then A40: {|[0,1]|} c= (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) by ZFMISC_1:31;

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

assume |[0,0]| in (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) ; :: thesis: contradiction
then A41: |[0,0]| in LSeg (p2,|[0,1]|) by XBOOLE_0:def 4;
p2 `2 <= |[0,1]| `2 by A22, A24, EUCLID:52;
hence contradiction by A18, A22, A27, A41, Lm5, TOPREAL1:4; :: thesis: verum

end;

then A42: {|[0,0]|} <> (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) by ZFMISC_1:31;
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= {|[0,0]|} by A19, Lm22, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
then A43: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A42, ZFMISC_1:33;
A44: (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= {|[0,0]|} by A3, A19, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
A45: (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)) c= {p2}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)) or a in {p2} )
assume A46: a in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A47: p in LSeg (p2,|[0,1]|) by A46, XBOOLE_0:def 4;
p2 `2 <= |[0,1]| `2 by A22, A24, EUCLID:52;
then A48: p2 `2 <= p `2 by A47, TOPREAL1:4;
A49: p in LSeg (p1,p2) by A46, XBOOLE_0:def 4;
then p `2 <= p2 `2 by A15, A22, A27, TOPREAL1:4;
then A50: p2 `2 = p `2 by A48, XXREAL_0:1;
p1 `1 <= p `1 by A15, A16, A22, A23, A49, TOPREAL1:3;
then p `1 = 0 by A15, A16, A22, A23, A49, TOPREAL1:3;
then p = |[0,(p2 `2)]| by A50, EUCLID:53
.= p2 by A22, A23, EUCLID:53 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

A51: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= {|[0,1]|} by A3, Lm20, TOPREAL1:6, TOPREAL1:15, XBOOLE_1:26;

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

assume |[0,1]| in (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; :: thesis: contradiction
then A52: |[0,1]| in LSeg (|[0,0]|,p1) by XBOOLE_0:def 4;
|[0,0]| `2 <= p1 `2 by A15, A18, EUCLID:52;
then |[0,1]| `2 <= p1 `2 by A52, TOPREAL1:4;
hence contradiction by A15, A17, A24, A27, Lm7, XXREAL_0:1; :: thesis: verum

end;

then A53: {|[0,1]|} <> (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by ZFMISC_1:31;
set P1 = LSeg (p1,p2);
set P2 = (LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)));
A54: p1 in LSeg (p1,|[0,0]|) by RLTOPSP1:68;
A55: LSeg (|[0,1]|,p2) c= LSeg (|[0,0]|,|[0,1]|) by A19, Lm22, TOPREAL1:6;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then p1 in (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) by A54, XBOOLE_0:def 4;
then {p1} c= (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) by ZFMISC_1:31;
then A56: (LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|)) = {p1} by A28, XBOOLE_0:def 10;
thus LSeg (p1,p2) is_an_arc_of p1,p2 by A1, TOPREAL1:9; :: thesis: ( (LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) is_an_arc_of p1,p2 & R^2-unit_square = (LSeg (p1,p2)) \/ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) & (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1,p2} )
A57: ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) /\ (LSeg (|[1,1]|,|[0,1]|)) = {} \/ {|[1,1]|} by Lm2, TOPREAL1:18, XBOOLE_1:23
.= {|[1,1]|} ;
(LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) is_an_arc_of |[0,0]|,|[1,1]| by Lm4, Lm8, TOPREAL1:12, TOPREAL1:16;
then A58: ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)) is_an_arc_of |[0,0]|,|[0,1]| by A57, TOPREAL1:10;
(((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) /\ (LSeg (|[0,1]|,p2)) = ((LSeg (|[0,1]|,p2)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,1]|,|[0,1]|))) by XBOOLE_1:23
.= ({} \/ ((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,1]|,|[0,1]|))) by A43, XBOOLE_1:23
.= {} \/ ((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,1]|,|[0,1]|))) by A55, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= {|[0,1]|} by A40, A34, TOPREAL1:15, XBOOLE_0:def 10 ;
then A59: (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)) is_an_arc_of |[0,0]|,p2 by A58, TOPREAL1:10;
(LSeg (p1,|[0,0]|)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) = ((LSeg (p1,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= (((LSeg (p1,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= ((((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= {|[0,0]|} by A9, A7, A35, A51, A53, ZFMISC_1:33 ;
hence (LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) is_an_arc_of p1,p2 by A59, TOPREAL1:11; :: thesis: ( R^2-unit_square = (LSeg (p1,p2)) \/ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) & (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1,p2} )
((LSeg (|[0,1]|,p2)) \/ (LSeg (p2,p1))) \/ (LSeg (p1,|[0,0]|)) = LSeg (|[0,0]|,|[0,1]|) by A3, A19, TOPREAL1:7;
hence R^2-unit_square = (((LSeg (p1,p2)) \/ (LSeg (|[0,1]|,p2))) \/ (LSeg (p1,|[0,0]|))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) by TOPREAL1:def 2, XBOOLE_1:4
.= ((LSeg (p1,p2)) \/ ((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,1]|,p2)))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) by XBOOLE_1:4
.= (LSeg (p1,p2)) \/ (((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,1]|,p2))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) by XBOOLE_1:4
.= (LSeg (p1,p2)) \/ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) by XBOOLE_1:4 ;
:: thesis: (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1,p2}
A60: p2 in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then p2 in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)) by A60, XBOOLE_0:def 4;
then {p2} c= (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)) by ZFMISC_1:31;
then A61: (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)) = {p2} by A45, XBOOLE_0:def 10;
A62: LSeg (p1,p2) c= LSeg (|[0,0]|,|[0,1]|) by A3, A19, TOPREAL1:6;
A63: (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = ((LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|))) \/ ((LSeg (p1,p2)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) by XBOOLE_1:23
.= ((LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|))) \/ (((LSeg (p1,p2)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)))) by XBOOLE_1:23
.= ((LSeg (p1,p2)) /\ (LSeg (p1,|[0,0]|))) \/ ((((LSeg (p1,p2)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)))) by XBOOLE_1:23
.= {p1} \/ (((((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)))) by A56, XBOOLE_1:23
.= {p1} \/ (((((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)))) by A62, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2})) by A61, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:4 ;

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

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

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

then |[0,0]| in LSeg (p1,p2) by RLTOPSP1:68;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) <> {} by Lm21, XBOOLE_0:def 4;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {p1} by A44, A65, ZFMISC_1:33;
hence (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by A63; :: thesis: verum

end;

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

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

assume |[0,0]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) ; :: thesis: contradiction
then |[0,0]| in LSeg (p1,p2) by XBOOLE_0:def 4;
then p1 `2 <= |[0,0]| `2 by A15, A22, A27, TOPREAL1:4;
then |[0,0]| `2 = p1 `2 by A3, Lm5, Lm7, TOPREAL1:4;
hence contradiction by A15, A16, A66, Lm5, EUCLID:53; :: thesis: verum

end;

then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) <> {|[0,0]|} by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A44, ZFMISC_1:33;
hence (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by A63; :: thesis: verum

end;

end;

end;

A67: (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= {|[0,1]|} by A3, A19, TOPREAL1:6, TOPREAL1:15, XBOOLE_1:26;

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

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

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

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

assume |[0,1]| in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; :: thesis: contradiction
then |[0,1]| in LSeg (p1,p2) by XBOOLE_0:def 4;
then A69: |[0,1]| `2 <= p2 `2 by A15, A22, A27, TOPREAL1:4;
p2 `2 <= |[0,1]| `2 by A19, Lm5, Lm7, TOPREAL1:4;
then A70: |[0,1]| `2 = p2 `2 by A69, XXREAL_0:1;
p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53
.= |[0,1]| by A22, A23, A70, EUCLID:52 ;
hence contradiction by A68; :: thesis: verum

end;

then (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) <> {|[0,1]|} by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A67, ZFMISC_1:33;
hence (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1,p2} by A64, ENUMSET1:1; :: thesis: verum

end;

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

then |[0,1]| in LSeg (p1,p2) by RLTOPSP1:68;
then (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) <> {} by Lm23, XBOOLE_0:def 4;
then (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {p2} by A67, A71, ZFMISC_1:33;
hence (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1,p2} by A64, ENUMSET1:1; :: thesis: verum

end;

end;

end;

hence (LSeg (p1,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) = {p1,p2} ; :: thesis: verum

end;

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

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p2,p1)) /\ (LSeg (|[0,1]|,p1)) or a in {p1} )
assume A74: a in (LSeg (p2,p1)) /\ (LSeg (|[0,1]|,p1)) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A75: p in LSeg (p1,|[0,1]|) by A74, XBOOLE_0:def 4;
p1 `2 <= |[0,1]| `2 by A15, A17, EUCLID:52;
then A76: p1 `2 <= p `2 by A75, TOPREAL1:4;
A77: p in LSeg (p2,p1) by A74, XBOOLE_0:def 4;
then p `2 <= p1 `2 by A15, A22, A72, TOPREAL1:4;
then A78: p1 `2 = p `2 by A76, XXREAL_0:1;
p2 `1 <= p `1 by A15, A16, A22, A23, A77, TOPREAL1:3;
then p `1 = 0 by A15, A16, A22, A23, A77, TOPREAL1:3;
then p = |[0,(p1 `2)]| by A78, EUCLID:53
.= p1 by A15, A16, EUCLID:53 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

A79: LSeg (p2,|[0,0]|) c= LSeg (|[0,0]|,|[0,1]|) by A19, Lm20, TOPREAL1:6;

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

set a = the Element of (LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,p1));
assume A81: (LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,p1)) <> {} ; :: thesis: contradiction
then reconsider p = the Element of (LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,p1)) as Point of (TOP-REAL 2) by TARSKI:def 3;
A82: p in LSeg (|[0,0]|,p2) by A81, XBOOLE_0:def 4;
A83: p in LSeg (p1,|[0,1]|) by A81, XBOOLE_0:def 4;
p1 `2 <= |[0,1]| `2 by A15, A17, EUCLID:52;
then A84: p1 `2 <= p `2 by A83, TOPREAL1:4;
|[0,0]| `2 <= p2 `2 by A22, A25, EUCLID:52;
then p `2 <= p2 `2 by A82, TOPREAL1:4;
hence contradiction by A15, A22, A72, A84, XXREAL_0:2; :: thesis: verum

end;

A85: (LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= {|[0,0]|} by A3, A19, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;

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

assume |[0,1]| in (LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; :: thesis: contradiction
then A86: |[0,1]| in LSeg (|[0,0]|,p2) by XBOOLE_0:def 4;
|[0,0]| `2 <= p2 `2 by A22, A25, EUCLID:52;
then |[0,1]| `2 <= p2 `2 by A86, TOPREAL1:4;
hence contradiction by A17, A22, A24, A72, Lm7, XXREAL_0:1; :: thesis: verum

end;

then A87: {|[0,1]|} <> (LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by ZFMISC_1:31;
A88: (LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= {|[0,0]|} by A19, Lm20, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;

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

assume |[0,0]| in (LSeg (|[0,1]|,p1)) /\ (LSeg (|[0,0]|,|[1,0]|)) ; :: thesis: contradiction
then A89: |[0,0]| in LSeg (p1,|[0,1]|) by XBOOLE_0:def 4;
p1 `2 <= |[0,1]| `2 by A15, A17, EUCLID:52;
hence contradiction by A15, A25, A72, A89, Lm5, TOPREAL1:4; :: thesis: verum

end;

then A90: {|[0,0]|} <> (LSeg (|[0,1]|,p1)) /\ (LSeg (|[0,0]|,|[1,0]|)) by ZFMISC_1:31;
A91: (LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= {|[0,1]|} by A19, Lm20, TOPREAL1:6, TOPREAL1:15, XBOOLE_1:26;
A92: (LSeg (p2,p1)) /\ (LSeg (p2,|[0,0]|)) c= {p2}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p2,p1)) /\ (LSeg (p2,|[0,0]|)) or a in {p2} )
assume A93: a in (LSeg (p2,p1)) /\ (LSeg (p2,|[0,0]|)) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A94: p in LSeg (|[0,0]|,p2) by A93, XBOOLE_0:def 4;
|[0,0]| `2 <= p2 `2 by A22, A25, EUCLID:52;
then A95: p `2 <= p2 `2 by A94, TOPREAL1:4;
A96: p in LSeg (p2,p1) by A93, XBOOLE_0:def 4;
then p2 `2 <= p `2 by A15, A22, A72, TOPREAL1:4;
then A97: p2 `2 = p `2 by A95, XXREAL_0:1;
p2 `1 <= p `1 by A15, A16, A22, A23, A96, TOPREAL1:3;
then p `1 = 0 by A15, A16, A22, A23, A96, TOPREAL1:3;
then p = |[0,(p2 `2)]| by A97, EUCLID:53
.= p2 by A22, A23, EUCLID:53 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

A98: (LSeg (|[0,1]|,p1)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= {|[0,0]|} by A3, Lm22, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
take P1 = LSeg (p2,p1); :: 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 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p2,|[0,0]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p1))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A99: p2 in LSeg (p2,|[0,0]|) by RLTOPSP1:68;
p2 in LSeg (p2,p1) by RLTOPSP1:68;
then p2 in (LSeg (p2,p1)) /\ (LSeg (p2,|[0,0]|)) by A99, XBOOLE_0:def 4;
then A100: {p2} c= (LSeg (p2,p1)) /\ (LSeg (p2,|[0,0]|)) by ZFMISC_1:31;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:9; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A101: (LSeg (|[0,1]|,|[1,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) = {} \/ {|[1,1]|} by Lm2, TOPREAL1:18, XBOOLE_1:23
.= {|[1,1]|} ;
(LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) is_an_arc_of |[1,1]|,|[0,0]| by Lm4, Lm8, TOPREAL1:12, TOPREAL1:16;
then A102: ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)) is_an_arc_of |[0,1]|,|[0,0]| by A101, TOPREAL1:11;
|[0,0]| in LSeg (p2,|[0,0]|) by RLTOPSP1:68;
then |[0,0]| in (LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by Lm21, XBOOLE_0:def 4;
then A103: {|[0,0]|} c= (LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by ZFMISC_1:31;
(LSeg (p1,|[0,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) = ((LSeg (|[0,1]|,p1)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,p1)) /\ (LSeg (|[1,1]|,|[0,1]|))) by XBOOLE_1:23
.= (((LSeg (|[0,1]|,p1)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[0,1]|,p1)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,p1)) /\ (LSeg (|[1,1]|,|[0,1]|))) by XBOOLE_1:23
.= ({} \/ ((LSeg (|[0,1]|,p1)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[0,1]|,p1)) /\ (LSeg (|[1,1]|,|[0,1]|))) by A98, A90, ZFMISC_1:33
.= {|[0,1]|} by A14, A10, A12, XBOOLE_0:def 10 ;
then A104: (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p1)) is_an_arc_of p1,|[0,0]| by A102, TOPREAL1:11;
((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p1))) /\ (LSeg (|[0,0]|,p2)) = ((LSeg (p2,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,p1))) by XBOOLE_1:23
.= (((LSeg (p2,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p2,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,p1))) by XBOOLE_1:23
.= ((((LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p2,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p2,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,p1))) by XBOOLE_1:23
.= ((((LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (p2,|[0,0]|)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,1]|,p1))) by A79, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= ((LSeg (p2,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {} by A80, A91, A87, ZFMISC_1:33
.= {|[0,0]|} by A103, A88, XBOOLE_0:def 10 ;
hence P2 is_an_arc_of p1,p2 by A104, TOPREAL1:10; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
((LSeg (|[0,1]|,p1)) \/ (LSeg (p1,p2))) \/ (LSeg (p2,|[0,0]|)) = LSeg (|[0,0]|,|[0,1]|) by A3, A19, TOPREAL1:7;
hence R^2-unit_square = (((LSeg (p2,p1)) \/ (LSeg (|[0,1]|,p1))) \/ (LSeg (p2,|[0,0]|))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) by TOPREAL1:def 2, XBOOLE_1:4
.= ((LSeg (p2,p1)) \/ ((LSeg (p2,|[0,0]|)) \/ (LSeg (|[0,1]|,p1)))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) by XBOOLE_1:4
.= (LSeg (p2,p1)) \/ (((LSeg (p2,|[0,0]|)) \/ (LSeg (|[0,1]|,p1))) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4 ;
:: thesis: P1 /\ P2 = {p1,p2}
A105: p1 in LSeg (|[0,1]|,p1) by RLTOPSP1:68;
p1 in LSeg (p2,p1) by RLTOPSP1:68;
then p1 in (LSeg (p2,p1)) /\ (LSeg (|[0,1]|,p1)) by A105, XBOOLE_0:def 4;
then A106: {p1} c= (LSeg (p2,p1)) /\ (LSeg (|[0,1]|,p1)) by ZFMISC_1:31;
A107: P1 /\ P2 = ((LSeg (p2,p1)) /\ (LSeg (p2,|[0,0]|))) \/ ((LSeg (p2,p1)) /\ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p1)))) by XBOOLE_1:23
.= ((LSeg (p2,p1)) /\ (LSeg (p2,|[0,0]|))) \/ (((LSeg (p2,p1)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[0,1]|,p1)))) by XBOOLE_1:23
.= ((LSeg (p2,p1)) /\ (LSeg (p2,|[0,0]|))) \/ ((((LSeg (p2,p1)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[0,1]|,p1)))) by XBOOLE_1:23
.= ((LSeg (p2,p1)) /\ (LSeg (p2,|[0,0]|))) \/ (((((LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[0,1]|,p1)))) by XBOOLE_1:23
.= {p2} \/ (((((LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[0,1]|,p1)))) by A100, A92, XBOOLE_0:def 10
.= {p2} \/ (((((LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {}) \/ ((LSeg (p2,p1)) /\ (LSeg (|[1,1]|,|[0,1]|)))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[0,1]|,p1)))) by A20, Lm3, XBOOLE_1:3, XBOOLE_1:26
.= {p2} \/ ((((LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p2,p1)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p1}) by A106, A73, XBOOLE_0:def 10
.= {p2} \/ (((LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (p2,p1)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p1})) by XBOOLE_1:4
.= ({p2} \/ ((LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (p2,p1)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p1}) by XBOOLE_1:4 ;

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

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

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

p2 in LSeg (p2,p1) by RLTOPSP1:68;
then (LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|)) <> {} by A109, Lm21, XBOOLE_0:def 4;
then (LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {p2} by A85, A109, ZFMISC_1:33;
hence P1 /\ P2 = {p2} \/ (((LSeg (p2,p1)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p1}) by A107; :: thesis: verum

end;

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

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

assume |[0,0]| in (LSeg (p2,p1)) /\ (LSeg (|[0,0]|,|[1,0]|)) ; :: thesis: contradiction
then |[0,0]| in LSeg (p2,p1) by XBOOLE_0:def 4;
then p2 `2 <= |[0,0]| `2 by A15, A22, A72, TOPREAL1:4;
then |[0,0]| `2 = p2 `2 by A19, Lm5, Lm7, TOPREAL1:4;
hence contradiction by A22, A23, A110, Lm5, EUCLID:53; :: thesis: verum

end;

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

end;

end;

end;

A111: (LSeg (p2,p1)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= {|[0,1]|} by A3, A19, TOPREAL1:6, TOPREAL1:15, XBOOLE_1:26;

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

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

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

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

assume |[0,1]| in (LSeg (p2,p1)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; :: thesis: contradiction
then |[0,1]| in LSeg (p2,p1) by XBOOLE_0:def 4;
then A113: |[0,1]| `2 <= p1 `2 by A15, A22, A72, TOPREAL1:4;
p1 `2 <= |[0,1]| `2 by A3, Lm5, Lm7, TOPREAL1:4;
then A114: |[0,1]| `2 = p1 `2 by A113, XXREAL_0:1;
p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53
.= |[0,1]| by A15, A16, A114, EUCLID:52 ;
hence contradiction by A112; :: thesis: verum

end;

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

end;

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

then |[0,1]| in LSeg (p2,p1) by RLTOPSP1:68;
then (LSeg (p2,p1)) /\ (LSeg (|[0,1]|,|[1,1]|)) <> {} by Lm23, XBOOLE_0:def 4;
then (LSeg (p2,p1)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {p1} by A111, A115, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A108, 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 A116: 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 A117: LSeg (|[0,1]|,p2) c= LSeg (|[0,1]|,|[1,1]|) by Lm23, TOPREAL1:6;
LSeg (p1,|[0,1]|) c= LSeg (|[0,0]|,|[0,1]|) by A3, Lm22, TOPREAL1:6;
then A118: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A117, XBOOLE_1:27;
take P1 = (LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A119: |[0,1]| in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
|[1,1]| in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
then A120: |[1,1]| in (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) by Lm27, XBOOLE_0:def 4;
|[0,1]| in LSeg (p1,|[0,1]|) by RLTOPSP1:68;
then (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) <> {} by A119, XBOOLE_0:def 4;
then A121: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) = {|[0,1]|} by A118, TOPREAL1:15, ZFMISC_1:33;
( p1 <> |[0,1]| or p2 <> |[0,1]| ) by A1;
hence P1 is_an_arc_of p1,p2 by A121, TOPREAL1:12; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A122: LSeg (|[0,0]|,|[0,1]|) = (LSeg (p1,|[0,1]|)) \/ (LSeg (p1,|[0,0]|)) by A3, TOPREAL1:5;
A123: LSeg (|[1,0]|,|[1,1]|) is_an_arc_of |[1,0]|,|[1,1]| by Lm9, Lm11, TOPREAL1:9;
LSeg (|[0,0]|,|[1,0]|) is_an_arc_of |[0,0]|,|[1,0]| by Lm4, Lm8, TOPREAL1:9;
then A124: (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) is_an_arc_of |[0,0]|,|[1,1]| by A123, TOPREAL1:2, TOPREAL1:16;
A125: LSeg (|[1,1]|,p2) c= LSeg (|[0,1]|,|[1,1]|) by A116, Lm26, TOPREAL1:6;
then A126: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by XBOOLE_1:27;
A127: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A125, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) /\ (LSeg (|[1,1]|,p2)) = ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= {|[1,1]|} by A127, A126, A120, TOPREAL1:18, ZFMISC_1:33 ;
then A128: ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)) is_an_arc_of |[0,0]|,p2 by A124, TOPREAL1:10;
A129: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,1]|,p2)) = {p2} by A116, TOPREAL1:8;
A130: LSeg (|[0,1]|,|[1,1]|) = (LSeg (|[1,1]|,p2)) \/ (LSeg (|[0,1]|,p2)) by A116, TOPREAL1:5;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[0,1]|} by A4, A125, TOPREAL1:15, XBOOLE_1:27;
then A131: ( (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) = {|[0,1]|} or (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) = {} ) by ZFMISC_1:33;
A132: LSeg (|[0,1]|,p2) c= LSeg (|[0,1]|,|[1,1]|) by A116, Lm23, TOPREAL1:6;
then A133: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by Lm2, XBOOLE_1:3, XBOOLE_1:27;
A134: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 1 ) by A116, TOPREAL1:13;

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

A136: p2 `1 <= |[1,1]| `1 by A134, EUCLID:52;
assume A137: |[0,1]| in (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) ; :: thesis: contradiction
then A138: |[0,1]| in LSeg (|[0,0]|,p1) by XBOOLE_0:def 4;
|[0,1]| in LSeg (p2,|[1,1]|) by A137, XBOOLE_0:def 4;
then A139: |[0,1]| `1 = p2 `1 by A134, A136, Lm6, TOPREAL1:3;
|[0,0]| `2 <= p1 `2 by A15, A18, EUCLID:52;
then |[0,1]| `2 <= p1 `2 by A138, TOPREAL1:4;
then |[0,1]| `2 = p1 `2 by A15, A17, Lm7, XXREAL_0:1;
then p1 = |[(|[0,1]| `1),(|[0,1]| `2)]| by A15, A16, Lm6, EUCLID:53
.= p2 by A134, A139, Lm7, EUCLID:53 ;
hence contradiction by A1; :: thesis: verum

end;

(LSeg (p1,|[0,0]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) = ((LSeg (p1,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) by A131, A135, XBOOLE_1:23, ZFMISC_1:31
.= {|[0,0]|} by A9, A5, A6, TOPREAL1:17, XBOOLE_0:def 10 ;
hence P2 is_an_arc_of p1,p2 by A128, TOPREAL1:11; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg (|[0,1]|,p2)) \/ ((LSeg (p1,|[0,1]|)) \/ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:4
.= ((LSeg (|[0,0]|,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) \/ (LSeg (|[0,1]|,p2)) by A122, XBOOLE_1:4
.= (LSeg (|[0,0]|,|[0,1]|)) \/ ((((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) \/ (LSeg (|[0,1]|,p2))) by XBOOLE_1:4
.= (LSeg (|[0,0]|,|[0,1]|)) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) by A130, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A140: {p1} = (LSeg (p1,|[0,1]|)) /\ (LSeg (p1,|[0,0]|)) by A3, TOPREAL1:8;
A141: P1 /\ P2 = ((LSeg (p1,|[0,1]|)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:23
.= (((LSeg (p1,|[0,1]|)) /\ (LSeg (p1,|[0,0]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by A140, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[0,0]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ ((LSeg (|[0,1]|,p2)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ (((LSeg (|[0,1]|,p2)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2})) by A129, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ ((((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2})) by A14, A133 ;

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

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

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

then A144: not p2 in LSeg (p1,|[0,1]|) by A13, Lm4, Lm6, Lm10, TOPREAL1:3;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = (LSeg (p1,|[0,1]|)) /\ {p2} by A143, RLTOPSP1:70
.= {} by A144, Lm1 ;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ {p2}) by A141, A143, TOPREAL1:18; :: thesis: verum

end;

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

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

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

end;

then A147: {|[0,1]|} <> (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) by ZFMISC_1:31;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[0,1]|} by A13, A125, TOPREAL1:15, XBOOLE_1:27;
then A148: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A147, ZFMISC_1:33;

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 A149: |[1,1]| in LSeg (|[0,1]|,p2) by XBOOLE_0:def 4;
|[0,1]| `1 <= p2 `1 by A134, EUCLID:52;
then |[1,1]| `1 <= p2 `1 by A149, TOPREAL1:3;
then p2 `1 = |[1,1]| `1 by A134, Lm10, XXREAL_0:1;
hence contradiction by A134, A145, Lm10, EUCLID:53; :: thesis: verum

end;

then A150: {|[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 A132, TOPREAL1:18, XBOOLE_1:27;
then (LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by A150, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ {p2}) by A141, A148; :: thesis: verum

end;

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

then p2 in LSeg (p1,|[0,1]|) by RLTOPSP1:68;
then A152: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) <> {} by A151, Lm23, XBOOLE_0:def 4;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) c= {p2} by A13, A151, TOPREAL1:15, XBOOLE_1:27;
then A153: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = {p2} by A152, ZFMISC_1:33;
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[0,1]|} /\ (LSeg (|[1,0]|,|[1,1]|)) by A151, RLTOPSP1:70
.= {} by Lm1, Lm15 ;
hence P1 /\ P2 = (({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2}) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ {p2}) by A141, A153, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ {p2}) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ ({p2} \/ {p2})) by XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|))) \/ {p2}) ;
:: thesis: verum

end;

end;

end;

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

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

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

then p1 in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
then A155: (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|)) <> {} by A154, Lm22, XBOOLE_0:def 4;
(LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|)) c= {p1} by A132, A154, TOPREAL1:15, XBOOLE_1:27;
then A156: (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|)) = {p1} by A155, ZFMISC_1:33;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {p1} /\ (LSeg (|[0,0]|,|[1,0]|)) by A154, RLTOPSP1:70
.= {} by A154, Lm1, Lm14 ;
hence P1 /\ P2 = ({p1} \/ {p1}) \/ {p2} by A142, A156, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:1 ;
:: thesis: verum

end;

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

A158: not |[0,0]| in LSeg (|[0,1]|,p2) by A132, Lm5, Lm7, Lm11, TOPREAL1:4;
(LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|)) = (LSeg (|[0,1]|,p2)) /\ {|[0,0]|} by A157, RLTOPSP1:70
.= {} by A158, Lm1 ;
hence P1 /\ P2 = {p1,p2} by A142, A157, ENUMSET1:1, TOPREAL1:17; :: thesis: verum

end;

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

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

assume |[0,1]| in (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|)) ; :: thesis: contradiction
then A160: |[0,1]| in LSeg (|[0,0]|,p1) by XBOOLE_0:def 4;
|[0,0]| `2 <= p1 `2 by A15, A18, EUCLID:52;
then |[0,1]| `2 <= p1 `2 by A160, TOPREAL1:4;
then p1 `2 = 1 by A15, A17, Lm7, XXREAL_0:1;
hence contradiction by A15, A16, A159, EUCLID:53; :: thesis: verum

end;

then A161: {|[0,1]|} <> (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|)) by ZFMISC_1:31;
(LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|)) c= {|[0,1]|} by A4, A132, TOPREAL1:15, XBOOLE_1:27;
then A162: (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[0,0]|)) = {} by A161, ZFMISC_1:33;

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

assume |[0,0]| in (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) ; :: thesis: contradiction
then A163: |[0,0]| in LSeg (p1,|[0,1]|) by XBOOLE_0:def 4;
p1 `2 <= |[0,1]| `2 by A15, A17, EUCLID:52;
then p1 `2 = 0 by A15, A18, A163, Lm5, TOPREAL1:4;
hence contradiction by A15, A16, A159, EUCLID:53; :: thesis: verum

end;

then A164: {|[0,0]|} <> (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by ZFMISC_1:31;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= {|[0,0]|} by A13, TOPREAL1:17, XBOOLE_1:27;
then (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A164, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A142, A162, ENUMSET1:1; :: thesis: verum

end;

end;

end;

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

end;

suppose A165: 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 A166: LSeg (|[0,0]|,p2) c= LSeg (|[0,0]|,|[1,0]|) by Lm21, TOPREAL1:6;
LSeg (p1,|[0,0]|) c= LSeg (|[0,0]|,|[0,1]|) by A3, Lm20, TOPREAL1:6;
then A167: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A166, XBOOLE_1:27;
take P1 = (LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A168: |[0,0]| in LSeg (|[0,0]|,p2) by RLTOPSP1:68;
|[1,0]| in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
then A169: |[1,0]| in (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) by Lm25, XBOOLE_0:def 4;
|[0,0]| in LSeg (p1,|[0,0]|) by RLTOPSP1:68;
then (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,p2)) <> {} by A168, XBOOLE_0:def 4;
then A170: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,p2)) = {|[0,0]|} by A167, TOPREAL1:17, ZFMISC_1:33;
( p1 <> |[0,0]| or |[0,0]| <> p2 ) by A1;
hence P1 is_an_arc_of p1,p2 by A170, TOPREAL1:12; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A171: LSeg (|[0,0]|,|[0,1]|) = (LSeg (p1,|[0,0]|)) \/ (LSeg (p1,|[0,1]|)) by A3, TOPREAL1:5;
A172: LSeg (|[1,0]|,|[1,1]|) is_an_arc_of |[1,1]|,|[1,0]| by Lm9, Lm11, TOPREAL1:9;
LSeg (|[0,1]|,|[1,1]|) is_an_arc_of |[0,1]|,|[1,1]| by Lm6, Lm10, TOPREAL1:9;
then A173: (LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) is_an_arc_of |[0,1]|,|[1,0]| by A172, TOPREAL1:2, TOPREAL1:18;
A174: LSeg (|[1,0]|,p2) c= LSeg (|[0,0]|,|[1,0]|) by A165, Lm24, TOPREAL1:6;
then A175: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by XBOOLE_1:27;
A176: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A174, Lm2, XBOOLE_1:3, XBOOLE_1:26;
((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) /\ (LSeg (|[1,0]|,p2)) = ((LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= {|[1,0]|} by A176, A175, A169, TOPREAL1:16, ZFMISC_1:33 ;
then A177: ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2)) is_an_arc_of |[0,1]|,p2 by A173, TOPREAL1:10;
A178: (LSeg (|[0,0]|,p2)) /\ (LSeg (|[1,0]|,p2)) = {p2} by A165, TOPREAL1:8;
A179: LSeg (|[0,0]|,|[1,0]|) = (LSeg (|[1,0]|,p2)) \/ (LSeg (|[0,0]|,p2)) by A165, TOPREAL1:5;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[0,0]|} by A13, A174, TOPREAL1:17, XBOOLE_1:27;
then A180: ( (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) = {|[0,0]|} or (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) = {} ) by ZFMISC_1:33;
A181: LSeg (|[0,0]|,p2) c= LSeg (|[0,0]|,|[1,0]|) by A165, Lm21, TOPREAL1:6;
then A182: (LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by Lm2, XBOOLE_1:3, XBOOLE_1:27;
A183: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 <= 1 & q `1 >= 0 & q `2 = 0 ) by A165, TOPREAL1:13;

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

A185: p2 `1 <= |[1,0]| `1 by A183, EUCLID:52;
assume A186: |[0,0]| in (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) ; :: thesis: contradiction
then A187: |[0,0]| in LSeg (p1,|[0,1]|) by XBOOLE_0:def 4;
|[0,0]| in LSeg (p2,|[1,0]|) by A186, XBOOLE_0:def 4;
then A188: |[0,0]| `1 = p2 `1 by A183, A185, Lm4, TOPREAL1:3;
p1 `2 <= |[0,1]| `2 by A15, A17, EUCLID:52;
then |[0,0]| `2 = p1 `2 by A15, A18, A187, Lm5, TOPREAL1:4;
then p1 = |[(|[0,0]| `1),(|[0,0]| `2)]| by A15, A16, Lm4, EUCLID:53
.= p2 by A183, A188, Lm5, EUCLID:53 ;
hence contradiction by A1; :: thesis: verum

end;

(LSeg (p1,|[0,1]|)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))) = ((LSeg (p1,|[0,1]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[0,1]|,p1)) /\ (LSeg (|[1,0]|,|[1,1]|))) by A180, A184, XBOOLE_1:23, ZFMISC_1:31
.= {|[0,1]|} by A14, A10, A12, XBOOLE_0:def 10 ;
hence P2 is_an_arc_of p1,p2 by A177, 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,|[0,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:4
.= ((LSeg (|[0,0]|,|[0,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2)))) \/ (LSeg (|[0,0]|,p2)) by A171, XBOOLE_1:4
.= (LSeg (|[0,0]|,|[0,1]|)) \/ ((((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))) \/ (LSeg (|[0,0]|,p2))) by XBOOLE_1:4
.= (LSeg (|[0,0]|,|[0,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[1,0]|,p2)) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:4
.= (LSeg (|[0,0]|,|[0,1]|)) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) by A179, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A189: {p1} = (LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|)) by A3, TOPREAL1:8;
A190: P1 /\ P2 = ((LSeg (p1,|[0,0]|)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))))) \/ ((LSeg (|[0,0]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:23
.= (((LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))))) \/ ((LSeg (|[0,0]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,0]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2))))) \/ ((LSeg (|[0,0]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))))) by A189, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2))))) \/ ((LSeg (|[0,0]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2))))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[0,0]|,p2)) /\ (((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2))))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ (((LSeg (|[0,0]|,p2)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2})) by A178, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2))))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ ((((LSeg (|[0,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2))))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2})) by A9, A182 ;

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

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

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

then not p2 in LSeg (p1,|[0,0]|) by A4, Lm4, Lm6, Lm8, TOPREAL1:3;
then A193: LSeg (p1,|[0,0]|) misses {p2} by ZFMISC_1:50;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) = (LSeg (p1,|[0,0]|)) /\ {p2} by A192, RLTOPSP1:70
.= {} by A193, XBOOLE_0:def 7 ;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2}) by A190, A192, TOPREAL1:16; :: thesis: verum

end;

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

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

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

end;

then A196: {|[0,0]|} <> (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) by ZFMISC_1:31;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[0,0]|} by A4, A174, TOPREAL1:17, XBOOLE_1:27;
then A197: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A196, ZFMISC_1:33;

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

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

end;

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

end;

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

then p2 in LSeg (p1,|[0,0]|) by RLTOPSP1:68;
then A201: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) <> {} by A200, Lm21, XBOOLE_0:def 4;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) c= {p2} by A4, A200, TOPREAL1:17, XBOOLE_1:27;
then A202: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) = {p2} by A201, ZFMISC_1:33;
(LSeg (|[0,0]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {|[0,0]|} /\ (LSeg (|[1,0]|,|[1,1]|)) by A200, RLTOPSP1:70
.= {} by Lm1, Lm12 ;
hence P1 /\ P2 = (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2}) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2}) by A190, A202, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2}) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ ({p2} \/ {p2})) by XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2}) ;
:: thesis: verum

end;

end;

end;

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

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

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

then A204: (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) = (LSeg (|[0,0]|,p2)) /\ {p1} by RLTOPSP1:70;
not p1 in LSeg (|[0,0]|,p2) by A181, A203, Lm5, Lm7, Lm9, TOPREAL1:4;
then (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) = {} by A204, Lm1;
hence P1 /\ P2 = {p1,p2} by A191, A203, ENUMSET1:1, TOPREAL1:15; :: thesis: verum

end;

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

|[0,0]| in LSeg (|[0,0]|,p2) by RLTOPSP1:68;
then A206: (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) <> {} by A205, Lm20, XBOOLE_0:def 4;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {p1} /\ (LSeg (|[0,1]|,|[1,1]|)) by A205, RLTOPSP1:70;
then A207: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A205, Lm1, Lm13;
(LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A165, A205, Lm21, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) = {p1} by A205, A206, TOPREAL1:17, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ {p1}) \/ {p2} by A191, A207, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:1 ;
:: thesis: verum

end;

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

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

assume |[0,0]| in (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) ; :: thesis: contradiction
then A209: |[0,0]| in LSeg (p1,|[0,1]|) by XBOOLE_0:def 4;
p1 `2 <= |[0,1]| `2 by A15, A17, EUCLID:52;
then p1 `2 = 0 by A15, A18, A209, Lm5, TOPREAL1:4;
hence contradiction by A15, A16, A208, EUCLID:53; :: thesis: verum

end;

then A210: {|[0,0]|} <> (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) by ZFMISC_1:31;
(LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A13, A181, XBOOLE_1:27;
then A211: (LSeg (|[0,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) = {} by A210, TOPREAL1:17, ZFMISC_1:33;

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

assume |[0,1]| in (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; :: thesis: contradiction
then A212: |[0,1]| in LSeg (|[0,0]|,p1) by XBOOLE_0:def 4;
|[0,0]| `2 <= p1 `2 by A15, A18, EUCLID:52;
then |[0,1]| `2 <= p1 `2 by A212, TOPREAL1:4;
then p1 `2 = 1 by A15, A17, Lm7, XXREAL_0:1;
hence contradiction by A15, A16, A208, EUCLID:53; :: thesis: verum

end;

then A213: {|[0,1]|} <> (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= {|[0,1]|} by A4, TOPREAL1:15, XBOOLE_1:27;
then (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A213, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A191, A211, ENUMSET1:1; :: thesis: verum

end;

end;

end;

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

end;

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

now :: thesis: for a being object st a in (LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|)) holds
a in {p1}

let a be object ; :: thesis: ( a in (LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|)) implies a in {p1} )
assume A215: a in (LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|)) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
a in LSeg (p1,|[0,1]|) by A215, XBOOLE_0:def 4;
then A216: p1 `2 <= p `2 by A15, A17, Lm7, TOPREAL1:4;
A217: a in LSeg (|[0,0]|,p1) by A215, XBOOLE_0:def 4;
then p `2 <= p1 `2 by A15, A18, Lm5, TOPREAL1:4;
then A218: p `2 = p1 `2 by A216, XXREAL_0:1;
p `1 <= p1 `1 by A15, A16, A217, Lm4, TOPREAL1:3;
then p `1 = p1 `1 by A15, A16, A217, Lm4, TOPREAL1:3;
then a = |[(p1 `1),(p1 `2)]| by A218, EUCLID:53
.= p1 by EUCLID:53 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum

end;

then A219: (LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|)) c= {p1} ;
A220: p2 in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
p2 in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
then p2 in (LSeg (|[1,0]|,p2)) /\ (LSeg (|[1,1]|,p2)) by A220, XBOOLE_0:def 4;
then A221: {p2} c= (LSeg (|[1,0]|,p2)) /\ (LSeg (|[1,1]|,p2)) by ZFMISC_1:31;
A222: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) by A214, TOPREAL1:13;

now :: thesis: for a being object st a in (LSeg (|[1,0]|,p2)) /\ (LSeg (|[1,1]|,p2)) holds
a in {p2}

let a be object ; :: thesis: ( a in (LSeg (|[1,0]|,p2)) /\ (LSeg (|[1,1]|,p2)) implies a in {p2} )
assume A223: a in (LSeg (|[1,0]|,p2)) /\ (LSeg (|[1,1]|,p2)) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A224: a in LSeg (|[1,0]|,p2) by A223, XBOOLE_0:def 4;
then A225: p2 `1 <= p `1 by A222, Lm8, TOPREAL1:3;
a in LSeg (p2,|[1,1]|) by A223, XBOOLE_0:def 4;
then A226: p2 `2 <= p `2 by A222, Lm11, TOPREAL1:4;
p `1 <= p2 `1 by A222, A224, Lm8, TOPREAL1:3;
then A227: p `1 = p2 `1 by A225, XXREAL_0:1;
p `2 <= p2 `2 by A222, A224, Lm9, TOPREAL1:4;
then p `2 = p2 `2 by A226, XXREAL_0:1;
then a = |[(p2 `1),(p2 `2)]| by A227, EUCLID:53
.= p2 by EUCLID:53 ;
hence a in {p2} by TARSKI:def 1; :: thesis: verum

end;

then A228: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[1,1]|,p2)) c= {p2} ;
LSeg (|[1,0]|,p2) c= LSeg (|[1,0]|,|[1,1]|) by A214, Lm25, TOPREAL1:6;
then A229: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[1,0]|} by TOPREAL1:16, XBOOLE_1:27;
take P1 = ((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A230: |[1,0]| in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
|[1,0]| in LSeg (|[0,0]|,|[1,0]|) by RLTOPSP1:68;
then (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) <> {} by A230, XBOOLE_0:def 4;
then (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) = {|[1,0]|} by A229, ZFMISC_1:33;
then A231: (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,p2)) is_an_arc_of |[0,0]|,p2 by Lm4, Lm8, TOPREAL1:12;
LSeg (|[1,0]|,p2) c= LSeg (|[1,0]|,|[1,1]|) by A214, Lm25, TOPREAL1:6;
then A232: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A4, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg (p1,|[0,0]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,p2))) = ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= {|[0,0]|} by A5, A6, A232, TOPREAL1:17, XBOOLE_0:def 10 ;
then (LSeg (p1,|[0,0]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,p2))) is_an_arc_of p1,p2 by A231, 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 A233: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) <> {} by Lm26, XBOOLE_0:def 4;
A234: LSeg (|[1,1]|,p2) c= LSeg (|[1,0]|,|[1,1]|) by A214, Lm27, TOPREAL1:6;
then A235: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A13, Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) c= {|[1,1]|} by A234, TOPREAL1:18, XBOOLE_1:27;
then (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) = {|[1,1]|} by A233, ZFMISC_1:33;
then A236: (LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,1]|,p2)) is_an_arc_of |[0,1]|,p2 by Lm6, Lm10, TOPREAL1:12;
(LSeg (p1,|[0,1]|)) /\ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,1]|,p2))) = ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= {|[0,1]|} by A10, A12, A235, XBOOLE_0:def 10 ;
then (LSeg (p1,|[0,1]|)) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ (LSeg (|[1,1]|,p2))) is_an_arc_of p1,p2 by A236, 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 (p1,|[0,0]|)) \/ (LSeg (p1,|[0,1]|))) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) by A3, TOPREAL1:5, TOPREAL1:def 2
.= ((LSeg (p1,|[0,0]|)) \/ ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:4
.= (LSeg (p1,|[0,0]|)) \/ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) by XBOOLE_1:4
.= (LSeg (p1,|[0,0]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|)))) by XBOOLE_1:4
.= ((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:4
.= ((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ ((LSeg (|[1,1]|,p2)) \/ (LSeg (|[1,0]|,p2)))) by A214, TOPREAL1:5
.= ((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[1,0]|,p2)) \/ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A237: p1 in LSeg (p1,|[0,1]|) by RLTOPSP1:68;
p1 in LSeg (p1,|[0,0]|) by RLTOPSP1:68;
then p1 in (LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|)) by A237, XBOOLE_0:def 4;
then {p1} c= (LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|)) by ZFMISC_1:31;
then A238: (LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|)) = {p1} by A219, XBOOLE_0:def 10;
A239: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A4, A234, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A240: LSeg (|[1,0]|,p2) c= LSeg (|[1,0]|,|[1,1]|) by A214, Lm25, TOPREAL1:6;
then A241: (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) = {} by A13, Lm3, XBOOLE_1:3, XBOOLE_1:27;
A242: P1 /\ P2 = (((LSeg (p1,|[0,0]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:23
.= (((LSeg (p1,|[0,0]|)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:23
.= ((((LSeg (p1,|[0,0]|)) /\ ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[1,1]|,p2)))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:23
.= ((((LSeg (p1,|[0,0]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by A239, XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,|[1,0]|)) /\ ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by A238, XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ ((LSeg (|[1,0]|,p2)) /\ (LSeg (|[1,1]|,p2)))) by Lm2, XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2}) by A221, A228, XBOOLE_0:def 10
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ ((((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)))) \/ (((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|))) \/ {p2}) by A241 ;

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

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

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

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

end;

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

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

end;

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

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 A247: |[1,1]| in LSeg (|[1,0]|,p2) by XBOOLE_0:def 4;
|[1,0]| `2 <= p2 `2 by A222, EUCLID:52;
then |[1,1]| `2 <= p2 `2 by A247, TOPREAL1:4;
then |[1,1]| `2 = p2 `2 by A222, Lm11, XXREAL_0:1;
then p2 = |[(|[1,1]| `1),(|[1,1]| `2)]| by A222, Lm10, EUCLID:53
.= |[1,1]| by EUCLID:53 ;
hence contradiction by A246; :: thesis: verum

end;

then A248: {|[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 A240, XBOOLE_1:27;
then A249: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A248, TOPREAL1:18, ZFMISC_1:33;

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

assume |[1,0]| in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) ; :: thesis: contradiction
then A250: |[1,0]| in LSeg (p2,|[1,1]|) by XBOOLE_0:def 4;
p2 `2 <= |[1,1]| `2 by A222, EUCLID:52;
then p2 `2 = |[1,0]| `2 by A222, A250, Lm9, TOPREAL1:4;
then p2 = |[(|[1,0]| `1),(|[1,0]| `2)]| by A222, Lm8, EUCLID:53
.= |[1,0]| by EUCLID:53 ;
hence contradiction by A246; :: thesis: verum

end;

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

end;

end;

end;

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

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

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

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

end;

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

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

assume |[0,1]| in (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) ; :: thesis: contradiction
then A254: |[0,1]| in LSeg (|[0,0]|,p1) by XBOOLE_0:def 4;
|[0,0]| `2 <= p1 `2 by A15, A18, EUCLID:52;
then |[0,1]| `2 <= p1 `2 by A254, TOPREAL1:4;
then p1 `2 = |[0,1]| `2 by A15, A17, Lm7, XXREAL_0:1;
then p1 = |[(|[0,1]| `1),(|[0,1]| `2)]| by A15, A16, Lm6, EUCLID:53
.= |[0,1]| by EUCLID:53 ;
hence contradiction by A253; :: thesis: verum

end;

then A255: {|[0,1]|} <> (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) c= {|[0,1]|} by A4, TOPREAL1:15, XBOOLE_1:27;
then A256: (LSeg (p1,|[0,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by A255, ZFMISC_1:33;

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

assume |[0,0]| in (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (p1,|[0,1]|)) ; :: thesis: contradiction
then |[0,0]| in LSeg (p1,|[0,1]|) by XBOOLE_0:def 4;
then p1 `2 = |[0,0]| `2 by A15, A17, A18, Lm5, Lm7, TOPREAL1:4;
then p1 = |[(|[0,0]| `1),(|[0,0]| `2)]| by A15, A16, Lm4, EUCLID:53
.= |[0,0]| by EUCLID:53 ;
hence contradiction by A253; :: thesis: verum

end;

then A257: {|[0,0]|} <> (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (p1,|[0,1]|)) by ZFMISC_1:31;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (p1,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A13, XBOOLE_1:27;
then (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (p1,|[0,1]|)) = {} by A257, TOPREAL1:17, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A243, A256, ENUMSET1:1; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

end;