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 ( x in {} & y in {} ) ; :: thesis: ( x c= y or y c= x or x misses y )
hence ( x c= y or y c= x or x misses y ) ; :: thesis: verum