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 Th8;
hence sup A = A by Def3; :: thesis: verum