for R being complete LATTICE
for N being constant net of R holds the_value_of N is_S-limit_of N by Th23;