let GX be TopSpace; :: thesis: for A, B being Subset of GX st [#] GX = A \/ B & A is open & B is open & A misses B holds
A,B are_separated
let A, B be Subset of GX; :: thesis: ( [#] GX = A \/ B & A is open & B is open & A misses B implies A,B are_separated )
assume that
A1: [#] GX = A \/ B and
A2: ( A is open & B is open ) and
A3: A misses B ; :: thesis: A,B are_separated
A4: ( Cl (([#] GX) \ A) = ([#] GX) \ A & Cl (([#] GX) \ B) = ([#] GX) \ B ) by A2, PRE_TOPC:53;
( B = ([#] GX) \ A & A = ([#] GX) \ B ) by A1, A3, PRE_TOPC:25;
then ( B is closed & A is closed ) by A4, PRE_TOPC:52;
hence A,B are_separated by A1, A3, Th3; :: thesis: verum