reconsider G = FreeGen X as V3() 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