let B be B_Lattice; :: thesis: for a, b being Element of B holds a => b = (a `) "\/" b
let a, b be Element of B; :: thesis: a => b = (a `) "\/" b
( a "/\" ((a `) "\/" b) [= b & ( for c being Element of B st a "/\" c [= b holds
c [= (a `) "\/" b ) ) by Th34;
hence a => b = (a `) "\/" b by Def8; :: thesis: verum