theorem Th47: :: WAYBEL_2:47

for L being non empty reflexive antisymmetric complete RelStr st ( for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) holds
for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))