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