let W be Universe; :: thesis: for x being set holds
( x is Ordinal of W iff x in On W )
let x be set ; :: thesis: ( x is Ordinal of W iff x in On W )
( ( x is Ordinal of W implies ( x is Ordinal & x in W ) ) & ( x is Ordinal & x in W implies x is Ordinal of W ) & ( x in On W implies ( x is Ordinal & x in W ) ) & ( x is Ordinal & x in W implies x in On W ) ) by ORDINAL1:def 10, ORDINAL4:def 2;
hence ( x is Ordinal of W iff x in On W ) ; :: thesis: verum