theorem :: ZF_REFLE:7

for W being Universe
for x being set holds
( x is Ordinal of W iff x in On W ) by ORDINAL1:def 9;