let L be non empty Boolean RelStr ; :: thesis: for a, b being Element of L holds (a "/\" b) "\/" (a \ b) = a
let a, b be Element of L; :: thesis: (a "/\" b) "\/" (a \ b) = a
thus (a "/\" b) "\/" (a \ b) = ((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" ('not' b)) by Th17
.= a "/\" ((a "/\" b) "\/" ('not' b)) by LATTICE3:17
.= a "/\" ((('not' b) "\/" a) "/\" (('not' b) "\/" b)) by Th17
.= a "/\" ((('not' b) "\/" a) "/\" (Top L)) by Th34
.= a "/\" (('not' b) "\/" a) by WAYBEL_1:4
.= a by LATTICE3:18 ; :: thesis: verum