[(idm a),[a,a]] in (Concretized A) -carrier_of a by Th43;
hence not (Concretized A) -carrier_of a is empty ; :: thesis: verum