theorem Th54: :: TSEP_1:54

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