theorem Th41: :: WAYBEL_2:41

for L being non empty reflexive RelStr st L is satisfying_MC holds
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))))