set A = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]};
set B = the InternalRel of (Necklace 4);
A1: [(0 + 1),0] in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } ;
A2: the InternalRel of (Necklace 4) = { [i,(i + 1)] where i is Element of NAT : i + 1 < 4 } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } by NECKLACE:18;
A3: the InternalRel of (Necklace 4) c= {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the InternalRel of (Necklace 4) or x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} )
assume A4: x in the InternalRel of (Necklace 4) ; :: thesis: x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
then consider y, z being object such that
A5: x = [y,z] by RELAT_1:def 1;

per cases ( x in { [i,(i + 1)] where i is Element of NAT : i + 1 < 4 } or x in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } ) by A2, A4, XBOOLE_0:def 3;

suppose x in { [i,(i + 1)] where i is Element of NAT : i + 1 < 4 } ; :: thesis: x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}

then consider i being Element of NAT such that
A6: [y,z] = [i,(i + 1)] and
A7: i + 1 < 4 by A5;
A8: y = i by A6, XTUPLE_0:1;
i + 1 < 1 + 3 by A7;
then i < 2 + 1 by XREAL_1:7;
then i <= 2 by NAT_1:13;
then not not y = 0 & ... & not y = 2 by A8;
hence x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} by A5, A6, A8, ENUMSET1:def 4; :: thesis: verum

end;

suppose x in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } ; :: thesis: x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}

then consider i being Element of NAT such that
A9: [y,z] = [(i + 1),i] and
A10: i + 1 < 4 by A5;
A11: z = i by A9, XTUPLE_0:1;
i + 1 < 1 + 3 by A10;
then i < 2 + 1 by XREAL_1:7;
then i <= 2 by NAT_1:13;
then not not z = 0 & ... & not z = 2 by A11;
hence x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} by A5, A9, A11, ENUMSET1:def 4; :: thesis: verum

end;

end;

end;

A12: [(2 + 1),(1 + 1)] in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } ;
A13: [(1 + 1),(2 + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < 4 } ;
A14: [(1 + 1),(0 + 1)] in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } ;
A15: [(0 + 1),(1 + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < 4 } ;
A16: [0,(0 + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < 4 } ;
{[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} c= the InternalRel of (Necklace 4)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} or x in the InternalRel of (Necklace 4) )
assume A17: x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} ; :: thesis: x in the InternalRel of (Necklace 4)

per cases ( x = [0,1] or x = [1,0] or x = [1,2] or x = [2,1] or x = [2,3] or x = [3,2] ) by A17, ENUMSET1:def 4;

suppose x = [0,1] ; :: thesis: x in the InternalRel of (Necklace 4)

hence x in the InternalRel of (Necklace 4) by A2, A16, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = [1,0] ; :: thesis: x in the InternalRel of (Necklace 4)

hence x in the InternalRel of (Necklace 4) by A2, A1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = [1,2] ; :: thesis: x in the InternalRel of (Necklace 4)

hence x in the InternalRel of (Necklace 4) by A2, A15, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = [2,1] ; :: thesis: x in the InternalRel of (Necklace 4)

hence x in the InternalRel of (Necklace 4) by A2, A14, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = [2,3] ; :: thesis: x in the InternalRel of (Necklace 4)

hence x in the InternalRel of (Necklace 4) by A2, A13, XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = [3,2] ; :: thesis: x in the InternalRel of (Necklace 4)

hence x in the InternalRel of (Necklace 4) by A2, A12, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence the InternalRel of (Necklace 4) = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} by A3, XBOOLE_0:def 10; :: thesis: verum