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

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

proof

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

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

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;

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