let x, y, W be set ; ( W is Tarski & x in W & y in W implies [x,y] in W )
assume A1:
W is Tarski
; ( 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
; [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; verum