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

( 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