let A, B be Subset of R^1 ; :: thesis: for b being real number st A = ].-infty ,b.[ & B = ].b,+infty .[ holds
A,B are_separated
let b be real number ; :: 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 A = ].-infty ,b.] by A1, Th77;
then A3: Cl A misses B by A2, XXREAL_1:91;
Cl B = [.b,+infty .[ by A2, Th75;
then Cl B misses A by A1, XXREAL_1:94;
hence A,B are_separated by A3, CONNSP_1:def 1; :: thesis: verum