not Total A c= id A by Th1;
hence not RelStr(# A,(Total A) #) is diagonal by Def1; :: thesis: verum