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