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