thus (Top L) "/\" a = ((Top L) "\/" a) "/\" a by Def17
.= a by Def9 ; :: thesis: verum