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