for L being LATTICE
for l being Element of L st (uparrow l) \ {l} is Filter of L holds
l is irreducible