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 )
thus Cl A1, Int A2 constitute_a_decomposition :: thesis: Int A1, Cl A2 constitute_a_decomposition

proof

Cl A1 = (Int (A1 ` )) ` by TDLAT_3:2;
then Cl A1 = (Int A2) ` by A1, Th4;
hence Cl A1, Int A2 constitute_a_decomposition by Th5; :: thesis: verum

end;

thus Int A1, Cl A2 constitute_a_decomposition :: thesis: verum

proof

Int A1 = (Cl (A1 ` )) ` by TOPS_1:def 1;
then Int A1 = (Cl A2) ` by A1, Th4;
hence Int A1, Cl A2 constitute_a_decomposition by Th5; :: thesis: verum

end;