theorem Th5: :: VALUED_0:5

for R being Relation
for S being integer-valued Relation st R c= S holds
R is integer-valued