for L being non empty OrthoLattRelStr st L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated holds
( L is Orthocomplemented & L is PartialOrdered )