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

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