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