theorem Th25: :: WAYBEL21:25

for S being complete LATTICE
for N being net of S holds { ("/\" ( { (N . i) where i is Element of N : i >= j } ,S)) where j is Element of N : verum } is non empty directed Subset of S