Description: A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of PtakPulmannova p. 68. ( atcvat3i analog.) (Contributed by NM, 30-Nov-2011)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cvrat3.b | |
|
cvrat3.l | |
||
cvrat3.j | |
||
cvrat3.m | |
||
cvrat3.a | |
||
Assertion | cvrat3 | |