:: deftheorem defines ==> TDGROUP:def 4 :
for ADG being Uniquely_Two_Divisible_Group
for a, b, c, d being Element of ADG holds
( a,b ==> c,d iff [[a,b],[c,d]] in the CONGR of (AV ADG) );