the carrier of (NormForm A) = Normal_forms_on A by Def12;
hence not NormForm A is empty ; :: thesis: verum