let L be non empty Boolean RelStr ; :: thesis: for a, b being Element of L holds (a "\/" b) \ (a "/\" b) = (a \ b) "\/" (b \ a)
let a, b be Element of L; :: thesis: (a "\/" b) \ (a "/\" b) = (a \ b) "\/" (b \ a)
thus (a "\/" b) \ (a "/\" b) = (a "\/" b) "/\" (('not' a) "\/" ('not' b)) by Th39
.= ((a "\/" b) "/\" ('not' a)) "\/" ((a "\/" b) "/\" ('not' b)) by WAYBEL_1:def 3
.= ((a "/\" ('not' a)) "\/" (b "/\" ('not' a))) "\/" ((a "\/" b) "/\" ('not' b)) by WAYBEL_1:def 3
.= ((Bottom L) "\/" (b "/\" ('not' a))) "\/" ((a "\/" b) "/\" ('not' b)) by Th37
.= (b \ a) "\/" ((a "\/" b) "/\" ('not' b)) by WAYBEL_1:3
.= (b \ a) "\/" ((a "/\" ('not' b)) "\/" (b "/\" ('not' b))) by WAYBEL_1:def 3
.= (b \ a) "\/" ((a "/\" ('not' b)) "\/" (Bottom L)) by Th37
.= (a \ b) "\/" (b \ a) by WAYBEL_1:3 ; :: thesis: verum