set A = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]};
set B = the InternalRel of ();
A1: [(0 + 1),0] in { [(i + 1),i] where i is Element of NAT : i + 1 < 4 } ;
A2: the InternalRel of () = { [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 () 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 () or x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} )
assume A4: x in the InternalRel of () ; :: 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 ;
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 ;
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 ; :: 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 ;
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 ; :: 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 ()
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 () )
assume A17: x in {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} ; :: thesis: x in the InternalRel of ()
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 ;
suppose x = [0,1] ; :: thesis: x in the InternalRel of ()
hence x in the InternalRel of () by ; :: thesis: verum
end;
suppose x = [1,0] ; :: thesis: x in the InternalRel of ()
hence x in the InternalRel of () by ; :: thesis: verum
end;
suppose x = [1,2] ; :: thesis: x in the InternalRel of ()
hence x in the InternalRel of () by ; :: thesis: verum
end;
suppose x = [2,1] ; :: thesis: x in the InternalRel of ()
hence x in the InternalRel of () by ; :: thesis: verum
end;
suppose x = [2,3] ; :: thesis: x in the InternalRel of ()
hence x in the InternalRel of () by ; :: thesis: verum
end;
suppose x = [3,2] ; :: thesis: x in the InternalRel of ()
hence x in the InternalRel of () by ; :: thesis: verum
end;
end;
end;
hence the InternalRel of () = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]} by ; :: thesis: verum