let s1, t1, s2, t2 be Real; 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); ( 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 ) }
; 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; verum