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 and

A3: B is open and

A4: A misses B ; :: thesis: A,B are_separated

A5: Cl (([#] GX) \ B) = ([#] GX) \ B by A3, PRE_TOPC:23;

A = ([#] GX) \ B by A1, A4, PRE_TOPC:5;

then A6: A is closed by A5, PRE_TOPC:22;

A7: Cl (([#] GX) \ A) = ([#] GX) \ A by A2, PRE_TOPC:23;

B = ([#] GX) \ A by A1, A4, PRE_TOPC:5;

then B is closed by A7, PRE_TOPC:22;

hence A,B are_separated by A4, A6, Th2; :: thesis: verum

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 and

A3: B is open and

A4: A misses B ; :: thesis: A,B are_separated

A5: Cl (([#] GX) \ B) = ([#] GX) \ B by A3, PRE_TOPC:23;

A = ([#] GX) \ B by A1, A4, PRE_TOPC:5;

then A6: A is closed by A5, PRE_TOPC:22;

A7: Cl (([#] GX) \ A) = ([#] GX) \ A by A2, PRE_TOPC:23;

B = ([#] GX) \ A by A1, A4, PRE_TOPC:5;

then B is closed by A7, PRE_TOPC:22;

hence A,B are_separated by A4, A6, Th2; :: thesis: verum