let L be non empty Boolean RelStr ; :: thesis: for a, b being Element of L st a <= b holds
b = a "\/" (b \ a)
let a, b be Element of L; :: thesis: ( a <= b implies b = a "\/" (b \ a) )
assume A1: a <= b ; :: thesis: b = a "\/" (b \ a)
a "\/" (b \ a) = (a "\/" b) "/\" (a "\/" ('not' a)) by WAYBEL_1:5
.= b "/\" (('not' a) "\/" a) by A1, Th8
.= b "/\" (Top L) by Th34
.= b by WAYBEL_1:4 ;
hence b = a "\/" (b \ a) ; :: thesis: verum