now :: thesis: for z being object holds
( ( not z in succRel 5 or z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) & ( ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) implies z in succRel 5 ) )

let z be object ; :: thesis: ( ( not z in succRel 5 or z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) & ( ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) implies z in succRel 5 ) )
thus ( not z in succRel 5 or z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) :: thesis: ( ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) implies z in succRel 5 )

proof

assume A1: z in succRel 5 ; :: thesis: ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] )
then consider x, y being object such that
A2: z = [x,y] by RELAT_1:def 1;
reconsider a = x, b = y as set by TARSKI:1;
[a,b] in succRel 5 by A1, A2;
then A3: ( a in 5 & b in 5 & b = succ a ) by Def1;

per cases then ( a = 0 or a = 1 or a = 2 or a = 3 or a = 4 ) by CARD_1:53, ENUMSET1:def 3;

suppose a = 0 ; :: thesis: ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] )

hence ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) by A2, A3; :: thesis: verum

end;

suppose a = 1 ; :: thesis: ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] )

hence ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) by A2, A3; :: thesis: verum

end;

suppose a = 2 ; :: thesis: ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] )

hence ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) by A2, A3; :: thesis: verum

end;

suppose a = 3 ; :: thesis: ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] )

hence ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) by A2, A3; :: thesis: verum

end;

suppose a = 4 ; :: thesis: ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] )

hence ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) by A3; :: thesis: verum

end;

end;

end;

assume A8: ( z = [0,1] or z = [1,2] or z = [2,3] or z = [3,4] ) ; :: thesis: z in succRel 5
( 1 = succ 0 & 1 in 5 & 2 = succ 1 & 2 in 5 & 3 = succ 2 & 3 in 5 & 4 = succ 3 & 4 in 5 ) by CARD_1:53, ENUMSET1:def 3;
hence z in succRel 5 by A8, Th4; :: thesis: verum

end;

hence succRel 5 = {[0,1],[1,2],[2,3],[3,4]} by ENUMSET1:def 2; :: thesis: verum