let L be non empty Boolean RelStr ; :: thesis: for a, b being Element of L st a misses b holds
(a "\/" b) \ b = a
let a, b be Element of L; :: thesis: ( a misses b implies (a "\/" b) \ b = a )
assume a misses b ; :: thesis: (a "\/" b) \ b = a
then a "/\" b = Bottom L by Def3;
then (a "\/" ('not' b)) "/\" (b "\/" ('not' b)) <= (Bottom L) "\/" ('not' b) by Th20;
then (a "\/" ('not' b)) "/\" (b "\/" ('not' b)) <= 'not' b by WAYBEL_1:3;
then (a "\/" ('not' b)) "/\" (Top L) <= 'not' b by Th37;
then A1: a "\/" ('not' b) <= 'not' b by WAYBEL_1:4;
'not' b <= a "\/" ('not' b) by YELLOW_0:22;
then a "\/" ('not' b) = 'not' b by A1, YELLOW_0:def 3;
then A2: a <= 'not' b by YELLOW_0:22;
(a "\/" b) \ b = (a "\/" b) "/\" ('not' b)
.= (a "/\" ('not' b)) "\/" (b "/\" ('not' b)) by WAYBEL_1:def 3
.= (a "/\" ('not' b)) "\/" (Bottom L) by Th37
.= a "/\" ('not' b) by WAYBEL_1:3
.= a by A2, Th10 ;
hence (a "\/" b) \ b = a ; :: thesis: verum