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 ` )
thus (a "\/" b) ` = (((a ` ) ` ) "\/" b) ` by Th49
.= (((a ` ) ` ) "\/" ((b ` ) ` )) ` by Th49
.= (((a ` ) "/\" (b ` )) ` ) ` by Th50
.= (a ` ) "/\" (b ` ) by Th49 ; :: thesis: verum