theorem Th42: :: FILTER_0:42

for B being B_Lattice
for a, b being Element of B holds a => b = (a `) "\/" b