id M in set_End M ;
hence id M is Element of set_End M ; :: thesis: verum