let s1, t1, s2, t2 be Real; :: thesis: for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } holds
P is connected
let P be Subset of (TOP-REAL 2); :: thesis: ( P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } implies P is connected )
assume P = { |[s,t]| where s, t is Real : ( not s1 <= s or not s <= s2 or not t1 <= t or not t <= t2 ) } ; :: thesis: P is connected
then A1: P = (( { |[s3,t3]| where s3, t3 is Real : s3 < s1 } \/ { |[s4,t4]| where s4, t4 is Real : t4 < t1 } ) \/ { |[s5,t5]| where s5, t5 is Real : s2 < s5 } ) \/ { |[s6,t6]| where s6, t6 is Real : t2 < t6 } by Th7;
reconsider A0 = { |[s,t]| where s, t is Real : s < s1 } , A1 = { |[s,t]| where s, t is Real : t < t1 } , A2 = { |[s,t]| where s, t is Real : s2 < s } , A3 = { |[s,t]| where s, t is Real : t2 < t } as Subset of (TOP-REAL 2) by Lm2, Lm3, Lm4, Lm5, Lm6;
A2: s1 - 1 < s1 by XREAL_1:44;
A3: t1 - 1 < t1 by XREAL_1:44;
A4: |[(s1 - 1),(t1 - 1)]| in A0 by A2;
|[(s1 - 1),(t1 - 1)]| in A1 by A3;
then A0 /\ A1 <> {} by A4, XBOOLE_0:def 4;
then A5: A0 meets A1 ;
A6: s2 < s2 + 1 by XREAL_1:29;
A7: |[(s2 + 1),(t1 - 1)]| in A1 by A3;
|[(s2 + 1),(t1 - 1)]| in A2 by A6;
then A1 /\ A2 <> {} by A7, XBOOLE_0:def 4;
then A8: A1 meets A2 ;
A9: t2 < t2 + 1 by XREAL_1:29;
A10: |[(s2 + 1),(t2 + 1)]| in A2 by A6;
|[(s2 + 1),(t2 + 1)]| in A3 by A9;
then A2 /\ A3 <> {} by A10, XBOOLE_0:def 4;
then A11: A2 meets A3 ;
A12: A0 is convex by Th10;
A13: A1 is convex by Th12;
A14: A2 is convex by Th9;
A3 is convex by Th11;
hence P is connected by A1, A5, A8, A11, A12, A13, A14, Th5; :: thesis: verum