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