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