let s1, t1, s2, t2 be Real; :: thesis: for P, P1, P2 being Subset of (TOP-REAL 2) st s1 < s2 & t1 < t2 & 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 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } holds
( P ` = P1 \/ P2 & P ` <> {} & P1 misses P2 & ( for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds
( P1A is a_component & P2B is a_component ) ) )
let P, P1, P2 be Subset of (TOP-REAL 2); :: thesis: ( s1 < s2 & t1 < t2 & 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 ) ) } & P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } & P2 = { pb where pb is Point of (TOP-REAL 2) : ( not s1 <= pb `1 or not pb `1 <= s2 or not t1 <= pb `2 or not pb `2 <= t2 ) } implies ( P ` = P1 \/ P2 & P ` <> {} & P1 misses P2 & ( for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds
( P1A is a_component & P2B is a_component ) ) ) )
assume that
A1: s1 < s2 and
A2: t1 < t2 and
A3: 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
A4: P1 = { pa where pa is Point of (TOP-REAL 2) : ( s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) } and
A5: 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: ( P ` = P1 \/ P2 & P ` <> {} & P1 misses P2 & ( for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds
( P1A is a_component & P2B is a_component ) ) )
now :: thesis: for x being object st x in P ` holds
x in P1 \/ P2
let x be object ; :: thesis: ( x in P ` implies x in P1 \/ P2 )
assume A6: x in P ` ; :: thesis: x in P1 \/ P2
then A7: not x in P by XBOOLE_0:def 5;
reconsider pd = x as Point of (TOP-REAL 2) by A6;
( 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 A3, A7;
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 A4, A5;
hence x in P1 \/ P2 by XBOOLE_0:def 3; :: thesis: verum
end;
then A8: P ` c= P1 \/ P2 ;
now :: thesis: for x being object st x in P1 \/ P2 holds
x in P `
let x be object ; :: thesis: ( x in P1 \/ P2 implies x in P ` )
assume A9: x in P1 \/ P2 ; :: thesis: x in P `
now :: thesis: x in P `
per cases ( x in P1 or x in P2 ) by A9, XBOOLE_0:def 3;
suppose A10: x in P1 ; :: thesis: x in P `
then A11: ex pa being Point of (TOP-REAL 2) st
( pa = x & s1 < pa `1 & pa `1 < s2 & t1 < pa `2 & pa `2 < t2 ) by A4;
now :: thesis: not x in P
assume x in P ; :: thesis: contradiction
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 A3;
hence contradiction by A11; :: thesis: verum
end;
hence x in P ` by A10, SUBSET_1:29; :: thesis: verum
end;
suppose x in P2 ; :: thesis: x in P `
then consider pc being Point of (TOP-REAL 2) such that
A12: pc = x and
A13: ( not s1 <= pc `1 or not pc `1 <= s2 or not t1 <= pc `2 or not pc `2 <= t2 ) by A5;
now :: thesis: not pc in P
assume pc in P ; :: thesis: contradiction
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 A3;
hence contradiction by A1, A2, A13; :: thesis: verum
end;
hence x in P ` by A12, SUBSET_1:29; :: thesis: verum
end;
end;
end;
hence x in P ` ; :: thesis: verum
end;
then A14: P1 \/ P2 c= P ` ;
hence A15: P ` = P1 \/ P2 by A8; :: thesis: ( P ` <> {} & P1 misses P2 & ( for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds
( P1A is a_component & P2B is a_component ) ) )
set s3 = (s1 + s2) / 2;
set t3 = (t1 + t2) / 2;
A16: s1 + s1 < s1 + s2 by A1, XREAL_1:6;
A17: t1 + t1 < t1 + t2 by A2, XREAL_1:6;
A18: (s1 + s1) / 2 < (s1 + s2) / 2 by A16, XREAL_1:74;
A19: (t1 + t1) / 2 < (t1 + t2) / 2 by A17, XREAL_1:74;
A20: s1 + s2 < s2 + s2 by A1, XREAL_1:6;
A21: t1 + t2 < t2 + t2 by A2, XREAL_1:6;
A22: (s1 + s2) / 2 < (s2 + s2) / 2 by A20, XREAL_1:74;
A23: (t1 + t2) / 2 < (t2 + t2) / 2 by A21, XREAL_1:74;
set pp = |[((s1 + s2) / 2),((t1 + t2) / 2)]|;
A24: |[((s1 + s2) / 2),((t1 + t2) / 2)]| `1 = (s1 + s2) / 2 by EUCLID:52;
|[((s1 + s2) / 2),((t1 + t2) / 2)]| `2 = (t1 + t2) / 2 by EUCLID:52;
then A25: |[((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 A18, A19, A22, A23, A24;
hence P ` <> {} by A4, A14; :: thesis: ( P1 misses P2 & ( for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds
( P1A is a_component & P2B is a_component ) ) )
set P9 = P ` ;
P1 misses P2 by A4, A5, Th29;
hence A26: P1 /\ P2 = {} ; :: according to XBOOLE_0:def 7 :: thesis: for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds
( P1A is a_component & P2B is a_component )
now :: thesis: for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds
( P1A is a_component & P1A is a_component & P2B is a_component )
let P1A, P2B be Subset of ((TOP-REAL 2) | (P `)); :: thesis: ( P1A = P1 & P2B = P2 implies ( P1A is a_component & P1A is a_component & P2B is a_component ) )
assume that
A27: P1A = P1 and
A28: P2B = P2 ; :: thesis: ( P1A is a_component & P1A is a_component & P2B is a_component )
P1 is convex by A4, Th25;
then A29: P1A is connected by A27, CONNSP_1:23;
A30: P2 is connected by A5, Th26;
A31: P2 = { |[sa,ta]| where sa, ta is Real : ( not s1 <= sa or not sa <= s2 or not t1 <= ta or not ta <= t2 ) } by A5, Th22;
reconsider A0 = { |[s3a,t3a]| where s3a, t3a is Real : s3a < s1 } as Subset of (TOP-REAL 2) by Lm2, Lm3;
reconsider A1 = { |[s4,t4]| where s4, t4 is Real : t4 < t1 } as Subset of (TOP-REAL 2) by Lm2, Lm4;
reconsider A2 = { |[s5,t5]| where s5, t5 is Real : s2 < s5 } as Subset of (TOP-REAL 2) by Lm2, Lm5;
reconsider A3 = { |[s6,t6]| where s6, t6 is Real : t2 < t6 } as Subset of (TOP-REAL 2) by Lm2, Lm6;
A32: P2 = ((A0 \/ A1) \/ A2) \/ A3 by A31, Th7;
t2 + 1 > t2 by XREAL_1:29;
then A33: |[(s2 + 1),(t2 + 1)]| in A3 ;
A34: P2B is connected by A28, A30, CONNSP_1:23;
A35: 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: ( CP is connected & P1A c= CP implies P1A = CP )
assume CP is connected ; :: thesis: ( not P1A c= CP or P1A = CP )
then A36: ((TOP-REAL 2) | (P `)) | CP is connected ;
now :: thesis: ( P1A c= CP & P1A c= CP implies P1A = CP )
assume A37: P1A c= CP ; :: thesis: ( not P1A c= CP or P1A = CP )
P1A /\ CP c= CP by XBOOLE_1:17;
then reconsider AP = P1A /\ CP as Subset of (((TOP-REAL 2) | (P `)) | CP) by PRE_TOPC:8;
A38: P1 /\ (P `) = P1A by A15, A27, XBOOLE_1:21;
P1 is open by A4, Th27;
then A39: P1 in the topology of (TOP-REAL 2) by PRE_TOPC:def 2;
A40: P ` = [#] ((TOP-REAL 2) | (P `)) by PRE_TOPC:def 5;
P1 /\ ([#] ((TOP-REAL 2) | (P `))) = P1A by A38, PRE_TOPC:def 5;
then A41: P1A in the topology of ((TOP-REAL 2) | (P `)) by A39, PRE_TOPC:def 4;
A42: CP = [#] (((TOP-REAL 2) | (P `)) | CP) by PRE_TOPC:def 5;
A43: AP <> {} (((TOP-REAL 2) | (P `)) | CP) by A4, A25, A27, A37, XBOOLE_1:28;
AP in the topology of (((TOP-REAL 2) | (P `)) | CP) by A41, A42, PRE_TOPC:def 4;
then A44: AP is open by PRE_TOPC:def 2;
P2B /\ CP c= CP by XBOOLE_1:17;
then reconsider BP = P2B /\ CP as Subset of (((TOP-REAL 2) | (P `)) | CP) by PRE_TOPC:8;
A45: P2 /\ (P `) = P2B by A15, A28, XBOOLE_1:21;
P2 is open by A5, Th28;
then A46: P2 in the topology of (TOP-REAL 2) by PRE_TOPC:def 2;
P2 /\ ([#] ((TOP-REAL 2) | (P `))) = P2B by A45, PRE_TOPC:def 5;
then A47: P2B in the topology of ((TOP-REAL 2) | (P `)) by A46, PRE_TOPC:def 4;
CP = [#] (((TOP-REAL 2) | (P `)) | CP) by PRE_TOPC:def 5;
then BP in the topology of (((TOP-REAL 2) | (P `)) | CP) by A47, PRE_TOPC:def 4;
then A48: BP is open by PRE_TOPC:def 2;
A49: CP = (P1A \/ P2B) /\ CP by A15, A27, A28, A40, XBOOLE_1:28
.= AP \/ BP by XBOOLE_1:23 ;
now :: thesis: not BP <> {}
assume A50: BP <> {} ; :: thesis: contradiction
A51: 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 A4, A5, Th29;
then P1 /\ P2 = {} ;
then AP misses BP by A27, A28, A51;
hence contradiction by A36, A42, A43, A44, A48, A49, A50, CONNSP_1:11; :: thesis: verum
end;
hence ( not P1A c= CP or P1A = CP ) by A49, XBOOLE_1:28; :: thesis: verum
end;
hence ( not P1A c= CP or P1A = CP ) ; :: thesis: verum
end;
hence P1A is a_component by A29; :: thesis: ( P1A is a_component & P2B is a_component )
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: ( CP is connected & P2B c= CP implies P2B = CP )
assume CP is connected ; :: thesis: ( not P2B c= CP or P2B = CP )
then A52: ((TOP-REAL 2) | (P `)) | CP is connected ;
assume A53: P2B c= CP ; :: thesis: P2B = CP
P2B /\ CP c= CP by XBOOLE_1:17;
then reconsider BP = P2B /\ CP as Subset of (((TOP-REAL 2) | (P `)) | CP) by PRE_TOPC:8;
A54: P2 /\ (P `) = P2B by A15, A28, XBOOLE_1:21;
P2 is open by A5, Th28;
then A55: P2 in the topology of (TOP-REAL 2) by PRE_TOPC:def 2;
A56: P ` = [#] ((TOP-REAL 2) | (P `)) by PRE_TOPC:def 5;
P2 /\ ([#] ((TOP-REAL 2) | (P `))) = P2B by A54, PRE_TOPC:def 5;
then A57: P2B in the topology of ((TOP-REAL 2) | (P `)) by A55, PRE_TOPC:def 4;
A58: CP = [#] (((TOP-REAL 2) | (P `)) | CP) by PRE_TOPC:def 5;
A59: BP <> {} (((TOP-REAL 2) | (P `)) | CP) by A28, A32, A33, A53, XBOOLE_1:28;
BP in the topology of (((TOP-REAL 2) | (P `)) | CP) by A57, A58, PRE_TOPC:def 4;
then A60: BP is open by PRE_TOPC:def 2;
P1A /\ CP c= CP by XBOOLE_1:17;
then reconsider AP = P1A /\ CP as Subset of (((TOP-REAL 2) | (P `)) | CP) by PRE_TOPC:8;
A61: P1 /\ (P `) = P1A by A15, A27, XBOOLE_1:21;
P1 is open by A4, Th27;
then A62: P1 in the topology of (TOP-REAL 2) by PRE_TOPC:def 2;
P1 /\ ([#] ((TOP-REAL 2) | (P `))) = P1A by A61, PRE_TOPC:def 5;
then A63: P1A in the topology of ((TOP-REAL 2) | (P `)) by A62, PRE_TOPC:def 4;
CP = [#] (((TOP-REAL 2) | (P `)) | CP) by PRE_TOPC:def 5;
then AP in the topology of (((TOP-REAL 2) | (P `)) | CP) by A63, PRE_TOPC:def 4;
then A64: AP is open by PRE_TOPC:def 2;
A65: CP = (P1A \/ P2B) /\ CP by A15, A27, A28, A56, XBOOLE_1:28
.= AP \/ BP by XBOOLE_1:23 ;
now :: thesis: not AP <> {}
assume A66: AP <> {} ; :: thesis: contradiction
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 A26, A27, A28;
hence contradiction by A52, A58, A59, A60, A64, A65, A66, CONNSP_1:11; :: thesis: verum
end;
hence P2B = CP by A53, A65, XBOOLE_1:28; :: thesis: verum
end;
hence ( P1A is a_component & P2B is a_component ) by A29, A34, A35; :: thesis: verum
end;
hence for P1A, P2B being Subset of ((TOP-REAL 2) | (P `)) st P1A = P1 & P2B = P2 holds
( P1A is a_component & P2B is a_component ) ; :: thesis: verum