let A, B be Subset of R^1; for a, b, c, d being Real st a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] holds
A,B are_separated
let a, b, c, d be Real; ( a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] implies A,B are_separated )
assume that
A1:
a < b
and
A2:
b <= c
and
A3:
c < d
and
A4:
A = [.a,b.[
and
A5:
B = ].c,d.]
; A,B are_separated
Cl ].c,d.] = [.c,d.]
by A3, BORSUK_4:11;
then
Cl B = [.c,d.]
by A5, JORDAN5A:24;
then A6:
Cl B misses A
by A2, A4, XXREAL_1:95;
Cl [.a,b.[ = [.a,b.]
by A1, BORSUK_4:12;
then
Cl A = [.a,b.]
by A4, JORDAN5A:24;
then
Cl A misses B
by A2, A5, XXREAL_1:90;
hence
A,B are_separated
by A6, CONNSP_1:def 1; verum