let L be B_Lattice; :: thesis: for a, b being Element of L holds (a "/\" b) ` = (a `) "\/" (b `)
let a, b be Element of L; :: thesis: (a "/\" b) ` = (a `) "\/" (b `)
A1: ((a `) "\/" (b `)) "/\" (a "/\" b) = (((a `) "\/" (b `)) "/\" a) "/\" b by Def7
.= (((a `) "/\" a) "\/" ((b `) "/\" a)) "/\" b by Def11
.= ((Bottom L) "\/" ((b `) "/\" a)) "/\" b by Th47
.= b "/\" ((b `) "/\" a) by Th39
.= (b "/\" (b `)) "/\" a by Def7
.= (Bottom L) "/\" a by Th47
.= Bottom L by Def16 ;
((a `) "\/" (b `)) "\/" (a "/\" b) = (a `) "\/" ((b `) "\/" (a "/\" b)) by Def5
.= (a `) "\/" (((b `) "\/" a) "/\" ((b `) "\/" b)) by Th31
.= (a `) "\/" (((b `) "\/" a) "/\" (Top L)) by Th48
.= ((b `) "\/" a) "\/" (a `) by Th43
.= (b `) "\/" (a "\/" (a `)) by Def5
.= (b `) "\/" (Top L) by Th48
.= Top L by Def17 ;
then (a `) "\/" (b `) is_a_complement_of a "/\" b by A1, Def18;
hence (a "/\" b) ` = (a `) "\/" (b `) by Def21; :: thesis: verum