theorem :: WAYBEL32:27

for R being /\-complete Semilattice
for N being net of R
for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V