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