let W, x, y be set ; :: thesis: ( W is Tarski & x in W & y in W implies [x,y] in W )
assume A1: W is Tarski ; :: thesis: ( not x in W or not y in W or [x,y] in W )
assume ( x in W & y in W ) ; :: thesis: [x,y] in W
then ( {x} in W & {x,y} in W & [x,y] = {{x,y},{x}} ) by A1, Th3;
hence [x,y] in W by A1, Th3; :: thesis: verum