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 17 :: thesis: contradiction
On W c= W by ORDINAL2:7;
then rng psi c= W by A2;
then sup (rng psi) in W by A1, Th11, ZF_REFLE:19;
then sup psi in On W by ORDINAL1:def 9;
hence contradiction by A3; :: thesis: verum