thus (Bottom L) "\/" a = ((Bottom L) "/\" a) "\/" a by Def16
.= a by Def8 ; :: thesis: verum