let A be Ordinal; :: thesis: for B, C being Ordinal holds
( [B,C] in succRel A iff ( succ B in A & C = succ B ) )
let B, C be Ordinal; :: thesis: ( [B,C] in succRel A iff ( succ B in A & C = succ B ) )

hereby :: thesis: ( succ B in A & C = succ B implies [B,C] in succRel A )

assume [B,C] in succRel A ; :: thesis: ( succ B in A & C = succ B )
then ( C in A & C = succ B ) by Def1;
hence ( succ B in A & C = succ B ) ; :: thesis: verum

end;

assume A1: ( succ B in A & C = succ B ) ; :: thesis: [B,C] in succRel A
B in succ B by ORDINAL1:6;
then B in A by A1, ORDINAL1:10;
hence [B,C] in succRel A by A1, Def1; :: thesis: verum