let A be Ordinal; :: thesis: for X being set st X c= A holds
On X = X
let X be set ; :: thesis: ( X c= A implies On X = X )
defpred S₁[ object ] means ( $1 in X & $1 is Ordinal );
assume X c= A ; :: thesis: On X = X
then A1: for x being object holds
( x in X iff S₁[x] ) ;
A2: for x being object holds
( x in On X iff S₁[x] ) by ORDINAL1:def 9;
thus On X = X from XBOOLE_0:sch 2(A2, A1); :: thesis: verum