a "/\" (a "\/" a) = a by Def9;
hence a "/\" a = a ; :: thesis: verum