let X be set ; :: thesis: ( X is trivial implies X is hierarchic )
assume A1: X is trivial ; :: thesis: X is hierarchic
per cases ( X is empty or ex a being object st X = {a} ) by A1, ZFMISC_1:131;
suppose A2: X is empty ; :: thesis: X is hierarchic
thus X is hierarchic by A2; :: thesis: verum
end;
suppose ex a being object st X = {a} ; :: thesis: X is hierarchic
then consider a being object such that
A3: X = {a} ;
X is hierarchic
proof
let x, y be set ; :: according to TAXONOM2:def 3 :: thesis: ( x in X & y in X & not x c= y & not y c= x implies x misses y )
assume that
A4: x in X and
A5: y in X ; :: thesis: ( x c= y or y c= x or x misses y )
x = a by A3, A4, TARSKI:def 1;
hence ( x c= y or y c= x or x misses y ) by A3, A5, TARSKI:def 1; :: thesis: verum
end;
hence X is hierarchic ; :: thesis: verum
end;
end;