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 :: thesis: for x, y being Element of L9 holds (((x + y) `) + ((x + (y `)) `)) ` = x

let x, y be Element of L9; :: thesis: (((x + y) `) + ((x + (y `)) `)) ` = x
thus (((x + y) `) + ((x + (y `)) `)) ` = (x + y) "/\" (x + (y `)) by Th33
.= ((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 Th33
.= 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 Th59
.= x + (Bottom L9) by Th60
.= x ; :: thesis: verum

end;

hence L is Robbins ; :: thesis: verum