let W be Universe; :: thesis: for a being Ordinal of W holds Rank a in W
let a be Ordinal of W; :: thesis: Rank a in W
( W = Rank (On W) & a in On W ) by CLASSES2:50, ZF_REFLE:7;
hence Rank a in W by CLASSES1:36; :: thesis: verum