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 L' = L as non empty Lattice-like Boolean well-complemented OrthoLattStr ;
A1: for x being Element of L' holds (x ` ) ` = x by ROBBINS1:3;
A2: for x, y being Element of L' holds x |_| (x ` ) = y |_| (y ` ) by ROBBINS1:4;
for x, y being Element of L' holds x "/\" y = ((x ` ) "\/" (y ` )) ` by ROBBINS1:34;
hence L is Ortholattice by A1, A2, Def6, Def7, ROBBINS1:def 23; :: thesis: verum