set A = {[0 ,1],[1,0 ],[1,2],[2,1],[2,3],[3,2]};
set B = the InternalRel of (Necklace 4);
A1: 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:19;
A2: [0 ,(0 + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < 4 } ;
A3: [(0 + 1),0 ] in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } ;
A4: [(0 + 1),(1 + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < 4 } ;
A5: [(1 + 1),(0 + 1)] in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } ;
A6: [(1 + 1),(2 + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < 4 } ;
A7: [(2 + 1),(1 + 1)] in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } ;
A8: {[0 ,1],[1,0 ],[1,2],[2,1],[2,3],[3,2]} c= the InternalRel of (Necklace 4)

proof

let x be set ; :: 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 A9: 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 A9, ENUMSET1:def 4;

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

hence x in the InternalRel of (Necklace 4) by A1, A2, 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 A1, A3, 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 A1, A4, 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 A1, A5, 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 A1, A6, 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 A1, A7, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

the InternalRel of (Necklace 4) c= {[0 ,1],[1,0 ],[1,2],[2,1],[2,3],[3,2]}

proof

let x be set ; :: 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 A10: 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 set such that
A11: 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 A1, A10, 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
A12: ( [y,z] = [i,(i + 1)] & i + 1 < 4 ) by A11;
A13: ( y = i & z = i + 1 ) by A12, ZFMISC_1:33;
i + 1 < 1 + 3 by A12;
then i < 2 + 1 by XREAL_1:9;
then i <= 2 by NAT_1:13;
then ( y = 0 or y = 1 or y = 2 ) by A13, NAT_1:27;
hence x in {[0 ,1],[1,0 ],[1,2],[2,1],[2,3],[3,2]} by A11, A13, 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
A14: ( [y,z] = [(i + 1),i] & i + 1 < 4 ) by A11;
A15: ( y = i + 1 & z = i ) by A14, ZFMISC_1:33;
i + 1 < 1 + 3 by A14;
then i < 2 + 1 by XREAL_1:9;
then i <= 2 by NAT_1:13;
then ( z = 0 or z = 1 or z = 2 ) by A15, NAT_1:27;
hence x in {[0 ,1],[1,0 ],[1,2],[2,1],[2,3],[3,2]} by A11, A15, ENUMSET1:def 4; :: thesis: verum

end;

end;

end;

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