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;