let A, B be Subset of I[01] ; :: thesis: for a, b, c being real number st a < b & b < c & A = [.a,b.[ & B = ].b,c.] holds
A,B are_separated
let a, b, c be real number ; :: thesis: ( a < b & b < c & A = [.a,b.[ & B = ].b,c.] implies A,B are_separated )
assume A1: ( a < b & b < c & A = [.a,b.[ & B = ].b,c.] ) ; :: thesis: A,B are_separated
then Cl A = [.a,b.] by Th24;
hence Cl A misses B by A1, XXREAL_1:90; :: according to CONNSP_1:def 1 :: thesis: A misses Cl B
Cl B = [.b,c.] by A1, Th23;
hence A misses Cl B by A1, XXREAL_1:95; :: thesis: verum