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 Lm3; :: thesis: verum