List of theorems referencing the symbol C_REV
(931) Theorem 808: (N in Cm) •imp ((C_Rev(N) in Cm) & (C_Rev(C_Rev(N)) = N))
(932) Theorem 809: (N in Cm) •imp (C_Rev(N) •C_PLUS N = C_0)
(936) Theorem 813: (N in Cm) •imp (C_abs(N) = C_abs(C_Rev(N)))