let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( Cl A, Int (A `) constitute_a_decomposition & Cl (A `), Int A constitute_a_decomposition & Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )
let A be Subset of X; :: thesis: ( Cl A, Int (A `) constitute_a_decomposition & Cl (A `), Int A constitute_a_decomposition & Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )
A1: A,A ` constitute_a_decomposition by Th5;
hence Cl A, Int (A `) constitute_a_decomposition by Th9; :: thesis: ( Cl (A `), Int A constitute_a_decomposition & Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )
A2: A ` ,A constitute_a_decomposition by Th5;
hence Cl (A `), Int A constitute_a_decomposition by Th9; :: thesis: ( Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )
thus Int A, Cl (A `) constitute_a_decomposition by A2, Th9; :: thesis: Int (A `), Cl A constitute_a_decomposition
thus Int (A `), Cl A constitute_a_decomposition by A1, Th9; :: thesis: verum