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