consider A being non empty set ;
consider B being empty set ;
consider C being set such that
A1: C = {A,B} ;
take C ; :: thesis: ( not C is trivial & C is hierarchic )
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 A3: ( x in C & y in C ) ; :: thesis: ( x c= y or y c= x or x misses y )

per cases ( x = A or x = B ) by A1, A3, TARSKI:def 2;

suppose A4: x = A ; :: thesis: ( x c= y or y c= x or x misses y )

per cases ( y = A or y = B ) by A1, A3, TARSKI:def 2;

suppose y = A ; :: 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 A4; :: thesis: verum

end;

suppose y = B ; :: 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 XBOOLE_1:65; :: thesis: verum

end;

end;

end;

suppose x = B ; :: 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 XBOOLE_1:65; :: thesis: verum

end;

end;

end;

now

assume A5: C is trivial ; :: thesis: contradiction

per cases ( C is empty or ex x being set st C = {x} ) by A5, REALSET1:def 4;

suppose C is empty ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose ex x being set st C = {x} ; :: thesis: contradiction

then consider a being set such that
A6: C = {a} ;
thus contradiction by A1, A6, ZFMISC_1:9; :: thesis: verum

end;

end;

end;

hence ( not C is trivial & C is hierarchic ) by A2; :: thesis: verum