let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 <> p2 & p2 in R^2-unit_square & p1 in LSeg (|[0,1]|,|[1,1]|) implies ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} ) )
assume that
A1: p1 <> p2 and
A2: p2 in R^2-unit_square and
A3: p1 in LSeg (|[0,1]|,|[1,1]|) ; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A4: ( p2 in (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,1]|,|[1,1]|)) or p2 in (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) ) by A2, TOPREAL1:def 2, XBOOLE_0:def 3;
A5: (LSeg (|[0,1]|,p1)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, Lm23, TOPREAL1:6, XBOOLE_1:26;
|[1,1]| in LSeg (p1,|[1,1]|) by RLTOPSP1:68;
then A6: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) <> {} by Lm27, XBOOLE_0:def 4;
|[0,1]| in LSeg (|[0,1]|,p1) by RLTOPSP1:68;
then A7: (LSeg (|[0,1]|,p1)) /\ (LSeg (|[0,0]|,|[0,1]|)) <> {} by Lm22, XBOOLE_0:def 4;
A8: LSeg (p1,|[1,1]|) c= LSeg (|[0,1]|,|[1,1]|) by A3, Lm26, TOPREAL1:6;
then A9: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by Lm2, XBOOLE_1:3, XBOOLE_1:26;
A10: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {|[1,1]|} by A3, Lm26, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
A11: LSeg (|[0,1]|,p1) c= LSeg (|[0,1]|,|[1,1]|) by A3, Lm23, TOPREAL1:6;
then A12: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by Lm2, XBOOLE_1:3, XBOOLE_1:26;
consider q1 being Point of (TOP-REAL 2) such that
A13: q1 = p1 and
A14: q1 `1 <= 1 and
A15: q1 `1 >= 0 and
A16: q1 `2 = 1 by A3, TOPREAL1:13;
per cases ( p2 in LSeg (|[0,0]|,|[0,1]|) or p2 in LSeg (|[0,1]|,|[1,1]|) or p2 in LSeg (|[0,0]|,|[1,0]|) or p2 in LSeg (|[1,0]|,|[1,1]|) ) by A4, XBOOLE_0:def 3;
suppose A17: p2 in LSeg (|[0,0]|,|[0,1]|) ; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
then A18: LSeg (|[0,1]|,p2) c= LSeg (|[0,0]|,|[0,1]|) by Lm22, TOPREAL1:6;
LSeg (p1,|[0,1]|) c= LSeg (|[0,1]|,|[1,1]|) by A3, Lm23, TOPREAL1:6;
then A19: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A18, XBOOLE_1:27;
take P1 = (LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,1]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A20: |[0,1]| in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
|[0,0]| in LSeg (|[0,0]|,p2) by RLTOPSP1:68;
then A21: {} <> (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) by Lm21, XBOOLE_0:def 4;
|[0,1]| in LSeg (p1,|[0,1]|) by RLTOPSP1:68;
then (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) <> {} by A20, XBOOLE_0:def 4;
then A22: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) = {|[0,1]|} by A19, TOPREAL1:15, ZFMISC_1:33;
( p1 <> |[0,1]| or p2 <> |[0,1]| ) by A1;
hence P1 is_an_arc_of p1,p2 by A22, TOPREAL1:12; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A23: (LSeg (p1,|[0,1]|)) \/ (LSeg (p1,|[1,1]|)) = LSeg (|[0,1]|,|[1,1]|) by A3, TOPREAL1:5;
A24: LSeg (|[1,0]|,|[1,1]|) is_an_arc_of |[1,1]|,|[1,0]| by Lm9, Lm11, TOPREAL1:9;
LSeg (|[0,0]|,|[1,0]|) is_an_arc_of |[1,0]|,|[0,0]| by Lm4, Lm8, TOPREAL1:9;
then A25: (LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)) is_an_arc_of |[1,1]|,|[0,0]| by A24, TOPREAL1:2, TOPREAL1:16;
A26: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,p2)) c= {|[0,0]|} by A17, Lm20, TOPREAL1:6, TOPREAL1:17, XBOOLE_1:26;
A27: (LSeg (|[0,0]|,p2)) \/ (LSeg (|[0,1]|,p2)) = LSeg (|[0,0]|,|[0,1]|) by A17, TOPREAL1:5;
A28: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,p2)) = {p2} by A17, TOPREAL1:8;
A29: LSeg (|[0,0]|,p2) c= LSeg (|[0,0]|,|[0,1]|) by A17, Lm20, TOPREAL1:6;
then A30: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by Lm3, XBOOLE_1:3, XBOOLE_1:27;
A31: ex q2 being Point of (TOP-REAL 2) st
( q2 = p2 & q2 `1 = 0 & q2 `2 <= 1 & q2 `2 >= 0 ) by A17, TOPREAL1:13;
((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) /\ (LSeg (|[0,0]|,p2)) = ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,p2))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))) by XBOOLE_1:23
.= {|[0,0]|} by A26, A21, A30, ZFMISC_1:33 ;
then A37: ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2)) is_an_arc_of |[1,1]|,p2 by A25, TOPREAL1:10;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A8, A29, XBOOLE_1:27;
then A38: ( (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {|[0,1]|} or (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} ) by TOPREAL1:15, ZFMISC_1:33;
A39: LSeg (p2,|[0,1]|) c= LSeg (|[0,0]|,|[0,1]|) by A17, Lm22, TOPREAL1:6;
then A40: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg (p1,|[1,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))) = ((LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) by A38, A32, XBOOLE_1:23, ZFMISC_1:31
.= {|[1,1]|} by A9, A6, A10, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A37, 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,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))) by XBOOLE_1:4
.= (LSeg (|[0,1]|,p2)) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2)))) by A23, XBOOLE_1:4
.= (LSeg (|[0,1]|,p2)) \/ (((LSeg (|[0,1]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ (LSeg (|[0,0]|,p2))) by XBOOLE_1:4
.= ((LSeg (|[0,0]|,p2)) \/ (LSeg (|[0,1]|,p2))) \/ ((LSeg (|[0,1]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) by XBOOLE_1:4
.= R^2-unit_square by A27, TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A41: {p1} = (LSeg (p1,|[0,1]|)) /\ (LSeg (p1,|[1,1]|)) by A3, TOPREAL1:8;
A42: P1 /\ P2 = ((LSeg (p1,|[0,1]|)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))) by XBOOLE_1:23
.= (((LSeg (p1,|[0,1]|)) /\ (LSeg (p1,|[1,1]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,1]|)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))) by A41, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[0,1]|,p2)) /\ ((LSeg (p1,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ ((LSeg (|[0,1]|,p2)) /\ (((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[0,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ (((LSeg (|[0,1]|,p2)) /\ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2})) by A12, A28, XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ ((((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[0,1]|,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})) by A40 ;
A43: now :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
per cases ( p1 = |[0,1]| or p1 = |[1,1]| or ( p1 <> |[1,1]| & p1 <> |[0,1]| ) ) ;
suppose A44: p1 = |[0,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
then p1 in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
then A45: (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|)) <> {} by A44, Lm23, XBOOLE_0:def 4;
(LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|)) c= {p1} by A39, A44, TOPREAL1:15, XBOOLE_1:27;
then A46: (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|)) = {p1} by A45, ZFMISC_1:33;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {p1} /\ (LSeg (|[1,0]|,|[1,1]|)) by A44, RLTOPSP1:70;
then (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by A44, Lm1, Lm15;
hence P1 /\ P2 = ({p1} \/ ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by A42, A46, XBOOLE_1:4
.= (({p1} \/ {p1}) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) ;
:: thesis: verum
end;
suppose A47: p1 = |[1,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
then A48: (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|)) = (LSeg (|[0,1]|,p2)) /\ {p1} by RLTOPSP1:70;
not p1 in LSeg (|[0,1]|,p2) by A31, A47, Lm6, Lm10, TOPREAL1:3;
then (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|)) = {} by A48, Lm1;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by A42, A47, TOPREAL1:18, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) ;
:: thesis: verum
end;
suppose A49: ( p1 <> |[1,1]| & p1 <> |[0,1]| ) ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})
then A51: {|[0,1]|} <> (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|)) by ZFMISC_1:31;
(LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|)) c= {|[0,1]|} by A8, A39, TOPREAL1:15, XBOOLE_1:27;
then A52: (LSeg (|[0,1]|,p2)) /\ (LSeg (p1,|[1,1]|)) = {} by A51, ZFMISC_1:33;
then A54: {|[1,1]|} <> (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {|[1,1]|} by A11, TOPREAL1:18, XBOOLE_1:27;
then (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by A54, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2}) by A42, A52; :: thesis: verum
end;
end;
end;
now :: thesis: P1 /\ P2 = {p1,p2}
per cases ( ( p2 <> |[0,0]| & p2 <> |[0,1]| ) or p2 = |[0,0]| or p2 = |[0,1]| ) ;
suppose A55: ( p2 <> |[0,0]| & p2 <> |[0,1]| ) ; :: thesis: P1 /\ P2 = {p1,p2}
then A57: {|[0,1]|} <> (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) by ZFMISC_1:31;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A11, A29, XBOOLE_1:27;
then A58: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A57, TOPREAL1:15, ZFMISC_1:33;
then A60: {|[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 A39, TOPREAL1:17, XBOOLE_1:27;
then (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A60, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A43, A58, ENUMSET1:1; :: thesis: verum
end;
suppose A63: p2 = |[0,1]| ; :: thesis: P1 /\ P2 = {p1,p2}
then p2 in LSeg (p1,|[0,1]|) by RLTOPSP1:68;
then A64: {} <> (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) by A63, Lm22, XBOOLE_0:def 4;
(LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[0,1]|} /\ (LSeg (|[0,0]|,|[1,0]|)) by A63, RLTOPSP1:70;
then A65: (LSeg (|[0,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by Lm1, Lm14;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A11, A29, XBOOLE_1:27;
then (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) = {p2} by A63, A64, TOPREAL1:15, ZFMISC_1:33;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A43, A65, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:1 ;
:: thesis: verum
end;
end;
end;
hence P1 /\ P2 = {p1,p2} ; :: thesis: verum
end;
suppose A66: p2 in LSeg (|[0,1]|,|[1,1]|) ; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A67: q1 = |[(q1 `1),(q1 `2)]| by EUCLID:53;
A68: LSeg (p1,p2) c= LSeg (|[0,1]|,|[1,1]|) by A3, A66, TOPREAL1:6;
consider q being Point of (TOP-REAL 2) such that
A69: q = p2 and
A70: q `1 <= 1 and
A71: q `1 >= 0 and
A72: q `2 = 1 by A66, TOPREAL1:13;
A73: 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 ( q1 `1 < q `1 or q `1 < q1 `1 ) by A1, A13, A16, A69, A72, A67, A73, XXREAL_0:1;
suppose A74: q1 `1 < q `1 ; :: thesis: ex P1 being Element of 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} )
A75: (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) c= {p2}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) or a in {p2} )
assume A76: a in (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A77: p in LSeg (p2,|[1,1]|) by A76, XBOOLE_0:def 4;
p2 `1 <= |[1,1]| `1 by A69, A70, EUCLID:52;
then A78: p2 `1 <= p `1 by A77, TOPREAL1:3;
A79: p in LSeg (p1,p2) by A76, XBOOLE_0:def 4;
then A80: p `2 <= p2 `2 by A13, A16, A69, A72, TOPREAL1:4;
p `1 <= p2 `1 by A13, A69, A74, A79, TOPREAL1:3;
then A81: p2 `1 = p `1 by A78, XXREAL_0:1;
p1 `2 <= p `2 by A13, A16, A69, A72, A79, TOPREAL1:4;
then p `2 = 1 by A13, A16, A69, A72, A80, XXREAL_0:1;
then p = |[(p2 `1),1]| by A81, EUCLID:53
.= p2 by A69, A72, 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 A82: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A11, XBOOLE_1:3, XBOOLE_1:26;
A83: now :: thesis: not (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) <> {}
set a = the Element of (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2));
assume A84: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) <> {} ; :: thesis: contradiction
then reconsider p = the Element of (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) as Point of (TOP-REAL 2) by TARSKI:def 3;
A85: p in LSeg (|[0,1]|,p1) by A84, XBOOLE_0:def 4;
A86: p in LSeg (p2,|[1,1]|) by A84, XBOOLE_0:def 4;
p2 `1 <= |[1,1]| `1 by A69, A70, EUCLID:52;
then A87: p2 `1 <= p `1 by A86, TOPREAL1:3;
|[0,1]| `1 <= p1 `1 by A13, A15, EUCLID:52;
then p `1 <= p1 `1 by A85, TOPREAL1:3;
hence contradiction by A13, A69, A74, A87, XXREAL_0:2; :: thesis: verum
end;
A88: ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) /\ (LSeg (|[1,0]|,|[1,1]|)) = ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:23
.= {|[1,0]|} by Lm3, TOPREAL1:16 ;
(LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)) is_an_arc_of |[0,1]|,|[1,0]| by Lm5, Lm7, TOPREAL1:9, TOPREAL1:10, TOPREAL1:17;
then A89: ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|)) is_an_arc_of |[0,1]|,|[1,1]| by A88, TOPREAL1:10;
A90: (LSeg (p1,p2)) /\ (LSeg (p1,|[0,1]|)) c= {p1}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p1,p2)) /\ (LSeg (p1,|[0,1]|)) or a in {p1} )
assume A91: a in (LSeg (p1,p2)) /\ (LSeg (p1,|[0,1]|)) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A92: p in LSeg (|[0,1]|,p1) by A91, XBOOLE_0:def 4;
|[0,1]| `1 <= p1 `1 by A13, A15, EUCLID:52;
then A93: p `1 <= p1 `1 by A92, TOPREAL1:3;
A94: p in LSeg (p1,p2) by A91, XBOOLE_0:def 4;
then A95: p `2 <= p2 `2 by A13, A16, A69, A72, TOPREAL1:4;
p1 `1 <= p `1 by A13, A69, A74, A94, TOPREAL1:3;
then A96: p1 `1 = p `1 by A93, XXREAL_0:1;
p1 `2 <= p `2 by A13, A16, A69, A72, A94, TOPREAL1:4;
then p `2 = 1 by A13, A16, A69, A72, A95, XXREAL_0:1;
then p = |[(p1 `1),1]| by A96, EUCLID:53
.= p1 by A13, A16, EUCLID:53 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum
end;
A97: (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, A66, TOPREAL1:6, XBOOLE_1:26;
now :: thesis: not |[1,1]| in (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))
assume |[1,1]| in (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; :: thesis: contradiction
then A98: |[1,1]| in LSeg (|[0,1]|,p1) by XBOOLE_0:def 4;
|[0,1]| `1 <= p1 `1 by A13, A15, EUCLID:52;
then |[1,1]| `1 <= p1 `1 by A98, TOPREAL1:3;
hence contradiction by A13, A14, A70, A74, Lm10, XXREAL_0:1; :: thesis: verum
end;
then A99: {|[1,1]|} <> (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {|[1,1]|} by A3, Lm23, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
then A100: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by A99, ZFMISC_1:33;
|[0,1]| in LSeg (p1,|[0,1]|) by RLTOPSP1:68;
then A101: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) <> {} by Lm22, XBOOLE_0:def 4;
then A103: {|[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 A66, Lm26, TOPREAL1:6, TOPREAL1:15, XBOOLE_1:26;
then A104: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A103, ZFMISC_1:33;
take P1 = LSeg (p1,p2); :: thesis: ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[0,1]|)) \/ ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A105: p1 in LSeg (p1,|[0,1]|) by RLTOPSP1:68;
A106: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, Lm23, TOPREAL1:6, XBOOLE_1:26;
|[1,1]| in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
then A107: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) <> {} by Lm27, XBOOLE_0:def 4;
(LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A66, Lm26, TOPREAL1:6, XBOOLE_1:26;
then A108: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) = {|[1,1]|} by A107, TOPREAL1:18, ZFMISC_1:33;
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} )
A109: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A66, Lm26, TOPREAL1:6, XBOOLE_1:26;
then A110: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)) = {} by A109, XBOOLE_1:3;
(((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) /\ (LSeg (|[1,1]|,p2)) = (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) /\ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= (((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,1]|,p2)))) \/ {|[1,1]|} by A108, XBOOLE_1:23
.= {|[1,1]|} by A104, A110 ;
then A111: (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)) is_an_arc_of |[0,1]|,p2 by A89, TOPREAL1:10;
(LSeg (p1,|[0,1]|)) /\ ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) = ((LSeg (p1,|[0,1]|)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,1]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[0,1]|)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) by A83, XBOOLE_1:23
.= ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) by A100, XBOOLE_1:23
.= {|[0,1]|} by A82, A106, A101, TOPREAL1:15, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A111, TOPREAL1:11; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = ((LSeg (|[0,1]|,p1)) \/ (LSeg (p1,p2))) \/ ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2))) by XBOOLE_1:4
.= (((LSeg (|[0,1]|,p1)) \/ (LSeg (p1,p2))) \/ (LSeg (p2,|[1,1]|))) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) by XBOOLE_1:4
.= (LSeg (|[0,1]|,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) by A3, A66, TOPREAL1:7
.= (LSeg (|[0,1]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) by XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A112: p2 in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then p2 in (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) by A112, XBOOLE_0:def 4;
then {p2} c= (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) by ZFMISC_1:31;
then A113: (LSeg (p1,p2)) /\ (LSeg (|[1,1]|,p2)) = {p2} by A75, XBOOLE_0:def 10;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
then A114: (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A68, XBOOLE_1:3, XBOOLE_1:26;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then p1 in (LSeg (p1,p2)) /\ (LSeg (p1,|[0,1]|)) by A105, XBOOLE_0:def 4;
then {p1} c= (LSeg (p1,p2)) /\ (LSeg (p1,|[0,1]|)) by ZFMISC_1:31;
then A115: (LSeg (p1,p2)) /\ (LSeg (p1,|[0,1]|)) = {p1} by A90, XBOOLE_0:def 10;
A116: P1 /\ P2 = ((LSeg (p1,p2)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (p1,p2)) /\ ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2}) by A115, A113, XBOOLE_1:23
.= {p1} \/ ((((LSeg (p1,p2)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2})) by A114, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by XBOOLE_1:4 ;
A117: now :: thesis: P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2})
per cases ( p1 = |[0,1]| or p1 <> |[0,1]| ) ;
suppose A118: p1 = |[0,1]| ; :: thesis: P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2})
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) <> {} by A118, Lm22, XBOOLE_0:def 4;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {p1} by A97, A118, TOPREAL1:15, ZFMISC_1:33;
hence P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by A116; :: thesis: verum
end;
suppose A119: p1 <> |[0,1]| ; :: thesis: P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2})
now :: thesis: not |[0,1]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))
assume |[0,1]| in (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) ; :: thesis: contradiction
then |[0,1]| in LSeg (p1,p2) by XBOOLE_0:def 4;
then p1 `1 = 0 by A13, A15, A69, A74, Lm6, TOPREAL1:3;
hence contradiction by A13, A16, A119, EUCLID:53; :: thesis: verum
end;
then {|[0,1]|} <> (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A97, TOPREAL1:15, ZFMISC_1:33;
hence P1 /\ P2 = {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ {p2}) by A116; :: thesis: verum
end;
end;
end;
A120: (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {|[1,1]|} by A3, A66, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
now :: thesis: P1 /\ P2 = {p1,p2}
per cases ( p2 = |[1,1]| or p2 <> |[1,1]| ) ;
suppose A121: p2 = |[1,1]| ; :: thesis: P1 /\ P2 = {p1,p2}
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) <> {} by A121, Lm27, XBOOLE_0:def 4;
then (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {p2} by A120, A121, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A117, ENUMSET1:1; :: thesis: verum
end;
suppose A122: p2 <> |[1,1]| ; :: thesis: P1 /\ P2 = {p1,p2}
now :: thesis: not |[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))
assume |[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; :: thesis: contradiction
then |[1,1]| in LSeg (p1,p2) by XBOOLE_0:def 4;
then |[1,1]| `1 <= p2 `1 by A13, A69, A74, TOPREAL1:3;
then p2 `1 = 1 by A69, A70, Lm10, XXREAL_0:1;
hence contradiction by A69, A72, A122, EUCLID:53; :: thesis: verum
end;
then {|[1,1]|} <> (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by A120, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A117, ENUMSET1:1; :: thesis: verum
end;
end;
end;
hence P1 /\ P2 = {p1,p2} ; :: thesis: verum
end;
suppose A123: q `1 < q1 `1 ; :: thesis: ex P1 being Element of 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} )
A124: (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 A125: a in (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)) ; :: thesis: a in {p2}
then reconsider p = a as Point of (TOP-REAL 2) ;
A126: p in LSeg (|[0,1]|,p2) by A125, XBOOLE_0:def 4;
|[0,1]| `1 <= p2 `1 by A69, A71, EUCLID:52;
then A127: p `1 <= p2 `1 by A126, TOPREAL1:3;
A128: p in LSeg (p2,p1) by A125, XBOOLE_0:def 4;
then A129: p `2 <= p1 `2 by A13, A16, A69, A72, TOPREAL1:4;
p2 `1 <= p `1 by A13, A69, A123, A128, TOPREAL1:3;
then A130: p2 `1 = p `1 by A127, XXREAL_0:1;
p2 `2 <= p `2 by A13, A16, A69, A72, A128, TOPREAL1:4;
then p `2 = 1 by A13, A16, A69, A72, A129, XXREAL_0:1;
then p = |[(p2 `1),1]| by A130, EUCLID:53
.= p2 by A69, A72, 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 A131: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A8, XBOOLE_1:3, XBOOLE_1:26;
A132: now :: thesis: not (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) <> {}
set a = the Element of (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2));
assume A133: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) <> {} ; :: thesis: contradiction
then reconsider p = the Element of (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) as Point of (TOP-REAL 2) by TARSKI:def 3;
A134: p in LSeg (p1,|[1,1]|) by A133, XBOOLE_0:def 4;
A135: p in LSeg (|[0,1]|,p2) by A133, XBOOLE_0:def 4;
|[0,1]| `1 <= p2 `1 by A69, A71, EUCLID:52;
then A136: p `1 <= p2 `1 by A135, TOPREAL1:3;
p1 `1 <= |[1,1]| `1 by A13, A14, EUCLID:52;
then p1 `1 <= p `1 by A134, TOPREAL1:3;
hence contradiction by A13, A69, A123, A136, XXREAL_0:2; :: thesis: verum
end;
A137: ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) /\ (LSeg (|[0,0]|,|[0,1]|)) = ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) by XBOOLE_1:23
.= {|[0,0]|} by Lm3, TOPREAL1:17 ;
(LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)) is_an_arc_of |[1,1]|,|[0,0]| by Lm9, Lm11, TOPREAL1:9, TOPREAL1:10, TOPREAL1:16;
then A138: ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|)) is_an_arc_of |[1,1]|,|[0,1]| by A137, TOPREAL1:10;
then A140: {|[1,1]|} <> (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) by ZFMISC_1:31;
(LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A66, Lm23, TOPREAL1:6, XBOOLE_1:26;
then A141: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A140, TOPREAL1:18, ZFMISC_1:33;
|[1,1]| in LSeg (p1,|[1,1]|) by RLTOPSP1:68;
then A142: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) <> {} by Lm27, XBOOLE_0:def 4;
then A144: {|[0,1]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, Lm26, TOPREAL1:6, XBOOLE_1:26;
then A145: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A144, TOPREAL1:15, ZFMISC_1:33;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
then A146: (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A68, XBOOLE_1:3, XBOOLE_1:26;
A147: (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) c= {p1}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) or a in {p1} )
assume A148: a in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) ; :: thesis: a in {p1}
then reconsider p = a as Point of (TOP-REAL 2) ;
A149: p in LSeg (p1,|[1,1]|) by A148, XBOOLE_0:def 4;
p1 `1 <= |[1,1]| `1 by A13, A14, EUCLID:52;
then A150: p1 `1 <= p `1 by A149, TOPREAL1:3;
A151: p in LSeg (p2,p1) by A148, XBOOLE_0:def 4;
then A152: p `2 <= p1 `2 by A13, A16, A69, A72, TOPREAL1:4;
p `1 <= p1 `1 by A13, A69, A123, A151, TOPREAL1:3;
then A153: p1 `1 = p `1 by A150, XXREAL_0:1;
p2 `2 <= p `2 by A13, A16, A69, A72, A151, TOPREAL1:4;
then p `2 = 1 by A13, A16, A69, A72, A152, XXREAL_0:1;
then p = |[(p1 `1),1]| by A153, EUCLID:53
.= p1 by A13, A16, EUCLID:53 ;
hence a in {p1} by TARSKI:def 1; :: thesis: verum
end;
A154: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {|[1,1]|} by A3, Lm26, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
|[0,1]| in LSeg (|[0,1]|,p2) by RLTOPSP1:68;
then A155: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) <> {} by Lm22, XBOOLE_0:def 4;
(LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) c= {|[0,1]|} by A66, Lm23, TOPREAL1:6, TOPREAL1:15, XBOOLE_1:26;
then A156: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2)) = {|[0,1]|} by A155, ZFMISC_1:33;
take P1 = LSeg (p1,p2); :: thesis: ex P2 being Element of K19( the carrier of (TOP-REAL 2)) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[1,1]|)) \/ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A157: p1 in LSeg (p1,|[1,1]|) by RLTOPSP1:68;
thus P1 is_an_arc_of p1,p2 by A1, TOPREAL1:9; :: thesis: ( P2 is_an_arc_of p1,p2 & P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
A158: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) = {} by TOPREAL1:19, XBOOLE_0:def 7;
(LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A66, Lm23, TOPREAL1:6, XBOOLE_1:26;
then A159: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)) = {} by A158, XBOOLE_1:3;
(((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) /\ (LSeg (|[0,1]|,p2)) = (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) /\ (LSeg (|[0,1]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= (((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,1]|,p2)))) \/ {|[0,1]|} by A156, XBOOLE_1:23
.= {|[0,1]|} by A141, A159 ;
then A160: (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)) is_an_arc_of |[1,1]|,p2 by A138, TOPREAL1:10;
(LSeg (p1,|[1,1]|)) /\ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) = ((LSeg (p1,|[1,1]|)) /\ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,1]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[1,1]|)) /\ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) by A132, XBOOLE_1:23
.= ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) by A145, XBOOLE_1:23
.= {|[1,1]|} by A131, A154, A142, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A160, TOPREAL1:11; :: thesis: ( P1 \/ P2 = R^2-unit_square & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = ((LSeg (p2,p1)) \/ (LSeg (p1,|[1,1]|))) \/ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2))) by XBOOLE_1:4
.= ((LSeg (|[0,1]|,p2)) \/ ((LSeg (p2,p1)) \/ (LSeg (p1,|[1,1]|)))) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) by XBOOLE_1:4
.= (LSeg (|[0,1]|,|[1,1]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) by A3, A66, TOPREAL1:7
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A161: 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 A161, XBOOLE_0:def 4;
then {p2} c= (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)) by ZFMISC_1:31;
then A162: (LSeg (p1,p2)) /\ (LSeg (|[0,1]|,p2)) = {p2} by A124, XBOOLE_0:def 10;
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then p1 in (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) by A157, XBOOLE_0:def 4;
then {p1} c= (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (p1,|[1,1]|)) = {p1} by A147, XBOOLE_0:def 10;
then A163: P1 /\ P2 = {p1} \/ ((LSeg (p1,p2)) /\ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,1]|,p2)))) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}) by A162, XBOOLE_1:23
.= {p1} \/ ((((LSeg (p1,p2)) /\ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}) by XBOOLE_1:23
.= {p1} \/ (((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})) by A146, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ (((LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2}) by XBOOLE_1:4 ;
A164: (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, A66, TOPREAL1:6, XBOOLE_1:26;
A165: now :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2}
per cases ( p2 = |[0,1]| or p2 <> |[0,1]| ) ;
suppose A166: p2 = |[0,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2}
p2 in LSeg (p1,p2) by RLTOPSP1:68;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) <> {} by A166, Lm22, XBOOLE_0:def 4;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {p2} by A164, A166, TOPREAL1:15, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2} by A163; :: thesis: verum
end;
suppose A167: p2 <> |[0,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2}
then {|[0,1]|} <> (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A164, TOPREAL1:15, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ {p2} by A163; :: thesis: verum
end;
end;
end;
A168: (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) c= {|[1,1]|} by A3, A66, TOPREAL1:6, TOPREAL1:18, XBOOLE_1:26;
now :: thesis: P1 /\ P2 = {p1,p2}
per cases ( p1 = |[1,1]| or p1 <> |[1,1]| ) ;
suppose A169: p1 = |[1,1]| ; :: thesis: P1 /\ P2 = {p1,p2}
p1 in LSeg (p1,p2) by RLTOPSP1:68;
then (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) <> {} by A169, Lm27, XBOOLE_0:def 4;
then (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {p1} by A168, A169, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A165, ENUMSET1:1; :: thesis: verum
end;
suppose A170: p1 <> |[1,1]| ; :: thesis: P1 /\ P2 = {p1,p2}
now :: thesis: not |[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|))
assume |[1,1]| in (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) ; :: thesis: contradiction
then |[1,1]| in LSeg (p2,p1) by XBOOLE_0:def 4;
then |[1,1]| `1 <= p1 `1 by A13, A69, A123, TOPREAL1:3;
then p1 `1 = 1 by A13, A14, Lm10, XXREAL_0:1;
hence contradiction by A13, A16, A170, EUCLID:53; :: thesis: verum
end;
then {|[1,1]|} <> (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) by ZFMISC_1:31;
then (LSeg (p1,p2)) /\ (LSeg (|[1,0]|,|[1,1]|)) = {} by A168, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A165, 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 A171: p2 in LSeg (|[0,0]|,|[1,0]|) ; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
|[0,0]| in LSeg (|[0,0]|,p2) by RLTOPSP1:68;
then A172: (LSeg (|[0,1]|,|[0,0]|)) /\ (LSeg (|[0,0]|,p2)) <> {} by Lm20, XBOOLE_0:def 4;
LSeg (|[0,0]|,p2) c= LSeg (|[0,0]|,|[1,0]|) by A171, Lm21, TOPREAL1:6;
then (LSeg (|[0,1]|,|[0,0]|)) /\ (LSeg (|[0,0]|,p2)) c= {|[0,0]|} by TOPREAL1:17, XBOOLE_1:27;
then (LSeg (|[0,1]|,|[0,0]|)) /\ (LSeg (|[0,0]|,p2)) = {|[0,0]|} by A172, ZFMISC_1:33;
then A173: (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,p2)) is_an_arc_of |[0,1]|,p2 by Lm5, Lm7, TOPREAL1:12;
LSeg (p2,|[0,0]|) c= LSeg (|[0,0]|,|[1,0]|) by A171, Lm21, TOPREAL1:6;
then A174: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A11, Lm2, XBOOLE_1:3, XBOOLE_1:27;
|[1,0]| in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
then A175: |[1,0]| in (LSeg (|[1,1]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) by Lm25, XBOOLE_0:def 4;
LSeg (|[1,0]|,p2) c= LSeg (|[0,0]|,|[1,0]|) by A171, Lm24, TOPREAL1:6;
then (LSeg (|[1,1]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by XBOOLE_1:27;
then (LSeg (|[1,1]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) = {|[1,0]|} by A175, TOPREAL1:16, ZFMISC_1:33;
then A176: (LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,0]|,p2)) is_an_arc_of |[1,1]|,p2 by Lm9, Lm11, TOPREAL1:12;
take P1 = ((LSeg (p1,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A177: (LSeg (p1,|[1,1]|)) \/ (LSeg (p1,|[0,1]|)) = LSeg (|[0,1]|,|[1,1]|) by A3, TOPREAL1:5;
A178: LSeg (p2,|[1,0]|) c= LSeg (|[0,0]|,|[1,0]|) by A171, Lm24, TOPREAL1:6;
then A179: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A8, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A180: (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A171, Lm21, TOPREAL1:6, XBOOLE_1:26;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) by A3, Lm26, TOPREAL1:6, XBOOLE_1:26;
then A181: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A180, Lm2, XBOOLE_1:1, XBOOLE_1:3;
A182: (LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,1]|)) = {} by A11, A178, Lm2, XBOOLE_1:3, XBOOLE_1:27;
A183: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,p2)) = {p2} by A171, TOPREAL1:8;
(LSeg (p1,|[1,1]|)) /\ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,0]|,p2))) = ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= {|[1,1]|} by A6, A10, A179, ZFMISC_1:33 ;
then (LSeg (p1,|[1,1]|)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,0]|,p2))) is_an_arc_of p1,p2 by A176, 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} )
A184: ex q2 being Point of (TOP-REAL 2) st
( q2 = p2 & q2 `1 <= 1 & q2 `1 >= 0 & q2 `2 = 0 ) by A171, TOPREAL1:13;
(LSeg (p1,|[0,1]|)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,p2))) = ((LSeg (|[0,1]|,p1)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,p2))) by XBOOLE_1:23
.= {|[0,1]|} by A7, A5, A174, TOPREAL1:15, ZFMISC_1:33 ;
then (LSeg (p1,|[0,1]|)) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,p2))) is_an_arc_of p1,p2 by A173, 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} )
(LSeg (|[1,0]|,p2)) \/ (LSeg (|[0,0]|,p2)) = LSeg (|[0,0]|,|[1,0]|) by A171, TOPREAL1:5;
hence R^2-unit_square = (LSeg (|[0,1]|,|[1,1]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ ((LSeg (|[1,0]|,p2)) \/ (LSeg (|[0,0]|,p2)))) \/ (LSeg (|[0,0]|,|[0,1]|))) by TOPREAL1:def 2, XBOOLE_1:4
.= (LSeg (|[0,1]|,|[1,1]|)) \/ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,0]|,p2))) \/ (LSeg (|[0,0]|,p2))) \/ (LSeg (|[0,0]|,|[0,1]|))) by XBOOLE_1:4
.= (LSeg (|[0,1]|,|[1,1]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:4
.= (LSeg (p1,|[1,1]|)) \/ ((((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,p2)))) \/ (LSeg (p1,|[0,1]|))) by A177, XBOOLE_1:4
.= (LSeg (p1,|[1,1]|)) \/ (((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,0]|,p2))) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,p2))) \/ (LSeg (p1,|[0,1]|)))) by XBOOLE_1:4
.= ((LSeg (p1,|[1,1]|)) \/ ((LSeg (|[1,0]|,|[1,1]|)) \/ (LSeg (|[1,0]|,p2)))) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,p2))) \/ (LSeg (p1,|[0,1]|))) by XBOOLE_1:4
.= (((LSeg (p1,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) \/ (LSeg (|[1,0]|,p2))) \/ ((LSeg (p1,|[0,1]|)) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:4
.= P1 \/ P2 by XBOOLE_1:4 ;
:: thesis: P1 /\ P2 = {p1,p2}
A185: (LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[0,1]|)) = {p1} by A3, TOPREAL1:8;
A186: P1 /\ P2 = (((LSeg (p1,|[1,1]|)) \/ (LSeg (|[1,0]|,|[1,1]|))) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:23
.= (((LSeg (p1,|[1,1]|)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:23
.= ((((LSeg (p1,|[1,1]|)) /\ ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:23
.= ((((LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))) by A181, XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,0]|,|[1,1]|)) /\ ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))) by A185, XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ ((LSeg (|[1,0]|,p2)) /\ (((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|))) \/ (LSeg (|[0,0]|,p2)))) by XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}) by A183, Lm3, XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ ((((LSeg (|[1,0]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}) by XBOOLE_1:23
.= (({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2))))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2}) by A182 ;
A187: now :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
per cases ( p1 = |[0,1]| or p1 = |[1,1]| or ( p1 <> |[1,1]| & p1 <> |[0,1]| ) ) ;
suppose A188: p1 = |[0,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
then (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (p1,|[0,1]|)) = (LSeg (|[1,0]|,|[1,1]|)) /\ {|[0,1]|} by RLTOPSP1:70
.= {} by Lm1, Lm15 ;
hence P1 /\ P2 = ({p1} \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2}) by A186, A188, TOPREAL1:15; :: thesis: verum
end;
suppose A189: p1 = |[1,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
then (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {|[1,1]|} /\ (LSeg (|[0,0]|,|[0,1]|)) by RLTOPSP1:70
.= {} by Lm1, Lm18 ;
hence P1 /\ P2 = (({p1} \/ {p1}) \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2}) by A186, A189, TOPREAL1:18, XBOOLE_1:4
.= ({p1} \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2}) ;
:: thesis: verum
end;
suppose A190: ( p1 <> |[1,1]| & p1 <> |[0,1]| ) ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2})
then A192: {|[1,1]|} <> (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (p1,|[0,1]|)) by ZFMISC_1:31;
(LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (p1,|[0,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A3, Lm23, TOPREAL1:6, XBOOLE_1:26;
then A193: (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (p1,|[0,1]|)) = {} by A192, TOPREAL1:18, ZFMISC_1:33;
then A195: {|[0,1]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A3, Lm26, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A195, TOPREAL1:15, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ((LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)))) \/ (((LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ {p2}) by A186, A193; :: thesis: verum
end;
end;
end;
now :: thesis: P1 /\ P2 = {p1,p2}
per cases ( p2 = |[0,0]| or p2 = |[1,0]| or ( p2 <> |[1,0]| & p2 <> |[0,0]| ) ) ;
suppose A196: p2 = |[0,0]| ; :: thesis: P1 /\ P2 = {p1,p2}
then (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = (LSeg (|[1,0]|,|[1,1]|)) /\ {|[0,0]|} by RLTOPSP1:70
.= {} by Lm1, Lm12 ;
hence P1 /\ P2 = {p1,p2} by A187, A196, ENUMSET1:1, TOPREAL1:17; :: thesis: verum
end;
suppose A197: p2 = |[1,0]| ; :: thesis: P1 /\ P2 = {p1,p2}
then (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {|[1,0]|} /\ (LSeg (|[0,0]|,|[0,1]|)) by RLTOPSP1:70
.= {} by Lm1, Lm16 ;
hence P1 /\ P2 = {p1} \/ ({p2} \/ {p2}) by A187, A197, TOPREAL1:16, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:1 ;
:: thesis: verum
end;
suppose A198: ( p2 <> |[1,0]| & p2 <> |[0,0]| ) ; :: thesis: P1 /\ P2 = {p1,p2}
then A200: {|[0,0]|} <> (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
(LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A171, Lm24, TOPREAL1:6, XBOOLE_1:26;
then A201: (LSeg (|[1,0]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A200, TOPREAL1:17, ZFMISC_1:33;
then A203: {|[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 A171, Lm21, TOPREAL1:6, XBOOLE_1:26;
then (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,p2)) = {} by A203, TOPREAL1:16, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A187, A201, ENUMSET1:1; :: thesis: verum
end;
end;
end;
hence P1 /\ P2 = {p1,p2} ; :: thesis: verum
end;
suppose A204: p2 in LSeg (|[1,0]|,|[1,1]|) ; :: thesis: ex P1, P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
then A205: LSeg (|[1,1]|,p2) c= LSeg (|[1,0]|,|[1,1]|) by Lm27, TOPREAL1:6;
LSeg (p1,|[1,1]|) c= LSeg (|[0,1]|,|[1,1]|) by A3, Lm26, TOPREAL1:6;
then A206: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[1,0]|,|[1,1]|)) by A205, XBOOLE_1:27;
take P1 = (LSeg (p1,|[1,1]|)) \/ (LSeg (|[1,1]|,p2)); :: thesis: ex P2 being non empty Subset of (TOP-REAL 2) st
( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
take P2 = (LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))); :: thesis: ( P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A207: |[1,1]| in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
|[1,0]| in LSeg (|[1,0]|,p2) by RLTOPSP1:68;
then A208: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) <> {} by Lm24, XBOOLE_0:def 4;
|[1,1]| in LSeg (p1,|[1,1]|) by RLTOPSP1:68;
then (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) <> {} by A207, XBOOLE_0:def 4;
then A209: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,1]|,p2)) = {|[1,1]|} by A206, TOPREAL1:18, ZFMISC_1:33;
( p1 <> |[1,1]| or |[1,1]| <> p2 ) by A1;
hence P1 is_an_arc_of p1,p2 by A209, TOPREAL1:12; :: thesis: ( P2 is_an_arc_of p1,p2 & R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
A210: LSeg (|[0,1]|,|[1,1]|) = (LSeg (p1,|[1,1]|)) \/ (LSeg (p1,|[0,1]|)) by A3, TOPREAL1:5;
A211: LSeg (|[0,0]|,|[1,0]|) is_an_arc_of |[0,0]|,|[1,0]| by Lm4, Lm8, TOPREAL1:9;
LSeg (|[0,0]|,|[0,1]|) is_an_arc_of |[0,1]|,|[0,0]| by Lm5, Lm7, TOPREAL1:9;
then A212: (LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)) is_an_arc_of |[0,1]|,|[1,0]| by A211, TOPREAL1:2, TOPREAL1:17;
A213: (LSeg (|[1,1]|,p2)) /\ (LSeg (|[1,0]|,p2)) = {p2} by A204, TOPREAL1:8;
A214: LSeg (|[1,0]|,|[1,1]|) = (LSeg (|[1,0]|,p2)) \/ (LSeg (|[1,1]|,p2)) by A204, TOPREAL1:5;
A215: LSeg (|[1,0]|,p2) c= LSeg (|[1,0]|,|[1,1]|) by A204, Lm25, TOPREAL1:6;
then A216: (LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[1,0]|} by TOPREAL1:16, XBOOLE_1:27;
A217: ex q being Point of (TOP-REAL 2) st
( q = p2 & q `1 = 1 & q `2 <= 1 & q `2 >= 0 ) by A204, TOPREAL1:13;
now :: thesis: not |[1,1]| in (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2))
A218: |[1,0]| `2 <= p2 `2 by A217, EUCLID:52;
assume A219: |[1,1]| in (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) ; :: thesis: contradiction
then A220: |[1,1]| in LSeg (|[0,1]|,p1) by XBOOLE_0:def 4;
|[1,1]| in LSeg (|[1,0]|,p2) by A219, XBOOLE_0:def 4;
then |[1,1]| `2 <= p2 `2 by A218, TOPREAL1:4;
then A221: |[1,1]| `2 = p2 `2 by A217, Lm11, XXREAL_0:1;
|[0,1]| `1 <= p1 `1 by A13, A15, EUCLID:52;
then |[1,1]| `1 <= p1 `1 by A220, TOPREAL1:3;
then |[1,1]| `1 = p1 `1 by A13, A14, Lm10, XXREAL_0:1;
then p1 = |[(|[1,1]| `1),(|[1,1]| `2)]| by A13, A16, Lm11, EUCLID:53
.= p2 by A217, A221, Lm10, EUCLID:53 ;
hence contradiction by A1; :: thesis: verum
end;
then A222: {|[1,1]|} <> (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) by ZFMISC_1:31;
A223: (LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A215, Lm3, XBOOLE_1:3, XBOOLE_1:26;
((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) /\ (LSeg (|[1,0]|,p2)) = ((LSeg (|[0,0]|,|[0,1]|)) /\ (LSeg (|[1,0]|,p2))) \/ ((LSeg (|[0,0]|,|[1,0]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= {|[1,0]|} by A223, A216, A208, ZFMISC_1:33 ;
then A224: ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2)) is_an_arc_of |[0,1]|,p2 by A212, TOPREAL1:10;
A225: LSeg (p2,|[1,1]|) c= LSeg (|[1,0]|,|[1,1]|) by A204, Lm27, TOPREAL1:6;
then A226: (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by Lm3, XBOOLE_1:3, XBOOLE_1:27;
(LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[1,1]|} by A11, A215, TOPREAL1:18, XBOOLE_1:27;
then A227: (LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A222, ZFMISC_1:33;
(LSeg (p1,|[0,1]|)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))) = ((LSeg (p1,|[0,1]|)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[1,0]|,p2))) by XBOOLE_1:23
.= ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[0,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|))) by A227, XBOOLE_1:23
.= {|[0,1]|} by A12, A7, A5, TOPREAL1:15, ZFMISC_1:33 ;
hence P2 is_an_arc_of p1,p2 by A224, TOPREAL1:11; :: thesis: ( R^2-unit_square = P1 \/ P2 & P1 /\ P2 = {p1,p2} )
thus P1 \/ P2 = (LSeg (|[1,1]|,p2)) \/ ((LSeg (p1,|[1,1]|)) \/ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:4
.= ((LSeg (|[0,1]|,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2)))) \/ (LSeg (|[1,1]|,p2)) by A210, XBOOLE_1:4
.= (LSeg (|[0,1]|,|[1,1]|)) \/ ((((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))) \/ (LSeg (|[1,1]|,p2))) by XBOOLE_1:4
.= (LSeg (|[0,1]|,|[1,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ ((LSeg (|[1,0]|,p2)) \/ (LSeg (|[1,1]|,p2)))) by XBOOLE_1:4
.= (LSeg (|[0,1]|,|[1,1]|)) \/ ((LSeg (|[0,0]|,|[0,1]|)) \/ ((LSeg (|[0,0]|,|[1,0]|)) \/ (LSeg (|[1,0]|,|[1,1]|)))) by A214, XBOOLE_1:4
.= R^2-unit_square by TOPREAL1:def 2, XBOOLE_1:4 ; :: thesis: P1 /\ P2 = {p1,p2}
A228: {p1} = (LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[0,1]|)) by A3, TOPREAL1:8;
A229: P1 /\ P2 = ((LSeg (p1,|[1,1]|)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:23
.= (((LSeg (p1,|[1,1]|)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,1]|)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))))) by A228, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))))) \/ ((LSeg (|[1,1]|,p2)) /\ ((LSeg (p1,|[0,1]|)) \/ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ ((LSeg (|[1,1]|,p2)) /\ (((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|))) \/ (LSeg (|[1,0]|,p2))))) by XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ (((LSeg (|[1,1]|,p2)) /\ ((LSeg (|[0,0]|,|[0,1]|)) \/ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2})) by A213, XBOOLE_1:23
.= ({p1} \/ ((((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ ((((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)))) \/ {p2})) by XBOOLE_1:23
.= ({p1} \/ (((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|))) \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2))))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|))) \/ {p2})) by A9, A226 ;
A230: now :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2})
per cases ( p2 = |[1,0]| or p2 = |[1,1]| or ( p2 <> |[1,1]| & p2 <> |[1,0]| ) ) ;
suppose A231: p2 = |[1,0]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2})
then A232: not p2 in LSeg (p1,|[1,1]|) by A8, Lm7, Lm9, Lm11, TOPREAL1:4;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) = (LSeg (p1,|[1,1]|)) /\ {p2} by A231, RLTOPSP1:70
.= {} by A232, Lm1 ;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2}) by A229, A231, TOPREAL1:16; :: thesis: verum
end;
suppose A233: p2 = |[1,1]| ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2})
then p2 in LSeg (p1,|[1,1]|) by RLTOPSP1:68;
then A234: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) <> {} by A233, Lm27, XBOOLE_0:def 4;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) c= {p2} by A8, A233, TOPREAL1:18, XBOOLE_1:27;
then A235: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) = {p2} by A234, ZFMISC_1:33;
(LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {|[1,1]|} /\ (LSeg (|[0,0]|,|[1,0]|)) by A233, RLTOPSP1:70
.= {} by Lm1, Lm19 ;
hence P1 /\ P2 = (({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ {p2}) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2}) by A229, A235, XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ ((((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2}) \/ {p2}) by XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ ({p2} \/ {p2})) by XBOOLE_1:4
.= ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2}) ;
:: thesis: verum
end;
suppose A236: ( p2 <> |[1,1]| & p2 <> |[1,0]| ) ; :: thesis: P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2})
then A238: {|[1,1]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) by ZFMISC_1:31;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) c= {|[1,1]|} by A8, A215, TOPREAL1:18, XBOOLE_1:27;
then A239: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[1,0]|,p2)) = {} by A238, ZFMISC_1:33;
then A241: {|[1,0]|} <> (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) by ZFMISC_1:31;
(LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[1,0]|)) by A225, XBOOLE_1:27;
then (LSeg (|[1,1]|,p2)) /\ (LSeg (|[0,0]|,|[1,0]|)) = {} by A241, TOPREAL1:16, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ ((LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)))) \/ (((LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))) \/ {p2}) by A229, A239; :: thesis: verum
end;
end;
end;
now :: thesis: P1 /\ P2 = {p1,p2}
per cases ( p1 = |[0,1]| or p1 = |[1,1]| or ( p1 <> |[1,1]| & p1 <> |[0,1]| ) ) ;
suppose A242: p1 = |[0,1]| ; :: thesis: P1 /\ P2 = {p1,p2}
then A243: (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|)) = (LSeg (|[1,1]|,p2)) /\ {p1} by RLTOPSP1:70;
not p1 in LSeg (|[1,1]|,p2) by A225, A242, Lm6, Lm8, Lm10, TOPREAL1:3;
then (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|)) = {} by A243, Lm1;
hence P1 /\ P2 = {p1,p2} by A230, A242, ENUMSET1:1, TOPREAL1:15; :: thesis: verum
end;
suppose A244: p1 = |[1,1]| ; :: thesis: P1 /\ P2 = {p1,p2}
|[1,1]| in LSeg (|[1,1]|,p2) by RLTOPSP1:68;
then A245: (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|)) <> {} by A244, Lm26, XBOOLE_0:def 4;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {p1} /\ (LSeg (|[0,0]|,|[0,1]|)) by A244, RLTOPSP1:70;
then A246: (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A244, Lm1, Lm18;
(LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A11, A225, XBOOLE_1:27;
then (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|)) = {p1} by A244, A245, TOPREAL1:18, ZFMISC_1:33;
hence P1 /\ P2 = ({p1} \/ {p1}) \/ {p2} by A230, A246, XBOOLE_1:4
.= {p1,p2} by ENUMSET1:1 ;
:: thesis: verum
end;
suppose A247: ( p1 <> |[1,1]| & p1 <> |[0,1]| ) ; :: thesis: P1 /\ P2 = {p1,p2}
now :: thesis: not |[1,1]| in (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|))
assume |[1,1]| in (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|)) ; :: thesis: contradiction
then A248: |[1,1]| in LSeg (|[0,1]|,p1) by XBOOLE_0:def 4;
|[0,1]| `1 <= p1 `1 by A13, A15, EUCLID:52;
then |[1,1]| `1 <= p1 `1 by A248, TOPREAL1:3;
then p1 `1 = 1 by A13, A14, Lm10, XXREAL_0:1;
hence contradiction by A13, A16, A247, EUCLID:53; :: thesis: verum
end;
then A249: {|[1,1]|} <> (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|)) by ZFMISC_1:31;
(LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|)) c= (LSeg (|[1,0]|,|[1,1]|)) /\ (LSeg (|[0,1]|,|[1,1]|)) by A11, A225, XBOOLE_1:27;
then A250: (LSeg (|[1,1]|,p2)) /\ (LSeg (p1,|[0,1]|)) = {} by A249, TOPREAL1:18, ZFMISC_1:33;
then A252: {|[0,1]|} <> (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by ZFMISC_1:31;
(LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) c= (LSeg (|[0,1]|,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) by A8, XBOOLE_1:27;
then (LSeg (p1,|[1,1]|)) /\ (LSeg (|[0,0]|,|[0,1]|)) = {} by A252, TOPREAL1:15, ZFMISC_1:33;
hence P1 /\ P2 = {p1,p2} by A230, A250, ENUMSET1:1; :: thesis: verum
end;
end;
end;
hence P1 /\ P2 = {p1,p2} ; :: thesis: verum
end;
end;