theorem :: WAYBEL11:17

for R being complete LATTICE
for N being net of R
for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q