theorem Th26: :: WAYBEL16:26

for L being complete LATTICE
for p being Element of L st ex k being Element of L st p is_maximal_in the carrier of L \ (uparrow k) holds
p is completely-irreducible