let B be B_Lattice; :: thesis: for a being Element of B
for a9 being Element of (B .:) holds
( (a .:) ` = a ` & (.: a9) ` = a9 ` )
let a be Element of B; :: thesis: for a9 being Element of (B .:) holds
( (a .:) ` = a ` & (.: a9) ` = a9 ` )
let a9 be Element of (B .:); :: thesis: ( (a .:) ` = a ` & (.: a9) ` = a9 ` )
(.: a9) .: = .: a9 ;
hence ( (a .:) ` = a ` & (.: a9) ` = a9 ` ) by Lm4; :: thesis: verum