Description: Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in Kalmbach p. 25. ( fh1 analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | omlfh1.b | |
|
omlfh1.j | |
||
omlfh1.m | |
||
omlfh1.c | |
||
Assertion | omlfh1N | |