let A be Ordinal; :: thesis: On A = A
for x being object holds
( x in A iff ( x in A & x is Ordinal ) ) ;
hence On A = A by ORDINAL1:def 9; :: thesis: verum