let x, y be set ; :: thesis: ( {x} c= {y} implies x = y )
( {x} = {y} implies x = y )

proof

x in {x} by TARSKI:def 1;
hence ( {x} = {y} implies x = y ) by TARSKI:def 1; :: thesis: verum

end;

hence ( {x} c= {y} implies x = y ) by Lm3; :: thesis: verum