let A, B be Subset of R^1; for b being Real st A = ].-infty,b.[ & B = ].b,+infty.[ holds
A,B are_separated
let b be Real; ( A = ].-infty,b.[ & B = ].b,+infty.[ implies A,B are_separated )
assume that
A1:
A = ].-infty,b.[
and
A2:
B = ].b,+infty.[
; A,B are_separated
Cl B = [.b,+infty.[
by A2, Th48;
then A3:
Cl B misses A
by A1, XXREAL_1:94;
Cl A = ].-infty,b.]
by A1, Th50;
then
Cl A misses B
by A2, XXREAL_1:91;
hence
A,B are_separated
by A3, CONNSP_1:def 1; verum