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