for T being complete Lawson TopLattice
for N being eventually-filtered net of T holds Lim N = {(inf N)}