let L be non empty OrthoLattStr ; :: thesis: ( L is Boolean & L is well-complemented & L is Lattice-like implies L is Ortholattice )
assume ( L is Boolean & L is well-complemented & L is Lattice-like ) ; :: thesis: L is Ortholattice
then reconsider L9 = L as non empty Lattice-like Boolean well-complemented OrthoLattStr ;
A1: for x, y being Element of L9 holds x "/\" y = ((x `) "\/" (y `)) ` by ROBBINS1:33;
( ( for x being Element of L9 holds (x `) ` = x ) & ( for x, y being Element of L9 holds x |_| (x `) = y |_| (y `) ) ) by ROBBINS1:3, ROBBINS1:4;
hence L is Ortholattice by A1, Def6, Def7, ROBBINS1:def 23; :: thesis: verum