theorem :: CAYLDICK:2

for u, x being set st <%u%> = <%x%> holds
u = x