for L being finite Lattice
for a being Element of L st a <> Bottom L & a <> Top L holds
( ( a is completely-meet-irreducible implies a % is meet-irreducible ) & ( a % is meet-irreducible implies a is completely-meet-irreducible ) & ( a is completely-join-irreducible implies a % is join-irreducible ) & ( a % is join-irreducible implies a is completely-join-irreducible ) ) by Th17, Th19;