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, Th2, PRE_TOPC:5;
A4: B c= Cl B by PRE_TOPC:18;

A5: now

assume A misses Cl B ; :: thesis: Cl B = B
then Cl B c= B by A1, XBOOLE_1:73;
hence Cl B = B by A4, XBOOLE_0:def 10; :: thesis: verum

end;

A6: A c= Cl A by PRE_TOPC:18;

A7: now

assume Cl A misses B ; :: thesis: Cl A = A
then Cl A c= A by A1, XBOOLE_1:73;
hence Cl A = A by A6, XBOOLE_0:def 10; :: thesis: verum

end;

B = ([#] GX) \ A by A1, A2, Th2, PRE_TOPC:5;
hence ( A is open & A is closed & B is open & B is closed ) by A2, A7, A5, A3, Def1, PRE_TOPC:22, PRE_TOPC:23; :: thesis: verum