let x, y, W 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 that
A2: x in W and
A3: y in W ; :: thesis: [x,y] in W
A4: {x} in W by A1, A2, Th2;
{x,y} in W by A1, A2, A3, Th2;
hence [x,y] in W by A1, A4, Th2; :: thesis: verum