theorem :: PARTIT_2:3

for Y being non empty set
for R being Relation of Y holds R c= nabla Y ;