thus a "\/" a = (a "/\" (a "\/" a)) "\/" a by Def9
.= a by Def8 ; :: thesis: verum