theorem Th57: :: TSEP_1:57

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