theorem Th2: :: VALUED_0:2

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