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 `)) & ((a `) "\/" (b `)) "\/" (a "/\" b) = (a "/\" b) "\/" ((a `) "\/" (b `)) ) ;
A2: ((a `) "\/" (b `)) "/\" (a "/\" b) = (((a `) "\/" (b `)) "/\" a) "/\" b by Def7
.= (((a `) "/\" a) "\/" ((b `) "/\" a)) "/\" b by Def11
.= ((Bottom L) "\/" ((b `) "/\" a)) "/\" b by Th18
.= (b "/\" (b `)) "/\" a by Def7
.= (Bottom L) "/\" a by Th18
.= Bottom L ;
((a `) "\/" (b `)) "\/" (a "/\" b) = (a `) "\/" ((b `) "\/" (a "/\" b)) by Def5
.= (a `) "\/" (((b `) "\/" a) "/\" ((b `) "\/" b)) by Th9
.= (a `) "\/" (((b `) "\/" a) "/\" (Top L)) by Th19
.= (b `) "\/" (a "\/" (a `)) by Def5
.= (b `) "\/" (Top L) by Th19
.= Top L ;
then (a `) "\/" (b `) is_a_complement_of a "/\" b by A1, A2;
hence (a "/\" b) ` = (a `) "\/" (b `) by Def21; :: thesis: verum