Description: A poset element less than or equal to an atom equals either zero or the atom. (Contributed by NM, 15-Oct-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | leatom.b | ||
leatom.l | |||
leatom.z | |||
leatom.a | |||
Assertion | leat |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leatom.b | ||
2 | leatom.l | ||
3 | leatom.z | ||
4 | leatom.a | ||
5 | 1 2 3 4 | leatb | |
6 | 5 | biimpa |