theorem Th7: :: EC_PF_2:7

for K being Abelian AddGroup
for a1, a2, a3, a4 being Element of K holds
( ((a1 + a2) + a3) + a4 = ((a4 + a2) + a3) + a1 & ((a1 + a2) + a3) + a4 = ((a1 + a4) + a3) + a2 )