theorem Th3: :: CAYLDICK:3
for u, v, x, y being set st <%u,v%> = <%x,y%> holds
( u = x & v = y )