Mutual exclusion algorithms are essential for contemporary programs having parallel processes, and they offer typical examples of verification of such time-concerned cooperating programs. Especially, the Ricart-Agrawala mutual exclusion algorithm for distributed systems is one of the outstanding and well-known algorithm not only practical but also theoretical. N-labeled calculus is investigated lately for verification and analysis of time-concerned cooperating program systems, especially those in the artificial intelligence area. It has high formality since they are based on the Peano arithmetic, one of the natural number theories. In this paper, the Ricart-Agrawala mutual exclusion algorithm is formally represented and verified in the calculus.