:: deftheorem defines AV TDGROUP:def 3 :
for ADG being non empty addLoopStr holds AV ADG = AffinStruct(# the carrier of ADG,(CONGRD ADG) #);