for ADG being Uniquely_Two_Divisible_Group holds
( the carrier of (AV ADG) = the carrier of ADG & the CONGR of (AV ADG) = CONGRD ADG ) ;