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