Theorem omlol

Description: An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Assertion	omlol	|- ( K e. OML -> K e. OL )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` K ) = ( Base ` K )
2		eqid	|- ( le ` K ) = ( le ` K )
3		eqid	|- ( join ` K ) = ( join ` K )
4		eqid	|- ( meet ` K ) = ( meet ` K )
5		eqid	|- ( oc ` K ) = ( oc ` K )
6	1 2 3 4 5	isoml	|- ( K e. OML <-> ( K e. OL /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( x ( le ` K ) y -> y = ( x ( join ` K ) ( y ( meet ` K ) ( ( oc ` K ) ` x ) ) ) ) ) )
7	6	simplbi	|- ( K e. OML -> K e. OL )