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