let A be Ordinal; :: thesis: On {A} = {A}
{A} c= succ A by XBOOLE_1:7;
hence On {A} = {A} by Th6; :: thesis: verum