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

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 )
;

end;

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;then A misses A by SUBSET_1:23;

then A /\ A = {} ;

hence contradiction by A2; :: thesis: verum