theorem Th27: :: FILTER_0:27

for L being Lattice st L is B_Lattice holds
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 ) )