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

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

hereby :: thesis: ( z = [0,1] implies z in succRel 2 )

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

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

suppose a = 0 ; :: thesis: z = [0,1]

hence z = [0,1] by A2, A3; :: thesis: verum

end;

suppose a = 1 ; :: thesis: z = [0,1]

hence z = [0,1] by A3; :: thesis: verum

end;

end;

end;

assume A5: z = [0,1] ; :: thesis: z in succRel 2
( 1 = succ 0 & 1 in 2 ) by CARD_1:50, TARSKI:def 2;
hence z in succRel 2 by A5, Th4; :: thesis: verum

end;

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