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