let x, y be set ; :: according to TAXONOM2:def 5 :: thesis: ( x in {} & y in {} & x <> y implies x misses y )
assume that
A1: x in {} and
y in {} ; :: thesis: ( not x <> y or x misses y )
thus ( not x <> y or x misses y ) by A1; :: thesis: verum