Description: An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | ollat | |- ( K e. OL -> K e. Lat ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isolat | |- ( K e. OL <-> ( K e. Lat /\ K e. OP ) ) |
|
2 | 1 | simplbi | |- ( K e. OL -> K e. Lat ) |