theorem Th23: :: WAYBEL32:23

for R being non empty RelStr
for N being net of R holds rng the mapping of (inf_net N) = { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum }