set B = the empty set ;
set A = the non empty set ;
consider C being set such that
A1: C = { the non empty set , the empty set } ;
A2: C is hierarchic
proof
let x, y be set ; :: according to TAXONOM2:def 3 :: thesis: ( x in C & y in C & not x c= y & not y c= x implies x misses y )
assume that
A3: x in C and
A4: y in C ; :: thesis: ( x c= y or y c= x or x misses y )
per cases ( x = the non empty set or x = the empty set ) by A1, A3, TARSKI:def 2;
suppose A5: x = the non empty set ; :: thesis: ( x c= y or y c= x or x misses y )
per cases ( y = the non empty set or y = the empty set ) by A1, A4, TARSKI:def 2;
suppose y = the non empty set ; :: thesis: ( x c= y or y c= x or x misses y )
hence ( x c= y or y c= x or x misses y ) by A5; :: thesis: verum
end;
suppose y = the empty set ; :: thesis: ( x c= y or y c= x or x misses y )
hence ( x c= y or y c= x or x misses y ) ; :: thesis: verum
end;
end;
end;
suppose x = the empty set ; :: thesis: ( x c= y or y c= x or x misses y )
hence ( x c= y or y c= x or x misses y ) ; :: thesis: verum
end;
end;
end;
take C ; :: thesis: ( not C is trivial & C is hierarchic )
now :: thesis: not C is trivial
assume A6: C is trivial ; :: thesis: contradiction
per cases ( C is empty or ex x being object st C = {x} ) by A6, ZFMISC_1:131;
end;
end;
hence ( not C is trivial & C is hierarchic ) by A2; :: thesis: verum