let X be non empty TopSpace; :: thesis: for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition )
let A1, A2 be Subset of X; :: thesis: ( A1,A2 constitute_a_decomposition implies ( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition ) )
assume A1: A1,A2 constitute_a_decomposition ; :: thesis: ( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition )
Cl A1 = (Int (A1 `)) ` by TDLAT_3:1;
then Cl A1 = (Int A2) ` by A1, Th3;
hence Cl A1, Int A2 constitute_a_decomposition by Th4; :: thesis: Int A1, Cl A2 constitute_a_decomposition
Int A1 = (Cl (A1 `)) ` by TOPS_1:def 1;
then Int A1 = (Cl A2) ` by A1, Th3;
hence Int A1, Cl A2 constitute_a_decomposition by Th4; :: thesis: verum