FreeGenSetNSG (f,D) is free by Th6;
hence FreeUnivAlgNSG (f,D) is free by Def7; :: thesis: verum