[.r,r.] = {r} by Th17;
hence not [.r,r.] is empty ; :: thesis: verum