let A, B be Subset of R^1; :: thesis: 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; :: thesis: ( 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.] ; :: thesis: 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; :: thesis: verum