let A be Ordinal; :: thesis: sup A = A
( On A = A & ( for B being Ordinal st On A c= B holds
A c= B ) ) by Th10;
hence sup A = A by Def7; :: thesis: verum