let x, y be set ; :: according to TAXONOM2:def 3 :: thesis: ( x in {{} } & y in {{} } & not x c= y & not y c= x implies x misses y )
assume that
A1: x in {{} } and
A2: y in {{} } ; :: thesis: ( x c= y or y c= x or x misses y )
x = {} by A1, TARSKI:def 1;
hence ( x c= y or y c= x or x misses y ) by A2, TARSKI:def 1; :: thesis: verum