for A, Y being set st A c= Y holds
id A = (id Y) | A