let L be non empty reflexive RelStr ; :: thesis: ( L is satisfying_MC implies 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)))) )
assume A1: L is satisfying_MC ; :: thesis: 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))))
let x be Element of L; :: thesis: for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
let N be prenet of L; :: thesis: ( N is eventually-directed implies x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
assume N is eventually-directed ; :: thesis: x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
then A2: rng (netmap (N,L)) is directed by Th18;
thus x "/\" (sup N) = x "/\" (sup (rng (netmap (N,L)))) by YELLOW_2:def 5
.= sup ({x} "/\" (rng (netmap (N,L)))) by A1, A2 ; :: thesis: verum