theorem Th17: :: PRE_POLY:18

for X being set
for R being Relation st field R c= X holds
R is Relation of X