let X be non empty 1-sorted ; :: thesis: for A being Subset of X holds A,A do_not_constitute_a_decomposition
let A be Subset of X; :: thesis: A,A do_not_constitute_a_decomposition
assume A1: A,A constitute_a_decomposition ; :: thesis: contradiction

per cases ( not A is empty or A is empty ) ;

suppose A2: not A is empty ; :: thesis: contradiction

A = A ` by A1, Th3;
then A misses A by SUBSET_1:23;
then A /\ A = {} ;
hence contradiction by A2; :: thesis: verum

end;

suppose A is empty ; :: thesis: contradiction

then {} = A \/ A
.= the carrier of X by A1 ;
hence contradiction ; :: thesis: verum

end;

end;