let A be Ordinal; :: thesis: sup {A} = succ A
A1: On {A} c= succ A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in On {A} or x in succ A )
assume x in On {A} ; :: thesis: x in succ A
then x in {A} by ORDINAL1:def 9;
then x = A by TARSKI:def 1;
hence x in succ A by ORDINAL1:6; :: thesis: verum
end;
now :: thesis: for B being Ordinal st On {A} c= B holds
succ A c= B
A in {A} by TARSKI:def 1;
then A2: A in On {A} by ORDINAL1:def 9;
let B be Ordinal; :: thesis: ( On {A} c= B implies succ A c= B )
assume On {A} c= B ; :: thesis: succ A c= B
hence succ A c= B by A2, ORDINAL1:21; :: thesis: verum
end;
hence sup {A} = succ A by A1, Def3; :: thesis: verum