let x, y be object ; :: thesis: ( x <> y implies {x} misses {y} )
assume x <> y ; :: thesis: {x} misses {y}
then not x in {y} by TARSKI:def 1;
hence {x} misses {y} by Lm6; :: thesis: verum