let GX be TopSpace; :: thesis: for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated holds

( A is open & A is closed & B is open & B is closed )

let A, B be Subset of GX; :: thesis: ( [#] GX = A \/ B & A,B are_separated implies ( A is open & A is closed & B is open & B is closed ) )

assume that

A1: [#] GX = A \/ B and

A2: A,B are_separated ; :: thesis: ( A is open & A is closed & B is open & B is closed )

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

B c= Cl B by PRE_TOPC:18;

then A4: ( A misses Cl B implies Cl B = B ) by A1, XBOOLE_1:73;

A c= Cl A by PRE_TOPC:18;

then A5: ( Cl A misses B implies Cl A = A ) by A1, XBOOLE_1:73;

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

hence ( A is open & A is closed & B is open & B is closed ) by A2, A5, A4, A3, PRE_TOPC:22, PRE_TOPC:23; :: thesis: verum

( A is open & A is closed & B is open & B is closed )

let A, B be Subset of GX; :: thesis: ( [#] GX = A \/ B & A,B are_separated implies ( A is open & A is closed & B is open & B is closed ) )

assume that

A1: [#] GX = A \/ B and

A2: A,B are_separated ; :: thesis: ( A is open & A is closed & B is open & B is closed )

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

B c= Cl B by PRE_TOPC:18;

then A4: ( A misses Cl B implies Cl B = B ) by A1, XBOOLE_1:73;

A c= Cl A by PRE_TOPC:18;

then A5: ( Cl A misses B implies Cl A = A ) by A1, XBOOLE_1:73;

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

hence ( A is open & A is closed & B is open & B is closed ) by A2, A5, A4, A3, PRE_TOPC:22, PRE_TOPC:23; :: thesis: verum