let A, B be Subset of R^1; :: thesis: for b being Real st A = ].-infty,b.[ & B = ].b,+infty.[ holds
A,B are_separated
let b be Real; :: thesis: ( A = ].-infty,b.[ & B = ].b,+infty.[ implies A,B are_separated )
assume that
A1: A = ].-infty,b.[ and
A2: B = ].b,+infty.[ ; :: thesis: 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; :: thesis: verum