let s1, t1, s2, t2 be Real; :: thesis:
let P, P1, P2 be Subset of (TOP-REAL 2); :: thesis:
assume that
A1: ( s1 < s2 & t1 < t2 ) and
A2: P = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) } and
A3: P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } and
A4: P2 = { pc where pc is Point of (TOP-REAL 2) : ( not s1 <= pc `1 or not pc `1 <= s2 or not t1 <= pc `2 or not pc `2 <= t2 ) } ; :: thesis:

now

let x be set ; :: thesis:
assume A5: x in P ` ; :: thesis:
then A6: ( x in [#] (TOP-REAL 2) & not x in P ) by XBOOLE_0:def 5;
reconsider pd = x as Point of (TOP-REAL 2) by A5;
( not ( pd `1 = s1 & pd `2 <= t2 & pd `2 >= t1 ) & not ( pd `1 <= s2 & pd `1 >= s1 & pd `2 = t2 ) & not ( pd `1 <= s2 & pd `1 >= s1 & pd `2 = t1 ) & not ( pd `1 = s2 & pd `2 <= t2 & pd `2 >= t1 ) ) by A2, A6;
then ( ( s1 < pd `1 & pd `1 < s2 & t1 < pd `2 & pd `2 < t2 ) or not s1 <= pd `1 or not pd `1 <= s2 or not t1 <= pd `2 or not pd `2 <= t2 ) by XXREAL_0:1;
then ( x in P1 or x in P2 ) by A3, A4;
hence x in P1 \/ P2 by XBOOLE_0:def 3; :: thesis:

end;

then A7: P ` c= P1 \/ P2 by TARSKI:def 3;

now

let x be set ; :: thesis:
assume A8: x in P1 \/ P2 ; :: thesis:

now

per cases by A8, XBOOLE_0:def 3;

suppose A9: x in P1 ; :: thesis:

then A10: ex pa being Point of (TOP-REAL 2) st
( pa = x & s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) by A3;

now

assume x in P ; :: thesis:
then ex pb being Point of (TOP-REAL 2) st
( pb = x & ( ( pb `1 = s1 & pb `2 <= t2 & pb `2 >= t1 ) or ( pb `1 <= s2 & pb `1 >= s1 & pb `2 = t2 ) or ( pb `1 <= s2 & pb `1 >= s1 & pb `2 = t1 ) or ( pb `1 = s2 & pb `2 <= t2 & pb `2 >= t1 ) ) ) by A2;
hence contradiction by A10; :: thesis:

end;

hence x in P ` by A9, SUBSET_1:50; :: thesis:

end;

suppose x in P2 ; :: thesis:

then consider pc being Point of (TOP-REAL 2) such that
A11: pc = x and
A12: ( not s1 <= pc `1 or not pc `1 <= s2 or not t1 <= pc `2 or not pc `2 <= t2 ) by A4;

now

assume pc in P ; :: thesis:
then ex p being Point of (TOP-REAL 2) st
( p = pc & ( ( p `1 = s1 & p `2 <= t2 & p `2 >= t1 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t2 ) or ( p `1 <= s2 & p `1 >= s1 & p `2 = t1 ) or ( p `1 = s2 & p `2 <= t2 & p `2 >= t1 ) ) ) by A2;
hence contradiction by A1, A12; :: thesis:

end;

hence x in P ` by A11, SUBSET_1:50; :: thesis:

end;

hence x in P ` ; :: thesis:

end;

then P1 \/ P2 c= P ` by TARSKI:def 3;
hence A13: P ` = P1 \/ P2 by A7, XBOOLE_0:def 10; :: thesis:
set s3 = (s1 + s2) / 2;
set t3 = (t1 + t2) / 2;
( s1 + s1 < s1 + s2 & t1 + t1 < t1 + t2 ) by A1, XREAL_1:8;
then A14: ( (s1 + s1) / 2 < (s1 + s2) / 2 & (t1 + t1) / 2 < (t1 + t2) / 2 ) by XREAL_1:76;
( s1 + s2 < s2 + s2 & t1 + t2 < t2 + t2 ) by A1, XREAL_1:8;
then A15: ( (s1 + s2) / 2 < (s2 + s2) / 2 & (t1 + t2) / 2 < (t2 + t2) / 2 ) by XREAL_1:76;
set pp = |[((s1 + s2) / 2),((t1 + t2) / 2)]|;
( |[((s1 + s2) / 2),((t1 + t2) / 2)]| `1 = (s1 + s2) / 2 & |[((s1 + s2) / 2),((t1 + t2) / 2)]| `2 = (t1 + t2) / 2 ) by EUCLID:56;
then A16: |[((s1 + s2) / 2),((t1 + t2) / 2)]| in { pp2 where pp2 is Point of (TOP-REAL 2) : ( s1 < pp2 `1 & pp2 `1 < s2 & t1 < pp2 `2 & pp2 `2 < t2 ) } by A14, A15;
then consider x being set such that
A17: x in P1 by A3;
thus P ` <> {} by A13, A17; :: thesis:
set P' = P ` ;
P1 misses P2 by A3, A4, Th40;
hence A18: P1 /\ P2 = {} by XBOOLE_0:def 7; :: according to XBOOLE_0:def 7 :: thesis:

now

let P1A, P2B be Subset of ((TOP-REAL 2) | (P ` )); :: thesis:
assume A19: ( P1A = P1 & P2B = P2 ) ; :: thesis:
P1 is connected by A3, Th36;
then A20: P1A is connected by A19, CONNSP_1:24;
A21: P2 is connected by A4, Th37;
A22: P2 = { |[sa,ta]| where sa, ta is Real : ( not s1 <= sa or not sa <= s2 or not t1 <= ta or not ta <= t2 ) } by A4, Th33;
reconsider A0 = { |[s3a,t3a]| where s3a, t3a is Real : s3a < s1 } as Subset of (TOP-REAL 2) by Lm2, XX;
reconsider A1 = { |[s4,t4]| where s4, t4 is Real : t4 < t1 } as Subset of (TOP-REAL 2) by Lm3, XX;
reconsider A2 = { |[s5,t5]| where s5, t5 is Real : s2 < s5 } as Subset of (TOP-REAL 2) by Lm4, XX;
reconsider A3 = { |[s6,t6]| where s6, t6 is Real : t2 < t6 } as Subset of (TOP-REAL 2) by Lm5, XX;
A23: P2 = ((A0 \/ A1) \/ A2) \/ A3 by A22, Th13;
t2 + 1 > t2 by XREAL_1:31;
then |[(s2 + 1),(t2 + 1)]| in A3 ;
then A24: P2B <> {} by A19, A23;
A25: P2B is connected by A19, A21, CONNSP_1:24;
A26: for CP being Subset of ((TOP-REAL 2) | (P ` )) st CP is connected & P1A c= CP holds
P1A = CP

proof

let CP be Subset of ((TOP-REAL 2) | (P ` )); :: thesis:
assume CP is connected ; :: thesis:
then A27: ((TOP-REAL 2) | (P ` )) | CP is connected by CONNSP_1:def 3;

now

assume A28: P1A c= CP ; :: thesis:
P1A /\ CP c= the carrier of (((TOP-REAL 2) | (P ` )) | CP)

proof

P1A /\ CP c= CP by XBOOLE_1:17;
hence P1A /\ CP c= the carrier of (((TOP-REAL 2) | (P ` )) | CP) by PRE_TOPC:29; :: thesis:

end;

then reconsider AP = P1A /\ CP as Subset of (((TOP-REAL 2) | (P ` )) | CP) ;
A29: P1 /\ (P ` ) = P1A by A13, A19, XBOOLE_1:21;
P1 is open by A3, Th38;
then A30: P1 in the topology of (TOP-REAL 2) by PRE_TOPC:def 5;
A31: P ` = [#] ((TOP-REAL 2) | (P ` )) by PRE_TOPC:def 10;
P1 /\ ([#] ((TOP-REAL 2) | (P ` ))) = P1A by A29, PRE_TOPC:def 10;
then A32: P1A in the topology of ((TOP-REAL 2) | (P ` )) by A30, PRE_TOPC:def 9;
A33: CP = [#] (((TOP-REAL 2) | (P ` )) | CP) by PRE_TOPC:def 10;
A34: AP <> {} (((TOP-REAL 2) | (P ` )) | CP) by A3, A16, A19, A28, XBOOLE_1:28;
AP in the topology of (((TOP-REAL 2) | (P ` )) | CP) by A32, A33, PRE_TOPC:def 9;
then A35: AP is open by PRE_TOPC:def 5;
P2B /\ CP c= the carrier of (((TOP-REAL 2) | (P ` )) | CP)

proof

P2B /\ CP c= CP by XBOOLE_1:17;
hence P2B /\ CP c= the carrier of (((TOP-REAL 2) | (P ` )) | CP) by PRE_TOPC:29; :: thesis:

end;

then reconsider BP = P2B /\ CP as Subset of (((TOP-REAL 2) | (P ` )) | CP) ;
A36: P2 /\ (P ` ) = P2B by A13, A19, XBOOLE_1:21;
P2 is open by A4, Th39;
then A37: P2 in the topology of (TOP-REAL 2) by PRE_TOPC:def 5;
P2 /\ ([#] ((TOP-REAL 2) | (P ` ))) = P2B by A36, PRE_TOPC:def 10;
then A38: P2B in the topology of ((TOP-REAL 2) | (P ` )) by A37, PRE_TOPC:def 9;
CP = [#] (((TOP-REAL 2) | (P ` )) | CP) by PRE_TOPC:def 10;
then BP in the topology of (((TOP-REAL 2) | (P ` )) | CP) by A38, PRE_TOPC:def 9;
then A39: BP is open by PRE_TOPC:def 5;
A40: CP = (P1A \/ P2B) /\ CP by A13, A19, A31, XBOOLE_1:28
.= AP \/ BP by XBOOLE_1:23 ;

now

assume A41: BP <> {} ; :: thesis:
A42: AP /\ BP = (P1A /\ (P2B /\ CP)) /\ CP by XBOOLE_1:16
.= ((P1A /\ P2B) /\ CP) /\ CP by XBOOLE_1:16
.= (P1A /\ P2B) /\ (CP /\ CP) by XBOOLE_1:16
.= (P1A /\ P2B) /\ CP ;
P1 misses P2 by A3, A4, Th40;
then P1 /\ P2 = {} by XBOOLE_0:def 7;
then AP misses BP by A19, A42, XBOOLE_0:def 7;
hence contradiction by A27, A33, A34, A35, A39, A40, A41, CONNSP_1:12; :: thesis:

end;

hence ( not P1A c= CP or P1A = CP ) by A40, XBOOLE_1:28; :: thesis:

end;

hence ( not P1A c= CP or P1A = CP ) ; :: thesis:

end;

hence P1A is_a_component_of (TOP-REAL 2) | (P ` ) by A20, CONNSP_1:def 5; :: thesis:
for CP being Subset of ((TOP-REAL 2) | (P ` )) st CP is connected & P2B c= CP holds
P2B = CP

proof

let CP be Subset of ((TOP-REAL 2) | (P ` )); :: thesis:
assume CP is connected ; :: thesis:
then A43: ((TOP-REAL 2) | (P ` )) | CP is connected by CONNSP_1:def 3;
assume A44: P2B c= CP ; :: thesis:
P2B /\ CP c= the carrier of (((TOP-REAL 2) | (P ` )) | CP)

proof

P2B /\ CP c= CP by XBOOLE_1:17;
hence P2B /\ CP c= the carrier of (((TOP-REAL 2) | (P ` )) | CP) by PRE_TOPC:29; :: thesis:

end;

then reconsider BP = P2B /\ CP as Subset of (((TOP-REAL 2) | (P ` )) | CP) ;
A45: P2 /\ (P ` ) = P2B by A13, A19, XBOOLE_1:21;
P2 is open by A4, Th39;
then A46: P2 in the topology of (TOP-REAL 2) by PRE_TOPC:def 5;
A47: P ` = [#] ((TOP-REAL 2) | (P ` )) by PRE_TOPC:def 10;
P2 /\ ([#] ((TOP-REAL 2) | (P ` ))) = P2B by A45, PRE_TOPC:def 10;
then A48: P2B in the topology of ((TOP-REAL 2) | (P ` )) by A46, PRE_TOPC:def 9;
A49: CP = [#] (((TOP-REAL 2) | (P ` )) | CP) by PRE_TOPC:def 10;
A50: BP <> {} (((TOP-REAL 2) | (P ` )) | CP) by A24, A44, XBOOLE_1:28;
BP in the topology of (((TOP-REAL 2) | (P ` )) | CP) by A48, A49, PRE_TOPC:def 9;
then A51: BP is open by PRE_TOPC:def 5;
P1A /\ CP c= the carrier of (((TOP-REAL 2) | (P ` )) | CP)

proof

P1A /\ CP c= CP by XBOOLE_1:17;
hence P1A /\ CP c= the carrier of (((TOP-REAL 2) | (P ` )) | CP) by PRE_TOPC:29; :: thesis:

end;

then reconsider AP = P1A /\ CP as Subset of (((TOP-REAL 2) | (P ` )) | CP) ;
A52: P1 /\ (P ` ) = P1A by A13, A19, XBOOLE_1:21;
P1 is open by A3, Th38;
then A53: P1 in the topology of (TOP-REAL 2) by PRE_TOPC:def 5;
P1 /\ ([#] ((TOP-REAL 2) | (P ` ))) = P1A by A52, PRE_TOPC:def 10;
then A54: P1A in the topology of ((TOP-REAL 2) | (P ` )) by A53, PRE_TOPC:def 9;
CP = [#] (((TOP-REAL 2) | (P ` )) | CP) by PRE_TOPC:def 10;
then AP in the topology of (((TOP-REAL 2) | (P ` )) | CP) by A54, PRE_TOPC:def 9;
then A55: AP is open by PRE_TOPC:def 5;
A56: CP = (P1A \/ P2B) /\ CP by A13, A19, A47, XBOOLE_1:28
.= AP \/ BP by XBOOLE_1:23 ;

now

assume A57: AP <> {} ; :: thesis:
AP /\ BP = (P1A /\ (P2B /\ CP)) /\ CP by XBOOLE_1:16
.= ((P1A /\ P2B) /\ CP) /\ CP by XBOOLE_1:16
.= (P1A /\ P2B) /\ (CP /\ CP) by XBOOLE_1:16
.= (P1A /\ P2B) /\ CP ;
then AP misses BP by A18, A19, XBOOLE_0:def 7;
hence contradiction by A43, A49, A50, A51, A55, A56, A57, CONNSP_1:12; :: thesis:

end;

hence P2B = CP by A44, A56, XBOOLE_1:28; :: thesis:

end;

hence ( P1A is_a_component_of (TOP-REAL 2) | (P ` ) & P2B is_a_component_of (TOP-REAL 2) | (P ` ) ) by A20, A25, A26, CONNSP_1:def 5; :: thesis:

end;

hence for P1A, P2B being Subset of ((TOP-REAL 2) | (P ` )) st P1A = P1 & P2B = P2 holds
( P1A is_a_component_of (TOP-REAL 2) | (P ` ) & P2B is_a_component_of (TOP-REAL 2) | (P ` ) ) ; :: thesis: