let L be well-complemented preOrthoLattice; :: thesis: ( L is Boolean implies L is Robbins )
assume L is Boolean ; :: thesis: L is Robbins
then reconsider L9 = L as Boolean well-complemented preOrthoLattice ;

now

let x, y be Element of L9; :: thesis: (((x + y) ` ) + ((x + (y ` )) ` )) ` = x
thus (((x + y) ` ) + ((x + (y ` )) ` )) ` = (x + y) "/\" (x + (y ` )) by Th34
.= ((x + y) "/\" x) + ((x + y) "/\" (y ` )) by LATTICES:def 11
.= ((x + y) "/\" x) + ((x "/\" (y ` )) + (y "/\" (y ` ))) by LATTICES:def 11
.= ((x + y) "/\" x) + ((x "/\" (y ` )) + (((y ` ) + ((y ` ) ` )) ` )) by Th34
.= x + ((x "/\" (y ` )) + (((y ` ) + ((y ` ) ` )) ` )) by LATTICES:def 9
.= (x + (x "/\" (y ` ))) + (((y ` ) + ((y ` ) ` )) ` ) by LATTICES:def 5
.= x + (((y ` ) + ((y ` ) ` )) ` ) by LATTICES:def 8
.= x + ((Top L9) ` ) by Th61
.= x + (Bottom L9) by Th62
.= x by LATTICES:39 ; :: thesis: verum

end;

hence L is Robbins by Def5; :: thesis: verum