theorem Th12: :: INT_3:12

for p being Nat st p > 1 holds
( INT.Ring p is non empty non degenerated right_complementable almost_left_invertible associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr iff p is Prime )