let X be non empty TopSpace; for A1, A2 being Subset of X holds
( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated )
let A1, A2 be Subset of X; ( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated )
( A1,A1 ` constitute_a_decomposition & A2,A2 ` constitute_a_decomposition )
by Th5;
hence
( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated )
by Th15; verum