theorem Th6: :: VALUED_0:6

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