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

( 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