let X be set ; :: thesis: ( X is trivial implies X is hierarchic )

assume A1: X is trivial ; :: thesis: 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;

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

end;A3: X = {a} ;

X is hierarchic

proof

hence
X is hierarchic
; :: thesis: verum
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;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