theorem Th39: :: NUMBER08:39

for P, R being Relation st rng R c= rng P & P is positive-yielding holds
R is positive-yielding