for X, Y being set
for a, b being object st X <> {} & X --> a c= Y --> b holds
a = b