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 and
A2: rng psi c= On W and
psi is increasing and
A3: On W = sup psi ; :: according to ORDINAL2:def 21 :: thesis: contradiction
On W c= W by ORDINAL2:9;
then rng psi c= W by A2, XBOOLE_1:1;
then sup (rng psi) in W by A1, Th12, ZF_REFLE:28;
then sup psi in On W by ORDINAL1:def 10;
hence contradiction by A3; :: thesis: verum