let L be non empty reflexive RelStr ; :: thesis: ( L is satisfying_MC implies for x being Element of L
for N being non empty 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 non empty 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 non empty prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap N,L)))
let N be non empty 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, Def6 ; :: thesis: verum