let A, B be Subset of R^1 ; :: thesis: for a, b, c, d being real number 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 number ; :: thesis: ( a < b & b <= c & c < d & A = [.a,b.[ & B = ].c,d.] implies A,B are_separated )
assume that
A1: ( a < b & b <= c & c < d ) and
A2: A = [.a,b.[ and
A3: B = ].c,d.] ; :: thesis: A,B are_separated
Cl [.a,b.[ = [.a,b.] by A1, BORSUK_4:21;
then Cl A = [.a,b.] by A2, TOPREAL6:80;
then A4: Cl A misses B by A1, A3, XXREAL_1:90;
Cl ].c,d.] = [.c,d.] by A1, BORSUK_4:20;
then Cl B = [.c,d.] by A3, TOPREAL6:80;
then Cl B misses A by A1, A2, XXREAL_1:95;
hence A,B are_separated by A4, CONNSP_1:def 1; :: thesis: verum