theorem Th13: :: WAYBEL_6:13

for L being LATTICE
for p being Element of L
for F being Filter of L st p is_maximal_in F ` holds
p is irreducible