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

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

take
C
; :: thesis: ( not C is trivial & C is hierarchic )
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 )

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

end;

now :: thesis: not C is trivial

hence
( not C is trivial & C is hierarchic )
by A2; :: thesis: verumassume A6:
C is trivial
; :: thesis: contradiction

end;