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