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

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