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

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