the Division of A in divs A by Def2;
hence not divs A is empty ; :: thesis: verum