theorem Th25: :: WAYBEL_2:25

for L being non empty reflexive antisymmetric RelStr
for J being set
for f being Function of J, the carrier of L holds rng f c= rng (netmap ((FinSups f),L))