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