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