let W be Universe; :: thesis: for a being Ordinal of W holds not On W is_cofinal_with a
let a be Ordinal of W; :: thesis: not On W is_cofinal_with a
given psi being Ordinal-Sequence such that A1: ( dom psi = a & rng psi c= On W & psi is increasing & On W = sup psi ) ; :: according to ORDINAL2:def 21 :: thesis: contradiction
On W c= W by ORDINAL2:9;
then ( dom psi in W & rng psi c= W ) by A1, XBOOLE_1:1;
then sup (rng psi) in W by Th12, ZF_REFLE:28;
then sup psi in On W by ORDINAL1:def 10;
hence contradiction by A1; :: thesis: verum