reconsider TD = the tagged_division of A as set by TARSKI:1;
TD in tagged_divs A by Def1;
hence not tagged_divs A is empty ; :: thesis: verum