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 ;
reconsider J = S as 1_Lattice ;
reconsider K = S as 0_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 p9 = p, q9 = q as Element of K ;
reconsider p99 = p as Element of S ;
A1: ( p99 "/\" (p99 ` ) = Bottom L & (Bottom K) "\/" (p9 "/\" q9) = p9 "/\" q9 ) by LATTICES:39, LATTICES:47;
reconsider K = S as D_Lattice ;
reconsider p9 = p, q9 = q, r9 = (p ` ) "\/" q as Element of K ;
p9 "/\" r9 = (p9 "/\" (p9 ` )) "\/" (p9 "/\" q9) 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 r19 = r1 as Element of K ;
reconsider pp = p, r99 = r1 as Element of J ;
A2: ( (p99 ` ) "\/" p99 = Top L & (Top J) "/\" ((pp ` ) "\/" r99) = (pp ` ) "\/" r99 ) by LATTICES:43, LATTICES:48;
assume p "/\" r1 [= q ; :: thesis: r1 [= (p ` ) "\/" q
then A3: (p ` ) "\/" (p "/\" r1) [= (p ` ) "\/" q by Th1;
( (p9 ` ) "\/" (p9 "/\" r19) = ((p9 ` ) "\/" p9) "/\" ((p9 ` ) "\/" r19) & r1 [= r1 "\/" (p ` ) ) by LATTICES:22, LATTICES:31;
hence r1 [= (p ` ) "\/" q by A3, A2, LATTICES:25; :: thesis: verum