set R = the non degenerated comRing;
take the non degenerated comRing ; :: thesis: ( the non degenerated comRing is add-associative & the non degenerated comRing is left_zeroed & the non degenerated comRing is right_zeroed )
thus ( the non degenerated comRing is add-associative & the non degenerated comRing is left_zeroed & the non degenerated comRing is right_zeroed ) ; :: thesis: verum