reconsider G = FreeGen X as non-empty GeneratorSet of T by MSAFREE4:45;
take G ; :: thesis: G is basic
thus FreeGen T c= G ; :: according to AOFA_A01:def 3 :: thesis: verum