theorem Th56: :: TSEP_1:56

for X being non empty TopSpace
for A1, A2 being Subset of X st A1 \/ A2 = the carrier of X holds
( A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
( A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 & C1 is closed & C2 is closed & C is open ) )