take succ a ; :: according to ORDINAL2:def 4 :: thesis: not rng <%a%> c/= succ a
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng <%a%> or x in succ a )
assume x in rng <%a%> ; :: thesis: x in succ a
then x in {a} by AFINSQ_1:33;
then x = a by TARSKI:def 1;
hence x in succ a by ORDINAL1:6; :: thesis: verum