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