let A, B be Subset of I[01]; :: thesis: for a, b, c being Real st a < b & b < c & A = [.a,b.[ & B = ].b,c.] holds
A,B are_separated
let a, b, c be Real; :: thesis: ( a < b & b < c & A = [.a,b.[ & B = ].b,c.] implies A,B are_separated )
assume that
A1: a < b and
A2: b < c and
A3: A = [.a,b.[ and
A4: B = ].b,c.] ; :: thesis: A,B are_separated
Cl A = [.a,b.] by A1, A3, Th12;
hence Cl A misses B by A4, XXREAL_1:90; :: according to CONNSP_1:def 1 :: thesis: A misses Cl B
Cl B = [.b,c.] by A2, A4, Th11;
hence A misses Cl B by A3, XXREAL_1:95; :: thesis: verum