let R be complete LATTICE; :: thesis: for N being constant net of R holds the_value_of N is_S-limit_of N
let N be constant net of R; :: thesis: the_value_of N is_S-limit_of N
the_value_of N <= lim_inf N by Th23;
hence the_value_of N is_S-limit_of N by Def7; :: thesis: verum