let x, y be object ; :: thesis: ( {x} \/ {y} = {x} implies x = y )
assume {x} \/ {y} = {x} ; :: thesis: x = y
then ( y in {x} or x in {y} ) by Lm4;
hence x = y by TARSKI:def 1; :: thesis: verum