let L be non empty meet-commutative meet-absorbing join-absorbing OrthoLattStr ; :: thesis: ( L is Boolean & L is well-complemented implies L is Kleene )
assume that
A1: L is Boolean and
A2: L is well-complemented ; :: thesis: L is Kleene
let x, y be Element of L; :: according to PARTPR_1:def 18 :: thesis: x "/\" (x `) [= y "\/" (y `)
( x ` is_a_complement_of x & y ` is_a_complement_of y ) by A2;
hence (x "/\" (x `)) "\/" (y "\/" (y `)) = y "\/" (y `) by A1, LATTICES:def 17; :: according to LATTICES:def 3 :: thesis: verum