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:54, ZF_REFLE:8;
hence Rank a in W by CLASSES1:42; :: thesis: verum