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

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

proof

assume A1: z in succRel 4 ; :: thesis: ( z = [0,1] or z = [1,2] or z = [2,3] )
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 4 by A1, A2;
then A3: ( a in 4 & b in 4 & b = succ a ) by Def1;

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

assume A7: ( z = [0,1] or z = [1,2] or z = [2,3] ) ; :: thesis: z in succRel 4
( 1 = succ 0 & 1 in 4 & 2 = succ 1 & 2 in 4 & 3 = succ 2 & 3 in 4 ) by CARD_1:52, ENUMSET1:def 2;
hence z in succRel 4 by A7, Th5; :: thesis: verum

end;

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