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
A1: B is implicative

proof

let p, q be Element of B; :: according to FILTER_0:def 7 :: thesis: ex r being Element of B st
( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds
r1 [= r ) )
take r = (p ` ) "\/" q; :: thesis: ( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds
r1 [= r ) )
thus ( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds
r1 [= r ) ) by Th34; :: thesis: verum

end;

( 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 A1, Def8; :: thesis: verum