let B be B_Lattice; :: thesis: B is implicative
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