命題
C を圏とする。
Set を集合の圏とする。
C は忠実(過去スレ017の403)な関手 F：C → Set をもつとする。

このとき C は正則べき良(>>650)かつ正則余べき良(>>660)である。

証明
X を C-対象とする。
(e, Y) を X の正則商対象(>>653)とする。
R(e, Y) = {(x, y) ∈ F(X)×F(X)；F(e)(x) = F(e)(y)} とおく。
R(e, Y) は F(X) 上の同値関係である。

(e_1, Y_1) と (e_2, Y_2) を X の正則商対象とし、
R(e_1, Y_1) = R(e_2, Y_2) とする。
(e_1, Y_1) = Coker(f_1, g_1)
(e_2, Y_2) = Coker(f_2, g_2)
とする。

e_1f_1 = e_1g_1 より、(F(f_1), F(g_1)) ∈ R(e_1, Y_1) = R(e_2, Y_2)
よって、e_2f_1 = e_2g_1
よって、(e_2, Y_2) ≦ (e_1, Y_1)
同様に (e_1, Y_1) ≦ (e_2, Y_2)
よって、(e_1, Y_1) と (e_2, Y_2) は同型(>>667)である。

以上から X の正則商対象の同型類全体は F(X) 上の同値関係全体の集合の部分集合と
１対１に対応する。
よって、C は正則余べき良である。

>>682より、C^o も正則余べき良である。
従って C は正則べき良である。
証明終