for Y1, Y2 being set
for P1, P2 being Relation st P1 c= P2 & Y1 c= Y2 holds
Y1 |` P1 c= Y2 |` P2