theorem :: CAYLDICK:4

for x, X being set st x in X holds
<%x%> in product <%X%>