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:20;
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:6; :: 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:21;
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:5, LATTICES:11;
hence r1 [= (p `) "\/" q by A3, A2, LATTICES:7; :: thesis: verum