for n being non zero Nat holds
( not addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is empty & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is Abelian & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_complementable & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is add-associative & addLoopStr(# the carrier of (INT.Ring n), the addF of (INT.Ring n), the ZeroF of (INT.Ring n) #) is right_zeroed )