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]}

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)

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

A12:
[(2 + 1),(1 + 1)] in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 }
;
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;

end;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;

end;

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;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

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;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

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

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
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)

end;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;

end;