theorem Th50: :: FILTER_1:50

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