let A, B be Subset of I[01]; 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; ( 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.]
; A,B are_separated
Cl A = [.a,b.]
by A1, A3, Th12;
hence
Cl A misses B
by A4, XXREAL_1:90; CONNSP_1:def 1 A misses Cl B
Cl B = [.b,c.]
by A2, A4, Th11;
hence
A misses Cl B
by A3, XXREAL_1:95; verum