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' b)) by Th36

.= (a "/\" ('not' a)) "\/" (a "/\" ('not' b)) by WAYBEL_1:def 3

.= (Bottom L) "\/" (a "/\" ('not' b)) by Th34

.= a \ b by WAYBEL_1:3 ; :: thesis: verum

let a, b be Element of L; :: thesis: a \ (a "/\" b) = a \ b

thus a \ (a "/\" b) = a "/\" (('not' a) "\/" ('not' b)) by Th36

.= (a "/\" ('not' a)) "\/" (a "/\" ('not' b)) by WAYBEL_1:def 3

.= (Bottom L) "\/" (a "/\" ('not' b)) by Th34

.= a \ b by WAYBEL_1:3 ; :: thesis: verum