let L be Quasi-Boolean_Algebra; :: thesis: (Bottom L) ` = Top L
thus (Bottom L) ` = ((((Bottom L) `) "/\" (Top L)) `) ` by ROBBINS3:def 6
.= ((((Bottom L) `) `) "\/" ((Top L) `)) ` by Def1
.= ((Bottom L) "\/" ((Top L) `)) ` by ROBBINS3:def 6
.= Top L by ROBBINS3:def 6 ; :: thesis: verum