ID M in setvect M ;
hence not setvect M is empty ; :: thesis: verum