let L be Quasi-Boolean_Algebra; :: thesis: for x, y being Element of L holds (x "\/" y) ` = (x `) "/\" (y `)
let x, y be Element of L; :: thesis: (x "\/" y) ` = (x `) "/\" (y `)
((x `) "/\" (y `)) ` = ((x `) `) "\/" ((y `) `) by Def1;
hence (x `) "/\" (y `) = (((x `) `) "\/" ((y `) `)) ` by ROBBINS3:def 6
.= (x "\/" ((y `) `)) ` by ROBBINS3:def 6
.= (x "\/" y) ` by ROBBINS3:def 6 ;
:: thesis: verum