let X be non empty 1-sorted ; :: 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
( A misses A ` & A \/ (A `) = [#] X ) by PRE_TOPC:2, XBOOLE_1:79;
hence A,A ` constitute_a_decomposition ; :: thesis: verum