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