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