let L be Lattice; :: thesis: ( L is B_Lattice implies for p, q being Element of L holds
( p "/\" ((p ` ) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p ` ) "\/" q ) ) )
assume L is B_Lattice ; :: thesis: for p, q being Element of L holds
( p "/\" ((p ` ) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p ` ) "\/" q ) )
then reconsider S = L as B_Lattice ;
let p, q be Element of L; :: thesis: ( p "/\" ((p ` ) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p ` ) "\/" q ) )
set r = (p ` ) "\/" q;
reconsider K = S as 0_Lattice ;
reconsider J = S as 1_Lattice ;
reconsider p' = p, q' = q as Element of K ;
reconsider p'' = p as Element of S ;
A1: ( p'' "/\" (p'' ` ) = Bottom L & (Bottom K) "\/" (p' "/\" q') = p' "/\" q' & p "/\" q = q "/\" p ) by LATTICES:39, LATTICES:47;
reconsider K = S as D_Lattice ;
reconsider p' = p, q' = q, r' = (p ` ) "\/" q as Element of K ;
p' "/\" r' = (p' "/\" (p' ` )) "\/" (p' "/\" q') by LATTICES:def 11;
hence p "/\" ((p ` ) "\/" q) [= q by A1, LATTICES:23; :: thesis: for r being Element of L st p "/\" r [= q holds
r [= (p ` ) "\/" q
let r1 be Element of L; :: thesis: ( p "/\" r1 [= q implies r1 [= (p ` ) "\/" q )
reconsider r1' = r1 as Element of K ;
reconsider pp = p, r'' = r1 as Element of J ;
assume p "/\" r1 [= q ; :: thesis: r1 [= (p ` ) "\/" q
then A2: (p ` ) "\/" (p "/\" r1) [= (p ` ) "\/" q by Th1;
( (p' ` ) "\/" (p' "/\" r1') = ((p' ` ) "\/" p') "/\" ((p' ` ) "\/" r1') & r1 [= r1 "\/" (p ` ) & (p'' ` ) "\/" p'' = Top L & (Top J) "/\" ((pp ` ) "\/" r'') = (pp ` ) "\/" r'' & r1 "\/" (p ` ) = (p ` ) "\/" r1 ) by LATTICES:22, LATTICES:31, LATTICES:43, LATTICES:48;
hence r1 [= (p ` ) "\/" q by A2, LATTICES:25; :: thesis: verum