let GX be TopSpace; 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; ( [#] 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
; ( 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; verum