theorem Th54: :: FILTER_2:54

for B being B_Lattice
for a being Element of B
for a9 being Element of (B .:) holds
( (a .:) ` = a ` & (.: a9) ` = a9 ` )