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