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