Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Ortholattices and orthomodular lattices
isolat
Next ⟩
ollat
Metamath Proof Explorer
Ascii
Unicode
Theorem
isolat
Description:
The predicate "is an ortholattice."
(Contributed by
NM
, 18-Sep-2011)
Ref
Expression
Assertion
isolat
⊢
K
∈
OL
↔
K
∈
Lat
∧
K
∈
OP
Proof
Step
Hyp
Ref
Expression
1
df-ol
⊢
OL
=
Lat
∩
OP
2
1
elin2
⊢
K
∈
OL
↔
K
∈
Lat
∧
K
∈
OP