theorem Th51: :: FILTER_1:51

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