Ord is a Mahlo cardinal — for every closed unbounded class of ordinals C (definable by a formula with parameters), there is a regular ordinal in C. This allows one to derive the existence of strong inaccessible cardinals and much more over any ordinal. References External links Mizar system proof: http://mizar.org/version/current/html/zf_refle.html Set theory Mathematical principles