let X be non empty TopSpace; :: thesis: 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; :: thesis: ( 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; :: thesis: verum