theorem :: CLASSES5:75

for x being object holds Trivial-addLoopStr x is strict AddGroup ;