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 Th27;
hence a => b = (a `) "\/" b by Def7; :: thesis: verum