for K, L being non empty ComplStr
for x being Element of K
for y being Element of L st the Compl of K = the Compl of L & x = y holds
x ` = y `