let L be Lattice; ( 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
; 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; ( 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; for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q
let r1 be Element of L; ( 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
; 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; verum