let A be set ; :: thesis: {} is Element of
the carrier of (NormForm A) = Normal_forms_on A by Def14;
hence {} is Element of by Lm4; :: thesis: verum