for x, y being set st <*x*> is_a_prefix_of <*y*> holds
x = y