let x, y be object ; :: thesis: ( {x} c= {y} implies x = y )
x in {x} by TARSKI:def 1;
then ( {x} = {y} implies x = y ) by TARSKI:def 1;
hence ( {x} c= {y} implies x = y ) by Lm3; :: thesis: verum