let X be non empty TopSpace; :: thesis: for A being Subset of X holds A,A ` constitute_a_decomposition
let A be Subset of X; :: thesis: A,A ` constitute_a_decomposition
thus A,A ` constitute_a_decomposition :: thesis: verum

proof

( A misses A ` & A \/ (A ` ) = [#] X ) by PRE_TOPC:18, XBOOLE_1:79;
hence A,A ` constitute_a_decomposition by Def1; :: thesis: verum

end;