theorem Th4: :: VALUED_0:4

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