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