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 Th6;
hence Cl A, Int (A ` ) constitute_a_decomposition by Th10; :: 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 Th6;
hence Cl (A ` ), Int A constitute_a_decomposition by Th10; :: 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, Th10; :: thesis: Int (A ` ), Cl A constitute_a_decomposition
thus Int (A ` ), Cl A constitute_a_decomposition by A1, Th10; :: thesis: verum