theorem Th11: :: WAYBEL33:11

for L being complete LATTICE
for N being net of L holds lim_inf N = "\/" ( { (inf (N | i)) where i is Element of N : verum } ,L)