theorem Th3: :: VALUED_0:3

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