Theorem isolatiN

Description: Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isolati.1	⊢ 𝐾 ∈ Lat
	isolati.2	⊢ 𝐾 ∈ OP
Assertion	isolatiN	⊢ 𝐾 ∈ OL

Proof

Step	Hyp	Ref	Expression
1		isolati.1	⊢ 𝐾 ∈ Lat
2		isolati.2	⊢ 𝐾 ∈ OP
3		isolat	⊢ ( 𝐾 ∈ OL ↔ ( 𝐾 ∈ Lat ∧ 𝐾 ∈ OP ) )
4	1 2 3	mpbir2an	⊢ 𝐾 ∈ OL