:: The Class of Series-Parallel Graphs, {I}
::  by Krzysztof Retel
::
:: Received November 18, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, CARD_1, ZFMISC_1, XBOOLE_0, SUBSET_1, ARYTM_3,
      FUNCT_3, FUNCT_1, RELAT_1, FUNCT_2, FUNCT_4, TARSKI, FUNCOP_1, ORDERS_2,
      STRUCT_0, RELAT_2, XXREAL_0, ARYTM_1, WELLORD1, CAT_1, SEQM_3, FINSET_1,
      ORDINAL1, CARD_2, SQUARE_1, NECKLACE;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, CARD_1, CARD_2,
      WELLORD1, FINSET_1, SQUARE_1, QUIN_1, ORDINAL1, NUMBERS, XCMPLX_0,
      REAL_1, NAT_1, NAT_D, RELAT_1, RELAT_2, FUNCT_3, FUNCOP_1, RELSET_1,
      FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, BINOP_1, XXREAL_0, STRUCT_0,
      ORDERS_2, WAYBEL_0, WAYBEL_1, ORDERS_3;
 constructors WELLORD1, REAL_1, SQUARE_1, NAT_1, QUIN_1, CARD_2, REALSET1,
      ORDERS_3, WAYBEL_1, NAT_D, RELSET_1;
 registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1,
      FUNCT_4, FINSET_1, XXREAL_0, XREAL_0, SQUARE_1, STRUCT_0, ORDERS_2,
      HILBERT3, CARD_1, RELAT_1, ZFMISC_1;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
 definitions WAYBEL_0, WAYBEL_1, ORDERS_3, STRUCT_0, FUNCT_1, RELAT_1, RELAT_2,
      XBOOLE_0, TARSKI, SQUARE_1, FUNCOP_1, WELLORD1, SUBSET_1, BINOP_1;
 theorems FUNCT_1, FUNCT_2, FUNCT_4, ENUMSET1, RELSET_1, ZFMISC_1, NAT_1,
      AXIOMS, CARD_1, WAYBEL_0, SUBSET_1, XBOOLE_0, XBOOLE_1, QUIN_1, WELLORD2,
      RELAT_1, FUNCT_3, TARSKI, FUNCOP_1, ORDERS_2, RELAT_2, ORDINAL1, CARD_2,
      SQUARE_1, WAYBEL_1, ORDERS_3, PARTFUN1, XREAL_1, XXREAL_0, FRECHET,
      XTUPLE_0;
 schemes NAT_1, FRAENKEL, FUNCT_7;

begin :: Preliminaries

reserve i,j,k,n for Nat;
reserve x,x1,x2,x3,y1,y2,y3 for set;

theorem
  4 = {0,1,2,3} by CARD_1:52;

theorem
  [:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[
  x2,y3],[x3,y1],[x3,y2],[x3,y3]}
proof
  thus [:{x1,x2,x3},{y1,y2,y3}:] = [:{x1}\/{x2,x3}, {y1,y2,y3}:] by ENUMSET1:2
    .= [:{x1}\/{x2,x3}, {y1}\/ {y2,y3}:] by ENUMSET1:2
    .= [:{x1},{y1}:] \/ [:{x1},{y2,y3}:] \/ [:{x2,x3},{y1}:] \/ [:{x2,x3},{
  y2,y3}:] by ZFMISC_1:98
    .= [:{x1},{y1}:] \/ [:{x1},{y2,y3}:] \/ [:{x2,x3},{y1}:] \/ ([:{x2},{y2,
  y3}:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:109
    .= {[x1,y1]} \/ [:{x1},{y2,y3}:] \/ [:{x2,x3},{y1}:] \/ ([:{x2},{y2,y3}
  :] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:29
    .= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ [:{x2,x3},{y1}:] \/ ([:{x2},{y2,y3}
  :] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30
    .= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]} \/ ([:{x2},{y2,y3
  }:] \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30
    .= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,
  y3]} \/ [:{x3},{y2,y3}:]) by ZFMISC_1:30
    .= {[x1,y1]} \/ {[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,
  y3]} \/ {[x3,y2],[x3,y3]}) by ZFMISC_1:30
    .= {[x1,y1],[x1,y2],[x1,y3]} \/ {[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,y3]}
  \/ {[x3,y2],[x3,y3]}) by ENUMSET1:2
    .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ ({[x2,y2],[x2,y3]} \/ {[
  x3,y2],[x3,y3]}) by ENUMSET1:9
    .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1]} \/ {[x2,y2],[x2,y3],[x3,y2]
  ,[x3,y3]} by ENUMSET1:5
    .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x3,y1],[x2,y2],[x2,y3], [x3,y2],[x3
  ,y3]} by ENUMSET1:81
    .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ {[x3,y1],[x2,y2],[x2,y3],[x3,y2]
  ,[x3,y3]} by ENUMSET1:80
    .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x3,y1],[x2,y2],[x2,y3]} \/ {[
  x3,y2],[x3,y3]}) by ENUMSET1:9
    .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x2,y2],[x2,y3],[x3,y1]} \/ {[
  x3,y2],[x3,y3]}) by ENUMSET1:59
    .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1]} \/ ({[x2,y2],[x2,y3],[x3,y1],[x3,y2
  ],[x3,y3]}) by ENUMSET1:9
    .= {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3], [x3,y1],[x3,y2],[x3
  ,y3]} by ENUMSET1:80;
end;

theorem Th3:
  for x being set, n be Nat holds x in n implies x is Nat
proof
  let x being set,n be Nat;
  reconsider m=n as Element of NAT by ORDINAL1:def 12;
  assume x in n;
  then x in {j where j is Element of NAT: j < m} by AXIOMS:4;
  then ex j being Element of NAT st x=j & j < m;
  hence thesis;
end;

theorem Th4:
  for x be non empty Nat holds 0 in x
proof
  let x be non empty Nat;
  reconsider n = x as Element of NAT by ORDINAL1:def 12;
  n = {i where i is Element of NAT: i < n} & 0 < n by AXIOMS:4,NAT_1:3;
  hence thesis;
end;

registration
  let X be set;
  cluster delta X -> one-to-one;
  coherence
  proof
    set f = delta X;
    let x1,x2 be set;
    assume that
A1: x1 in dom f & x2 in dom f and
A2: f.x1 = f.x2;
    f.x1 = [x1,x1] & f.x2 = [x2,x2] by A1,FUNCT_3:def 6;
    hence thesis by A2,XTUPLE_0:1;
  end;
end;

theorem Th5:
  for X being set holds card id X = card X
proof
  let X be set;
  id X in Funcs(X,X) by FUNCT_2:9;
  hence thesis by CARD_2:3;
end;

registration
  cluster trivial -> one-to-one for Function;
  coherence
  proof
    let f be Function such that
A1: f is trivial;
    let x1,x2 be set;
    assume that
A2: x1 in dom f and
A3: x2 in dom f and
    f.x1 = f.x2;
    reconsider f as trivial Function by A1;
    consider x being set such that
A4: dom f = {x} by A2,ZFMISC_1:131;
    x1 = x by A2,A4,TARSKI:def 1;
    hence thesis by A3,A4,TARSKI:def 1;
  end;
end;

theorem
  for f,g be Function st dom f misses dom g holds rng(f +* g) = rng f \/
  rng g by FRECHET:35,PARTFUN1:56;

theorem Th7:
  for f,g be one-to-one Function st dom f misses dom g & rng f
  misses rng g holds (f+*g)" = f" +* g"
proof
  let f,g be one-to-one Function such that
A1: dom f misses dom g and
A2: rng f misses rng g;
A3: (f+*g) is one-to-one by A2,FUNCT_4:92;
A4: for y,x being set holds y in rng (f+*g) & x = (f" +* g").y iff x in dom
  (f+*g) & y = (f+*g).x
  proof
    let y,x be set;
    thus y in rng (f+*g) & x = (f" +* g").y implies x in dom (f+*g) & y = (f+*
    g).x
    proof
A5:   rng (f+*g) c= rng f \/ rng g by FUNCT_4:17;
      assume that
A6:   y in rng (f+*g) and
A7:   x = (f" +* g").y;
      per cases by A6,A5,XBOOLE_0:def 3;
      suppose
A8:     y in rng f;
        then consider z being set such that
A9:     z in dom f and
A10:    y = f.z by FUNCT_1:def 3;
        dom (f +* g) = dom f \/ dom g by FUNCT_4:def 1;
        then
A11:    z in dom (f +* g) by A9,XBOOLE_0:def 3;
A12:    dom (f") = rng f & dom (g") = rng g by FUNCT_1:33;
        y = (f +* g).z & z = f".y by A1,A9,A10,FUNCT_1:32,FUNCT_4:16;
        hence thesis by A2,A7,A8,A11,A12,FUNCT_4:16;
      end;
      suppose
A13:    y in rng g;
A14:    dom (f") = rng f & dom (g") = rng g by FUNCT_1:33;
        consider z being set such that
A15:    z in dom g and
A16:    y = g.z by A13,FUNCT_1:def 3;
        z = g".y by A15,A16,FUNCT_1:32;
        then z = (g" +* f").y by A2,A13,A14,FUNCT_4:16;
        then
A17:    z = x by A2,A7,A14,FUNCT_4:35;
        dom (f +* g) = dom f \/ dom g & y = (g +* f).z by A1,A15,A16,FUNCT_4:16
,def 1;
        hence thesis by A1,A15,A17,FUNCT_4:35,XBOOLE_0:def 3;
      end;
    end;
    thus x in dom (f+*g) & y = (f+*g).x implies y in rng (f+*g) & x = (f" +* g
    ").y
    proof
A18:  dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
      assume that
A19:  x in dom (f+*g) and
A20:  y = (f+*g).x;
      per cases by A19,A18,XBOOLE_0:def 3;
      suppose
A21:    x in dom f;
        then not x in dom g by A1,XBOOLE_0:3;
        then
A22:    y = f.x by A20,FUNCT_4:11;
        then
A23:    x = f".y by A21,FUNCT_1:32;
A24:    dom (f") = rng f & dom (g") = rng g by FUNCT_1:33;
A25:    y in rng f by A21,A22,FUNCT_1:def 3;
        then y in rng f \/ rng g by XBOOLE_0:def 3;
        hence thesis by A1,A2,A25,A23,A24,FRECHET:35,FUNCT_4:16,PARTFUN1:56;
      end;
      suppose
A26:    x in dom g;
        then
A27:    y = g.x by A20,FUNCT_4:13;
        then
A28:    y in rng g by A26,FUNCT_1:def 3;
        then
A29:    y in rng f \/ rng g by XBOOLE_0:def 3;
A30:    dom (f") = rng f & dom (g") = rng g by FUNCT_1:33;
        x = g".y by A26,A27,FUNCT_1:32;
        then x = (g" +* f").y by A2,A28,A30,FUNCT_4:16;
        hence thesis by A1,A2,A29,A30,FRECHET:35,FUNCT_4:35,PARTFUN1:56;
      end;
    end;
  end;
  dom (f" +* g") = dom (f") \/ dom (g") by FUNCT_4:def 1
    .= rng f \/ dom (g") by FUNCT_1:33
    .= rng f \/ rng g by FUNCT_1:33
    .= rng (f +* g) by A1,FRECHET:35,PARTFUN1:56;
  hence thesis by A3,A4,FUNCT_1:32;
end;

theorem
  for A,a,b being set holds (A --> a) +* (A --> b) = A --> b
proof
  let A,a,b be set;
  set g = A --> b;
  dom g = A by FUNCOP_1:13;
  then dom (A --> a) c= dom g;
  hence thesis by FUNCT_4:19;
end;

theorem Th9:
  for a,b being set holds (a .--> b)" = b .--> a
proof
  let a,b be set;
  set f = a .--> b, g = b .--> a;
A1: for y,x be set holds y in rng f & x = g.y iff x in dom f & y = f.x
  proof
    let y,x be set;
    thus y in rng f & x = g.y implies x in dom f & y = f.x
    proof
      assume that
A2:   y in rng f and
A3:   x = g.y;
A4:   y in {b} by A2,FUNCOP_1:8;
      then
A5:   x = g.b by A3,TARSKI:def 1
        .= a by FUNCOP_1:72;
      then
A6:   x in {a} by TARSKI:def 1;
      f.x = b by A5,FUNCOP_1:72
        .= y by A4,TARSKI:def 1;
      hence thesis by A6,FUNCOP_1:13;
    end;
    assume that
A7: x in dom f and
A8: y = f.x;
A9: x in {a} by A7;
    then
A10: y = f.a by A8,TARSKI:def 1
      .= b by FUNCOP_1:72;
    then
A11: y in {b} by TARSKI:def 1;
    g.y = a by A10,FUNCOP_1:72
      .= x by A9,TARSKI:def 1;
    hence thesis by A11,FUNCOP_1:8;
  end;
  dom g = {b} by FUNCOP_1:13
    .= rng f by FUNCOP_1:8;
  hence thesis by A1,FUNCT_1:32;
end;

theorem Th10:
  for a,b,c,d being set st a = b iff c = d holds (a,b) --> (c,d)"
  = (c,d) --> (a,b)
proof
  let a,b,c,d being set such that
A1: a = b iff c = d;
  per cases by A1;
  suppose
A2: a = b & c = d;
    (a,a) --> (d,d)" = (a .--> d)" by FUNCT_4:81
      .= (d .--> a) by Th9
      .= (d,d) --> (a,a) by FUNCT_4:81;
    hence thesis by A2;
  end;
  suppose
A3: a <> b & c <> d;
    set f = (a,b) --> (c,d), g = (c,d) --> (a,b);
A4: for y,x be set holds y in rng f & x = g.y iff x in dom f & y = f.x
    proof
      let y,x be set;
A5:   x in dom f & y = f.x implies y in rng f & x = g.y
      proof
        assume that
A6:     x in dom f and
A7:     y = f.x;
A8:     x in {a,b} by A6,FUNCT_4:62;
        per cases by A8,TARSKI:def 2;
        suppose
A9:       x = a;
          then
A10:      y = c by A3,A7,FUNCT_4:63;
          then y in {c,d} by TARSKI:def 2;
          hence thesis by A3,A9,A10,FUNCT_4:63,64;
        end;
        suppose
A11:      x = b;
          then
A12:      y = d by A7,FUNCT_4:63;
          then y in {c,d} by TARSKI:def 2;
          hence thesis by A3,A11,A12,FUNCT_4:63,64;
        end;
      end;
      y in rng f & x = g.y implies x in dom f & y = f.x
      proof
        assume that
A13:    y in rng f and
A14:    x = g.y;
A15:    y in {c,d} by A3,A13,FUNCT_4:64;
        per cases by A15,TARSKI:def 2;
        suppose
A16:      y = c;
          then
A17:      x = a by A3,A14,FUNCT_4:63;
          then x in {a,b} by TARSKI:def 2;
          hence thesis by A3,A16,A17,FUNCT_4:62,63;
        end;
        suppose
A18:      y = d;
          then
A19:      x = b by A14,FUNCT_4:63;
          then x in {a,b} by TARSKI:def 2;
          hence thesis by A18,A19,FUNCT_4:62,63;
        end;
      end;
      hence thesis by A5;
    end;
A20: f is one-to-one
    proof
A21:  dom f = {a,b} by FUNCT_4:62;
      let x1,x2 being set such that
A22:  x1 in dom f & x2 in dom f and
A23:  f.x1 = f.x2;
      per cases by A22,A21,TARSKI:def 2;
      suppose
        x1 = a & x2 = a or x1 = b & x2 = b;
        hence thesis;
      end;
      suppose
A24:    x1 = a & x2 = b;
        then f.x1 = c by A3,FUNCT_4:63;
        hence thesis by A3,A23,A24,FUNCT_4:63;
      end;
      suppose
A25:    x1 = b & x2 = a;
        then f.x1 = d by FUNCT_4:63;
        hence thesis by A3,A23,A25,FUNCT_4:63;
      end;
    end;
    dom g = {c,d} by FUNCT_4:62
      .= rng f by A3,FUNCT_4:64;
    hence thesis by A20,A4,FUNCT_1:32;
  end;
end;

scheme
  Convers{X()-> non empty set, R() -> Relation, F,G(set)-> set, P[set]}: R()~
  ={[F(x),G(x)] where x is Element of X(): P[x]}
provided
A1: R() = {[G(x),F(x)] where x is Element of X(): P[x]}
proof
  set S = {[F(x),G(x)] where x is Element of X(): P[x]};
  S is Relation-like
  proof
    let x being set;
    assume x in S;
    then ex y being Element of X() st x = [F(y),G(y)] & P[y];
    hence thesis;
  end;
  then reconsider S9 = S as Relation;
A2: for x,y being set holds [y,x] in R() implies [x,y] in S9
  proof
    let x,y being set;
    assume [y,x] in R();
    then consider z being Element of X() such that
A3: [y,x] = [G(z),F(z)] and
A4: P[z] by A1;
    y = G(z) & x = F(z) by A3,XTUPLE_0:1;
    hence thesis by A4;
  end;
  for x,y being set holds [x,y] in S9 implies [y,x] in R()
  proof
    let x,y being set;
    assume [x,y] in S9;
    then consider z being Element of X() such that
A5: [x,y] = [F(z),G(z)] and
A6: P[z];
    x = F(z) & y = G(z) by A5,XTUPLE_0:1;
    hence thesis by A1,A6;
  end;
  hence thesis by A2,RELAT_1:def 7;
end;

theorem
  for i,j,n be Nat holds i < j & j in n implies i in n
proof
  let i,j,n be Nat;
  assume that
A1: i < j and
A2: j in n;
  j < n by A2,NAT_1:44;
  then i < n by A1,XXREAL_0:2;
  hence thesis by NAT_1:44;
end;

begin   :: Auxiliary Concepts

definition
  let R,S be RelStr;

  pred S embeds R means
  :Def1:
  ex f being Function of R,S st f is one-to-one &
for x,y being Element of R holds [x,y] in the InternalRel of R iff [f.x,f.y] in
  the InternalRel of S;
end;

definition
  let R,S be non empty RelStr;
  redefine pred S embeds R;
  reflexivity
  proof
    let R be non empty RelStr;
    set f = id the carrier of R;
    reconsider f as Function of R,R;
    take f;
    thus f is one-to-one;
    let x,y be Element of R;
    x = f.x by FUNCT_1:18;
    hence thesis by FUNCT_1:18;
  end;
end;

theorem Th12:
  for R,S,T be non empty RelStr holds R embeds S & S embeds T
  implies R embeds T
proof
  let R,S,T be non empty RelStr;
  assume R embeds S;
  then consider f being Function of S,R such that
A1: f is one-to-one and
A2: for x,y being Element of S holds [x,y] in the InternalRel of S iff [
  f.x,f.y] in the InternalRel of R by Def1;
  assume S embeds T;
  then consider g being Function of T,S such that
A3: g is one-to-one and
A4: for x,y being Element of T holds [x,y] in the InternalRel of T iff [
  g.x,g.y] in the InternalRel of S by Def1;
  reconsider h=f*g as Function of T,R;
  take h;
  thus h is one-to-one by A1,A3;
  thus for x,y being Element of T holds [x,y] in the InternalRel of T iff [h.x
  ,h.y] in the InternalRel of R
  proof
    let x,y be Element of T;
    thus [x,y] in the InternalRel of T implies [h.x,h.y] in the InternalRel of
    R
    proof
      assume [x,y] in the InternalRel of T;
      then
A5:   [g.x,g.y] in the InternalRel of S by A4;
      h.x=f.(g.x) & h.y=f.(g.y) by FUNCT_2:15;
      hence thesis by A2,A5;
    end;
    thus [h.x,h.y] in the InternalRel of R implies [x,y] in the InternalRel of
    T
    proof
A6:   h.x=f.(g.x) & h.y=f.(g.y) by FUNCT_2:15;
      assume [h.x,h.y] in the InternalRel of R;
      then [g.x,g.y] in the InternalRel of S by A2,A6;
      hence thesis by A4;
    end;
  end;
end;

definition
  let R,S be non empty RelStr;
  pred R is_equimorphic_to S means
  :Def2:
  R embeds S & S embeds R;
  reflexivity;
  symmetry;
end;

theorem
  for R,S,T be non empty RelStr holds R is_equimorphic_to S & S
  is_equimorphic_to T implies R is_equimorphic_to T
proof
  let R,S,T be non empty RelStr;
  assume
A1: R is_equimorphic_to S & S is_equimorphic_to T;
  then S embeds R & T embeds S by Def2;
  then
A2: T embeds R by Th12;
  R embeds S & S embeds T by A1,Def2;
  then R embeds T by Th12;
  hence thesis by A2,Def2;
end;

notation
  let R be non empty RelStr;
  antonym R is parallel for R is connected;
end;

definition
  let R be RelStr;
  attr R is symmetric means
  :Def3:
  the InternalRel of R is_symmetric_in the carrier of R;
end;

definition
  let R be RelStr;
  attr R is asymmetric means
  :Def4:
  the InternalRel of R is asymmetric;
end;

theorem
  for R be RelStr st R is asymmetric holds the InternalRel of R misses (
  the InternalRel of R)~
proof
  let R be RelStr;
  assume R is asymmetric;
  then the InternalRel of R is asymmetric by Def4;
  then
A1: the InternalRel of R is_asymmetric_in field (the InternalRel of R) by
RELAT_2:def 13;
  assume the InternalRel of R meets (the InternalRel of R)~;
  then consider x being set such that
A2: x in the InternalRel of R and
A3: x in (the InternalRel of R)~ by XBOOLE_0:3;
  consider y,z being set such that
A4: x = [y,z] by A3,RELAT_1:def 1;
A5: z in field the InternalRel of R by A2,A4,RELAT_1:15;
  [z,y] in the InternalRel of R & y in field the InternalRel of R by A2,A3,A4,
RELAT_1:15,def 7;
  hence contradiction by A2,A4,A1,A5,RELAT_2:def 5;
end;

definition
  let R be RelStr;
  attr R is irreflexive means
  for x being set st x in the carrier of R holds
  not [x,x] in the InternalRel of R;
end;

definition
  let n be Nat;
  func n-SuccRelStr -> strict RelStr means
  :Def6:
  the carrier of it = n & the
  InternalRel of it = {[i,i+1] where i is Element of NAT:i+1 < n};
  existence
  proof
    set r = {[i,i+1] where i is Element of NAT:i+1 < n};
    r c= [:n,n:]
    proof
      let x be set;
      assume x in r;
      then consider i be Element of NAT such that
A1:   x = [i,i+1] and
A2:   i+1 < n;
      i <= i+1 by NAT_1:11;
      then i < n by A2,XXREAL_0:2;
      then
A3:   i in n by NAT_1:44;
      i+1 in n by A2,NAT_1:44;
      hence thesis by A1,A3,ZFMISC_1:87;
    end;
    then reconsider r as Relation of n;
    take RelStr (#n,r#);
    thus thesis;
  end;
  uniqueness;
end;

theorem
  for n be Nat holds n-SuccRelStr is asymmetric
proof
  let n be Nat;
  set S = n-SuccRelStr;
  the InternalRel of S is_asymmetric_in field the InternalRel of S
  proof
    let x,y be set;
    assume that
    x in field the InternalRel of S and
    y in field the InternalRel of S and
A1: [x,y] in the InternalRel of S;
A2: [x,y] in {[i,i+1] where i is Element of NAT:i+1 < n} by A1,Def6;
    assume [y,x] in the InternalRel of S;
    then [y,x] in {[i9,i9+1] where i9 is Element of NAT:i9+1 < n} by Def6;
    then consider j be Element of NAT such that
A3: [y,x] = [j,j+1] and
    j+1<n;
A4: y = j & x = j+1 by A3,XTUPLE_0:1;
    consider i be Element of NAT such that
A5: [x,y] = [i,i+1] and
    i+1<n by A2;
    x = i & y = i+1 by A5,XTUPLE_0:1;
    hence contradiction by A4;
  end;
  hence the InternalRel of S is asymmetric by RELAT_2:def 13;
end;

theorem Th16:
  n > 0 implies card the InternalRel of n-SuccRelStr = n-1
proof
  deffunc F(Element of NAT) = [$1,$1+1];
  defpred P[Element of NAT] means $1+1<n;
  defpred Q[set] means $1 in n-'1;
A1: n-'1 c= NAT;
  assume
A2: n > 0;
  then
A3: n >= 0+1 by NAT_1:13;
A4: i in n-'1 implies i+1<n
  proof
    assume i in n-'1;
    then
A5: i < n-'1 by NAT_1:44;
    n >= 0+1 by A2,NAT_1:13;
    then i < n-1 by A5,XREAL_1:233;
    hence thesis by XREAL_1:20;
  end;
A6: for i being Element of NAT holds P[i] iff Q[i]
  proof
    let i be Element of NAT;
    thus i+1<n implies i in n-'1
    proof
      assume i+1<n;
      then i < n-1 by XREAL_1:20;
      then i < n-'1 by A3,XREAL_1:233;
      hence thesis by NAT_1:44;
    end;
    thus thesis by A4;
  end;
A7: {F(i) where i is Element of NAT: P[i]} = {F(i) where i is Element of
  NAT: Q[i]} from FRAENKEL:sch 3(A6);
  deffunc F(Element of NAT) = [$1,$1+1];
A8: for d1,d2 being Element of NAT st F(d1) = F(d2) holds d1 = d2 by XTUPLE_0:1
;
A9: n-'1, {F(i) where i is Element of NAT: i in n-'1} are_equipotent from
  FUNCT_7:sch 4(A1,A8);
  thus card the InternalRel of n-SuccRelStr = card {[i,i+1] where i is Element
  of NAT:i+1 < n} by Def6
    .= card (n-'1) by A7,A9,CARD_1:5
    .= n-'1 by CARD_1:def 2
    .= n-1 by A3,XREAL_1:233;
end;

definition
  let R be RelStr;
  func SymRelStr R -> strict RelStr means
  :Def7:
  the carrier of it = the
  carrier of R & the InternalRel of it = (the InternalRel of R) \/ (the
  InternalRel of R)~;
  existence
  proof
    take RelStr (#the carrier of R, (the InternalRel of R) \/ (the InternalRel
      of R)~ #);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let R be RelStr;
  cluster SymRelStr R -> symmetric;
  coherence
  proof
    let x,y be set;
    assume that
    x in the carrier of SymRelStr R and
    y in the carrier of SymRelStr R and
A1: [x,y] in the InternalRel of SymRelStr R;
A2: [x,y] in (the InternalRel of R) \/ (the InternalRel of R)~ by A1,Def7;
    per cases by A2,XBOOLE_0:def 3;
    suppose
      [x,y] in the InternalRel of R;
      then [y,x] in (the InternalRel of R)~ by RELAT_1:def 7;
      then [y,x] in (the InternalRel of R) \/ (the InternalRel of R)~ by
XBOOLE_0:def 3;
      hence thesis by Def7;
    end;
    suppose
      [x,y] in (the InternalRel of R)~;
      then [y,x] in the InternalRel of R by RELAT_1:def 7;
      then [y,x] in (the InternalRel of R) \/ (the InternalRel of R)~ by
XBOOLE_0:def 3;
      hence thesis by Def7;
    end;
  end;
end;

registration
  cluster non empty symmetric for RelStr;
  existence
  proof
    set R = {[0,0]};
    R c= [:{0},{0}:] by ZFMISC_1:29;
    then reconsider R = {[0,0]} as Relation of {0};
    take S = RelStr (#{0},R#);
    thus S is non empty;
    thus the InternalRel of S is_symmetric_in the carrier of S
    proof
      let x,y be set;
      assume that
      x in the carrier of S and
      y in the carrier of S and
A1:   [x,y] in the InternalRel of S;
      x = 0 & y = 0 by A1,ZFMISC_1:28;
      then [y,x] in [:{0},{0}:] by ZFMISC_1:28;
      hence thesis by ZFMISC_1:29;
    end;
  end;
end;

registration
  let R be symmetric RelStr;
  cluster the InternalRel of R -> symmetric;
  coherence
  proof
    let x,y be set;
    assume
A1: x in field the InternalRel of R & y in field the InternalRel of R
    & [x,y ] in the InternalRel of R;
    the InternalRel of R is_symmetric_in the carrier of R & field the
InternalRel of R c= (the carrier of R) \/ the carrier of R by Def3,RELSET_1:8;
    hence thesis by A1,RELAT_2:def 3;
  end;
end;

Lm1: for S,R being non empty RelStr holds S,R are_isomorphic implies card (the
InternalRel of S) = card (the InternalRel of R)
proof
  let S,R being non empty RelStr;
  set A = the carrier of S, B = the carrier of R, C = the InternalRel of S, D
  = the InternalRel of R;
  reconsider C as set;
  assume S,R are_isomorphic;
  then consider f being Function of S,R such that
A1: f is isomorphic by WAYBEL_1:def 8;
  reconsider f9=f as one-to-one Function by A1,WAYBEL_0:def 38;
A2: [:f9,f9:] is one-to-one;
A3: dom f = A by FUNCT_2:def 1;
A4: rng f = B by A1,WAYBEL_0:66;
A5: f is monotone by A1,WAYBEL_0:def 38;
  the InternalRel of S,the InternalRel of R are_equipotent
  proof
    set P = [:f,f:];
    set F = [:f,f:]|C;
    set L = dom F;
A6: dom F = dom ([:f,f:]) /\ C by RELAT_1:61
      .= [:dom f, dom f:] /\ C by FUNCT_3:def 8
      .= C by A3,XBOOLE_1:28;
A7: rng F c= D
    proof
      let a be set;
      assume a in rng F;
      then consider x being set such that
A8:   x in dom F and
A9:   a = F.x by FUNCT_1:def 3;
      consider x1,x2 being set such that
A10:  x = [x1,x2] by A8,RELAT_1:def 1;
A11:    x in dom [:f,f:] by A8,RELAT_1:57;
      then reconsider X1 = x1, X2 = x2 as Element of S by A10,ZFMISC_1:87;
      X1 <= X2 by A8,A10,ORDERS_2:def 5;
      then
A12:  f.X1 <= f.X2 by A5,ORDERS_3:def 5;
A13:  a = P.(x1,x2) by A8,A9,A10,FUNCT_1:47;
      x1 in dom f & x2 in dom f by A3,A10,A11,ZFMISC_1:87;
      then a = [f.x1,f.x2] by A13,FUNCT_3:def 8;
      hence thesis by A12,ORDERS_2:def 5;
    end;
    then reconsider F as Function of L,[:B,B:] by FUNCT_2:2,XBOOLE_1:1;
    reconsider F as Function of L,D by A7,FUNCT_2:6;
A14: rng F = D
    proof
      thus rng F c= D by A7;
      let x be set;
      assume
A15:  x in D;
      then consider x1,x2 being set such that
A16:  x = [x1,x2] by RELAT_1:def 1;
      reconsider x19 = x1, x29 = x2 as Element of B by A15,A16,ZFMISC_1:87;
      x1 in B by A15,A16,ZFMISC_1:87;
      then consider X1 being set such that
A17:  X1 in dom f and
A18:  x1 = f.X1 by A4,FUNCT_1:def 3;
      x2 in B by A15,A16,ZFMISC_1:87;
      then consider X2 being set such that
A19:  X2 in dom f and
A20:  x2 = f.X2 by A4,FUNCT_1:def 3;
      reconsider X19 = X1, X29 = X2 as Element of S by A17,A19;
      x19 <= x29 by A15,A16,ORDERS_2:def 5;
      then X19 <= X29 by A1,A18,A20,WAYBEL_0:66;
      then
A21:  [X1,X2] in C by ORDERS_2:def 5;
      set Pi = [X1,X2];
      Pi in [:dom f,dom f:] by A17,A19,ZFMISC_1:87;
      then x = [:f,f:].(X1,X2) by A16,A18,A20,FUNCT_3:65
        .= F.[X1,X2] by A6,A21,FUNCT_1:47;
      hence thesis by A6,A21,FUNCT_1:def 3;
    end;
    F is one-to-one by A2,FUNCT_1:52;
    hence thesis by A6,A14,WELLORD2:def 4;
  end;
  hence thesis by CARD_1:5;
end;

definition
  let R be RelStr;
  func ComplRelStr R -> strict RelStr means
  :Def8:
  the carrier of it = the
  carrier of R & the InternalRel of it = (the InternalRel of R)` \ id (the
  carrier of R);
  existence
  proof
    reconsider r = (the InternalRel of R)` \ id (the carrier of R) as Relation
    of the carrier of R;
    take RelStr(#the carrier of R, r#);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let R be non empty RelStr;
  cluster ComplRelStr R -> non empty;
  coherence
  proof
    the carrier of ComplRelStr R = the carrier of R by Def8;
    hence the carrier of ComplRelStr R is non empty;
  end;
end;

theorem Th17:
  for S,R being RelStr holds S,R are_isomorphic implies card the
  InternalRel of S = card the InternalRel of R
proof
  let S,R be RelStr;
  assume
A1: S,R are_isomorphic;
  then
A2: ex f being Function of S,R st f is isomorphic by WAYBEL_1:def 8;
  per cases by A2,WAYBEL_0:def 38;
  suppose
    S is non empty & R is non empty;
    hence thesis by A1,Lm1;
  end;
  suppose
    S is empty & R is empty;
    then reconsider S, R as empty RelStr;
    the InternalRel of S = {} & the InternalRel of R = {};
    hence thesis;
  end;
end;

begin   :: Necklace n

definition
  let n be Nat;
  func Necklace n -> strict RelStr equals
  SymRelStr(n-SuccRelStr);
  coherence;
end;

registration
  let n be Nat;
  cluster Necklace n -> symmetric;
  coherence;
end;

theorem Th18:
  the InternalRel of Necklace n = {[i,i+1] where i is Element of
  NAT:i+1 < n} \/ {[i+1,i] where i is Element of NAT:i+1 < n}
proof
  set I = {[i,i+1] where i is Element of NAT:i+1 < n};
  I is Relation-like
  proof
    let x be set;
    assume x in I;
    then ex i being Element of NAT st x = [i,i+1] & i+1<n;
    hence thesis;
  end;
  then reconsider I as Relation;
  set B = n-SuccRelStr;
  deffunc F(Element of NAT) = $1;
  deffunc G(Element of NAT) = $1+1;
  defpred P[Element of NAT] means $1+1 < n;
  set R = {[G(i),F(i)] where i is Element of NAT: P[i]};
A1: I = {[F(i),G(i)] where i is Element of NAT: P[i]};
A2: I~ = R from Convers(A1);
  the InternalRel of B = I by Def6;
  hence thesis by A2,Def7;
end;

theorem Th19:
  for x be set holds x in the InternalRel of Necklace n iff ex i
  being Element of NAT st i+1 < n & (x = [i,i+1] or x = [i+1,i])
proof
  let x be set;
  thus x in the InternalRel of Necklace n implies ex i being Element of NAT st
  i+1< n & (x = [i,i+1] or x = [i+1,i])
  proof
    assume x in the InternalRel of Necklace n;
    then
    x in ({[i,i+1] where i is Element of NAT:i+1 < n} \/ {[i+1,i] where i
    is Element of NAT:i+1 < n } ) by Th18;
    then x in {[i,i+1] where i is Element of NAT:i+1 < n} or x in {[i+1,i]
    where i is Element of NAT:i+1 < n} by XBOOLE_0:def 3;
    then (ex i being Element of NAT st x = [i,i+1] & i+1<n) or ex i being
    Element of NAT st x = [i+1,i] & i+1<n;
    hence thesis;
  end;
  thus (ex i being Element of NAT st i+1 < n & (x = [i,i+1] or x = [i+1,i]))
  implies x in the InternalRel of Necklace n
  proof
    given i being Element of NAT such that
A1: i+1 < n &( x=[i,i+1] or x=[i+1,i]);
    per cases by A1;
    suppose
      i+1 < n & x=[i,i+1];
      then x in {[j,j+1] where j is Element of NAT:j+1 < n};
      then
      x in ({[j,j+1] where j is Element of NAT:j+1 < n} \/ {[j+1,j] where
      j is Element of NAT:j+1 < n}) by XBOOLE_0:def 3;
      hence thesis by Th18;
    end;
    suppose
      i+1 < n & x=[i+1,i];
      then x in {[j+1,j] where j is Element of NAT:j+1 < n};
      then
      x in ({[j+1,j] where j is Element of NAT:j+1 < n} \/ {[j,j+1] where
      j is Element of NAT:j+1 < n}) by XBOOLE_0:def 3;
      hence thesis by Th18;
    end;
  end;
end;

registration
  let n be Nat;
  cluster Necklace n -> irreflexive;
  coherence
  proof
    let x be set;
    set A = Necklace n;
    assume x in the carrier of A;
A1: the InternalRel of Necklace n = {[i,i+1] where i is Element of NAT:i+1
    < n} \/ {[i+1,i] where i is Element of NAT:i+1 < n} by Th18;
    assume
A2: [x,x] in the InternalRel of A;
    per cases by A2,A1,XBOOLE_0:def 3;
    suppose
      [x,x] in {[i,i+1] where i is Element of NAT:i+1 < n};
      then consider i being Element of NAT such that
A3:   [x,x] = [i,i+1] and
      i+1 < n;
      x = i & x = i+1 by A3,XTUPLE_0:1;
      hence contradiction;
    end;
    suppose
      [x,x] in {[i+1,i] where i is Element of NAT:i+1 < n};
      then consider i being Element of NAT such that
A4:   [x,x] = [i+1,i] and
      i+1 < n;
      x = i+1 & x = i by A4,XTUPLE_0:1;
      hence contradiction;
    end;
  end;
end;

theorem Th20:
  for n be Nat holds the carrier of Necklace n = n
proof
  let n be Nat;
  the carrier of Necklace n = the carrier of n-SuccRelStr by Def7
    .= n by Def6;
  hence thesis;
end;

registration
  let n be non empty Nat;
  cluster Necklace n -> non empty;
  coherence by Th20;
end;

registration
  let n be Nat;
  cluster the carrier of Necklace n -> finite;
  coherence by Th20;
end;

theorem Th21:
  for n,i be Nat st i+1 < n holds [i,i+1] in the InternalRel of Necklace n
proof
  let n,j be Nat such that
A1: j+1 < n;
  reconsider j as Element of NAT by ORDINAL1:def 12;
A2: [j,j+1] in {[i,i+1] where i is Element of NAT:i+1 < n} by A1;
  the InternalRel of Necklace n = {[i,i+1] where i is Element of NAT:i+1 <
  n} \/ {[i+1,i] where i is Element of NAT:i+1 < n} by Th18;
  hence thesis by A2,XBOOLE_0:def 3;
end;

theorem Th22:
  for n be Nat, i being Nat st i in the carrier of Necklace n holds i < n
proof
  let n be Nat, i being Nat;
  assume i in the carrier of Necklace n;
  then i in n by Th20;
  hence thesis by NAT_1:44;
end;

theorem
  for n be non empty Nat holds Necklace n is connected
proof
  let n be non empty Nat;
  given X,Y being Subset of Necklace n such that
A1: X <> {} and
A2: Y <> {} and
A3: [#] Necklace n = X \/ Y and
A4: X misses Y and
A5: the InternalRel of Necklace n = (the InternalRel of Necklace n)|_2 X
  \/ (the InternalRel of Necklace n) |_2 Y;
A6: the carrier of Necklace n = n & 0 in n by Th4,Th20;
  per cases by A3,A6,XBOOLE_0:def 3;
  suppose
A7: 0 in X;
    defpred P[Nat] means $1 in Y;
    consider x being Element of Necklace n such that
A8: x in Y by A2,SUBSET_1:4;
    x in the carrier of Necklace n;
    then x in n by Th20;
    then x is natural by Th3;
    then
A9: ex x being Nat st P[x] by A8;
    consider k being Nat such that
A10: P[k] and
A11: for i being Nat st P[i] holds k <= i from NAT_1:sch 5 (A9);
    k <> 0 by A4,A7,A10,XBOOLE_0:3;
    then consider i being Nat such that
A12: k = i+1 by NAT_1:6;
    reconsider i as Element of NAT by ORDINAL1:def 12;
A13: not i in Y by A11,A12,XREAL_1:29;
A14: not i+1 in X by A4,A10,A12,XBOOLE_0:3;
A15: [i,i+1] in the InternalRel of Necklace n by A10,A12,Th21,Th22;
    now
      per cases by A5,A15,XBOOLE_0:def 3;
      suppose
        [i,i+1] in (the InternalRel of Necklace n) |_2 X;
        then [i,i+1] in [:X,X:] by XBOOLE_0:def 4;
        hence contradiction by A14,ZFMISC_1:87;
      end;
      suppose
        [i,i+1] in (the InternalRel of Necklace n) |_2 Y;
        then [i,i+1] in [:Y,Y:] by XBOOLE_0:def 4;
        hence contradiction by A13,ZFMISC_1:87;
      end;
    end;
    hence contradiction;
  end;
  suppose
A16: 0 in Y;
    defpred P[Nat] means $1 in X;
    consider y being Element of Necklace n such that
A17: y in X by A1,SUBSET_1:4;
    y in the carrier of Necklace n;
    then y in n by Th20;
    then y is natural by Th3;
    then
A18: ex y being Nat st P[y] by A17;
    consider k being Nat such that
A19: P[k] and
A20: for i being Nat st P[i] holds k <= i from NAT_1:sch 5 (A18);
    k <> 0 by A4,A16,A19,XBOOLE_0:3;
    then consider i being Nat such that
A21: k = i+1 by NAT_1:6;
    reconsider i as Element of NAT by ORDINAL1:def 12;
A22: not i in X by A20,A21,XREAL_1:29;
A23: not i+1 in Y by A4,A19,A21,XBOOLE_0:3;
A24: [i,i+1] in the InternalRel of Necklace n by A19,A21,Th21,Th22;
    now
      per cases by A5,A24,XBOOLE_0:def 3;
      suppose
        [i,i+1] in (the InternalRel of Necklace n) |_2 Y;
        then [i,i+1] in [:Y,Y:] by XBOOLE_0:def 4;
        hence contradiction by A23,ZFMISC_1:87;
      end;
      suppose
        [i,i+1] in (the InternalRel of Necklace n) |_2 X;
        then [i,i+1] in [:X,X:] by XBOOLE_0:def 4;
        hence contradiction by A22,ZFMISC_1:87;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th24:
  for i,j being Nat st [i,j] in the InternalRel of Necklace n
  holds i = j + 1 or j = i + 1
proof
  let i,j be Nat;
  assume [i,j] in the InternalRel of Necklace n;
  then
  [i,j] in {[k,k+1] where k is Element of NAT:k+1 < n} \/ {[l+1,l] where l
  is Element of NAT:l+1 < n} by Th18;
  then
A1: [i,j] in {[k,k+1] where k is Element of NAT:k+1 < n} or [i,j] in {[k+1,k
  ] where k is Element of NAT:k+1 < n} by XBOOLE_0:def 3;
  i + 1 = j or j + 1 = i
  proof
    per cases by A1;
    suppose
      ex k being Element of NAT st [i,j] = [k,k+1] & k+1 < n;
      then consider k such that
A2:   [i,j] = [k,k+1] and
      k+1 < n;
      i = k by A2,XTUPLE_0:1;
      hence thesis by A2,XTUPLE_0:1;
    end;
    suppose
      ex k being Element of NAT st [i,j] = [k+1,k] & k+1 < n;
      then consider k such that
A3:   [i,j] = [k+1,k] and
      k+1 < n;
      i = k+1 by A3,XTUPLE_0:1;
      hence thesis by A3,XTUPLE_0:1;
    end;
  end;
  hence thesis;
end;

theorem Th25:
  for i,j being Nat st (i = j + 1 or j = i + 1) & i in the carrier
  of Necklace n & j in the carrier of Necklace n holds [i,j] in the InternalRel
  of Necklace n
proof
  let i,j be Nat such that
A1: i = j + 1 or j = i + 1 and
A2: i in the carrier of Necklace n and
A3: j in the carrier of Necklace n;
  per cases by A1;
  suppose
A4: i=j+1;
    then [j,j+1] in the InternalRel of Necklace n by A2,Th21,Th22;
    then [j+1,j] in (the InternalRel of Necklace n)~ by RELAT_1:def 7;
    hence thesis by A4,RELAT_2:13;
  end;
  suppose
    j=i+1;
    hence thesis by A3,Th21,Th22;
  end;
end;

theorem Th26:
  n > 0 implies card ({[i+1,i] where i is Element of NAT:i+1 < n}) = n-1
proof
  deffunc F(Element of NAT) = [$1+1,$1];
  defpred P[Element of NAT] means $1+1<n;
  defpred Q[Element of NAT] means $1 in n-'1;
A1: for d1,d2 being Element of NAT st F(d1) = F(d2) holds d1=d2 by XTUPLE_0:1;
  assume
A2: n > 0;
  then
A3: n >= 0+1 by NAT_1:13;
A4: i in n-'1 implies i+1<n
  proof
    assume i in n-'1;
    then
A5: i < n-'1 by NAT_1:44;
    n >= 0+1 by A2,NAT_1:13;
    then i < n-1 by A5,XREAL_1:233;
    hence thesis by XREAL_1:20;
  end;
A6: for i being Element of NAT holds P[i] iff Q[i]
  proof
    let i being Element of NAT;
    thus i+1<n implies i in n-'1
    proof
      assume i+1<n;
      then i < n-1 by XREAL_1:20;
      then i < n-'1 by A3,XREAL_1:233;
      hence thesis by NAT_1:44;
    end;
    thus thesis by A4;
  end;
A7: {F(i) where i is Element of NAT: P[i]} = {F(i) where i is Element of
  NAT: Q[i]} from FRAENKEL:sch 3(A6);
A8: n-'1 c= NAT;
  n-'1, {F(i) where i is Element of NAT: i in n-'1} are_equipotent from
  FUNCT_7:sch 4 (A8,A1);
  hence
  card ({[i+1,i] where i is Element of NAT:i+1 < n}) = card (n-'1) by A7,
CARD_1:5
    .= n-'1 by CARD_1:def 2
    .= n-1 by A3,XREAL_1:233;
end;

theorem Th27:
  n > 0 implies card the InternalRel of Necklace n = 2*(n-1)
proof
  deffunc G(Element of NAT) = $1+1;
  deffunc F(Element of NAT) = $1;
  defpred P[Element of NAT] means $1+1 < n;
  set A = {[i,i+1] where i is Element of NAT:i+1 < n}, B = {[G(i),F(i)] where
  i is Element of NAT:P[i]};
A1: A is Relation-like
  proof
    let x be set;
    assume x in A;
    then ex i being Element of NAT st x = [i,i+1] & i+1<n;
    hence thesis;
  end;
A2: the InternalRel of Necklace n = A \/ B by Th18;
  assume
A3: n > 0;
  then n >= 0+1 by NAT_1:13;
  then
A4: n-'1 = n-1 by XREAL_1:233;
  A = the InternalRel of n-SuccRelStr by Def6;
  then
A5: card A = n-1 by A3,Th16;
  reconsider A as Relation by A1;
A6: A = {[F(i),G(i)] where i is Element of NAT: P[i]};
A7: A~ = B from Convers(A6);
A8: A misses B
  proof
    assume A meets B;
    then consider x being set such that
A9: x in A and
A10: x in B by XBOOLE_0:3;
    consider y,z being set such that
A11: x = [y,z] by A9,RELAT_1:def 1;
    [z,y] in A by A7,A10,A11,RELAT_1:def 7;
    then consider j be Element of NAT such that
A12: [z,y] = [j,j+1] and
    j+1<n;
A13: z = j & y = j+1 by A12,XTUPLE_0:1;
    consider i be Element of NAT such that
A14: [y,z] = [i,i+1] and
    i+1<n by A9,A11;
    y = i & z = i+1 by A14,XTUPLE_0:1;
    hence contradiction by A13;
  end;
  card B = n-1 by A3,Th26;
  then
  card the InternalRel of Necklace n = card (n-1) +` card (n-1) by A2,A5,A8,
CARD_2:35
    .= card ((n-'1) + (n-'1)) by A4,CARD_2:38
    .= 2*(n-1) by A4,CARD_1:def 2;
  hence thesis;
end;

theorem
  Necklace 1, ComplRelStr Necklace 1 are_isomorphic
proof
  set f = 0 .--> 0;
  set S = Necklace 1, T = ComplRelStr S;
A1: the carrier of S = the carrier of T by Def8;
  the carrier of S = {0} by Th20,CARD_1:49;
  then reconsider g = f as Function of S,T by Def8;
A2: rng g = {0} by FUNCOP_1:8;
A3: dom g = {0} by FUNCOP_1:13;
  for y,x being set holds y in rng g & x = g.y iff x in dom g & y = g.x
  proof
    let x,y being set;
A4: x in dom g & y=g.x implies y in rng g & x = g.y
    proof
      assume that
A5:   x in dom g and
A6:   y = g.x;
      the carrier of S = {0} by Th20,CARD_1:49;
      then
A7:   x = 0 by A5,TARSKI:def 1;
      then y = 0 by A6,FUNCOP_1:72;
      hence thesis by A2,A7,FUNCOP_1:72,TARSKI:def 1;
    end;
    y in rng g & x = g.y implies x in dom g & y=g.x
    proof
      assume that
A8:   y in rng g and
A9:   x = g.y;
A10:  y = 0 by A2,A8,TARSKI:def 1;
      then x = 0 by A9,FUNCOP_1:72;
      hence thesis by A3,A10,FUNCOP_1:72,TARSKI:def 1;
    end;
    hence thesis by A2,A4,FUNCOP_1:13;
  end;
  then reconsider h = g" as Function of T,S by A1,A3,A2,FUNCT_1:32;
A11: h is monotone
  proof
    let x,y being Element of T;
    assume x <= y;
    then [x,y] in the InternalRel of T by ORDERS_2:def 5;
    then [x,y] in (the InternalRel of S)` \ id (the carrier of S) by Def8;
    then not [x,y] in id (the carrier of S) by XBOOLE_0:def 5;
    then
A12: not x in (the carrier of S) or x <> y by RELAT_1:def 10;
    let a,b being Element of S such that
    a = h.x and
    b = h.y;
A13: x in (the carrier of T);
A14: the carrier of T = 1 by A1,Th20;
    then reconsider i = x, j = y as Nat by Th3;
A15: j = 0 by A14,CARD_1:49,TARSKI:def 1;
A16: i = 0 by A14,CARD_1:49,TARSKI:def 1;
A17: i + 1 <> j & j + 1 <> i & i <> j
    proof
      hereby
        assume
A18:    i+1=j or j+1=i;
        per cases by A18;
        suppose
          i+1 = j;
          hence contradiction by A14,A16,NAT_1:44;
        end;
        suppose
          j+1=i;
          hence contradiction by A14,A15,NAT_1:44;
        end;
      end;
      thus thesis by A12,A13,Def8;
    end;
A19: y = 0 by A14,CARD_1:49,TARSKI:def 1;
    the carrier of T = {0} by A1,Th20,CARD_1:49;
    hence thesis by A17,A19,TARSKI:def 1;
  end;
  g is monotone
  proof
    let x,y being Element of S;
    assume x <= y;
    then
A20: [x,y] in the InternalRel of S by ORDERS_2:def 5;
    the carrier of S = 1 by Th20;
    then reconsider i = x, j = y as Nat by Th3;
    let a,b being Element of T such that
    a = g.x and
    b = g.y;
    the carrier of S = {0} by Th20,CARD_1:49;
    then
A21: x = 0 & y = 0 by TARSKI:def 1;
    i = j + 1 or j = i + 1 by A20,Th24;
    hence thesis by A21;
  end;
  then g is isomorphic by A11,WAYBEL_0:def 38;
  hence thesis by WAYBEL_1:def 8;
end;

theorem
  Necklace 4, ComplRelStr Necklace 4 are_isomorphic
proof
  set g = (0,1) --> (1,3), h = (2,3) --> (0,2), f = g +* h;
  set S = Necklace 4, T = ComplRelStr Necklace 4;
A1: rng h = {0,2} by FUNCT_4:64;
A2: rng g = {1,3} by FUNCT_4:64;
A3: rng f c= the carrier of T
  proof
    let x be set;
    assume
A4: x in rng f;
A5: rng f c= rng g \/ rng h by FUNCT_4:17;
    rng g \/ rng h = {1,3,0,2} by A2,A1,ENUMSET1:5
      .= {0,1,2,3} by ENUMSET1:69;
    then x in 4 by A4,A5,CARD_1:52;
    then x in the carrier of S by Th20;
    hence thesis by Def8;
  end;
A6: dom f = dom (0,1) --> (1,3) \/ dom (2,3) --> (0,2) by FUNCT_4:def 1
    .= {0,1} \/ dom (2,3) --> (0,2) by FUNCT_4:62
    .= {0,1} \/ {2,3} by FUNCT_4:62
    .= {0,1,2,3} by ENUMSET1:5;
  then
A7: dom f = the carrier of S by Th20,CARD_1:52;
  then reconsider f as Function of S,T by A3,FUNCT_2:def 1,RELSET_1:4;
  take f;
  per cases;
  case that
    S is non empty and
    T is non empty;
    set A = the InternalRel of T;
A8: rng (0 .--> 1) misses rng (1 .--> 3)
    proof
      assume rng (0 .--> 1) meets rng (1 .--> 3);
      then consider x being set such that
A9:   x in rng (0 .--> 1) and
A10:  x in rng (1 .--> 3) by XBOOLE_0:3;
      rng (0 .--> 1) = {1} by FUNCOP_1:8;
      then rng (1 .--> 3) = {3} & x = 1 by A9,FUNCOP_1:8,TARSKI:def 1;
      hence contradiction by A10,TARSKI:def 1;
    end;
A11: rng g misses rng h
    proof
      assume rng g meets rng h;
      then consider x being set such that
A12:  x in rng g and
A13:  x in rng h by XBOOLE_0:3;
      x = 1 or x = 3 by A2,A12,TARSKI:def 2;
      hence contradiction by A1,A13,TARSKI:def 2;
    end;
    set B = {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]};
A14: rng (2 .--> 0) misses rng (3 .--> 2)
    proof
      assume rng (2 .--> 0) meets rng (3 .--> 2);
      then consider x being set such that
A15:  x in rng (2 .--> 0) and
A16:  x in rng (3 .--> 2) by XBOOLE_0:3;
      rng (2 .--> 0) = {0} by FUNCOP_1:8;
      then rng (3 .--> 2) = {2} & x = 0 by A15,FUNCOP_1:8,TARSKI:def 1;
      hence contradiction by A16,TARSKI:def 1;
    end;
    h = (2 .--> 0) +* (3 .-->2) by FUNCT_4:def 4;
    then
A17: h is one-to-one by A14,FUNCT_4:92;
A18: dom g misses dom h
    proof
      assume dom g meets dom h;
      then consider x being set such that
A19:  x in dom g and
A20:  x in dom h by XBOOLE_0:3;
      x = 0 or x = 1 by A19,TARSKI:def 2;
      hence contradiction by A20,TARSKI:def 2;
    end;
    then
A21: rng f = rng g \/ rng h by FRECHET:35,PARTFUN1:56
      .= {1,3,0,2} by A2,A1,ENUMSET1:5
      .= {0,1,2,3} by ENUMSET1:69
      .= the carrier of S by Th20,CARD_1:52
      .= the carrier of T by Def8;
    g = (0 .--> 1) +* (1 .-->3) by FUNCT_4:def 4;
    then
A22: g is one-to-one by A8,FUNCT_4:92;
    hence f is one-to-one by A17,A11,FUNCT_4:92;
    then reconsider F = f" as Function of T,S by A21,FUNCT_2:25;
A23: B c= A
    proof
      set C = the carrier of S;
      let x be set;
      assume x in B;
      then
A24:  x = [1,3] or x = [3,1] or x = [0,2] or x = [2,0] or x = [0,3] or x
      = [3,0] by ENUMSET1:def 4;
A25:  2 in C & 3 in C by A6,A7,ENUMSET1:def 2;
      0 in C & 1 in C by A6,A7,ENUMSET1:def 2;
      then reconsider x9=x as Element of [:C,C:] by A24,A25,ZFMISC_1:87;
      not x9 in the InternalRel of S
      proof
        assume x9 in the InternalRel of S;
        then consider i being Element of NAT such that
        i+1< 4 and
A26:    x9= [i,i+1] or x9= [i+1,i] by Th19;
        i=1 & i+1=3 or i=3 & i+1=1 or i=0 & i+1=2 or i=2 & i+1=0 or i=0 &
        i+1=3 or i=3 & i+1=0 by A24,A26,XTUPLE_0:1;
        hence contradiction;
      end;
      then
A27:  x9 in (the InternalRel of S)` by SUBSET_1:29;
      not x in id (the carrier of S) by A24,RELAT_1:def 10;
      then x in (the InternalRel of S)` \ id (the carrier of S) by A27,
XBOOLE_0:def 5;
      hence thesis by Def8;
    end;
    thus f is monotone
    proof
A28:  dom h = {2,3} by FUNCT_4:62;
      then 2 in dom h by TARSKI:def 2;
      then
A29:  f.2 = h.2 by FUNCT_4:13
        .= 0 by FUNCT_4:63;
      3 in dom h by A28,TARSKI:def 2;
      then
A30:  f.3 = h.3 by FUNCT_4:13
        .= 2 by FUNCT_4:63;
A31:  dom g = {0,1} by FUNCT_4:62;
      then 0 in dom g by TARSKI:def 2;
      then
A32:  f.0 = g.0 by A18,FUNCT_4:16
        .= 1 by FUNCT_4:63;
      1 in dom g by A31,TARSKI:def 2;
      then
A33:  f.1 = g.1 by A18,FUNCT_4:16
        .= 3 by FUNCT_4:63;
      let x,y being Element of S;
      assume x <= y;
      then
A34:  [x,y] in the InternalRel of S by ORDERS_2:def 5;
      the carrier of S = 4 by Th20;
      then reconsider i = x, j = y as Nat by Th3;
A35:  i = j + 1 or j = i + 1 by A34,Th24;
      let a,b being Element of T such that
A36:  a = f.x & b = f.y;
      per cases by A6,A7,ENUMSET1:def 2;
      suppose
        x = 0 & y = 0;
        hence thesis by A35;
      end;
      suppose
        x = 0 & y = 1;
        then [a,b] in B by A36,A32,A33,ENUMSET1:def 4;
        hence thesis by A23,ORDERS_2:def 5;
      end;
      suppose
        x = 0 & y = 2;
        hence thesis by A35;
      end;
      suppose
        x = 0 & y = 3;
        hence thesis by A35;
      end;
      suppose
        x = 1 & y = 0;
        then [a,b] in B by A36,A32,A33,ENUMSET1:def 4;
        hence thesis by A23,ORDERS_2:def 5;
      end;
      suppose
        x = 1 & y = 1;
        hence thesis by A35;
      end;
      suppose
        x = 1 & y = 2;
        then [a,b] in B by A36,A33,A29,ENUMSET1:def 4;
        hence thesis by A23,ORDERS_2:def 5;
      end;
      suppose
        x = 1 & y = 3;
        hence thesis by A35;
      end;
      suppose
        x = 2 & y = 0;
        hence thesis by A35;
      end;
      suppose
        x = 2 & y = 1;
        then [a,b] in B by A36,A33,A29,ENUMSET1:def 4;
        hence thesis by A23,ORDERS_2:def 5;
      end;
      suppose
        x = 2 & y = 2;
        hence thesis by A35;
      end;
      suppose
        x = 2 & y = 3;
        then [a,b] in B by A36,A29,A30,ENUMSET1:def 4;
        hence thesis by A23,ORDERS_2:def 5;
      end;
      suppose
        x = 3 & y = 0;
        hence thesis by A35;
      end;
      suppose
        x = 3 & y = 1;
        hence thesis by A35;
      end;
      suppose
        x = 3 & y = 2;
        then [a,b] in B by A36,A29,A30,ENUMSET1:def 4;
        hence thesis by A23,ORDERS_2:def 5;
      end;
      suppose
        x = 3 & y = 3;
        hence thesis by A35;
      end;
    end;
    take F;
    thus F = f";
    thus F is monotone
    proof
      let x,y being Element of T;
      assume x <= y;
      then [x,y] in the InternalRel of T by ORDERS_2:def 5;
      then
A37:  [x,y] in (the InternalRel of S)` \ id (the carrier of S) by Def8;
      then not [x,y] in id (the carrier of S) by XBOOLE_0:def 5;
      then
A38:  not x in (the carrier of S) or x <> y by RELAT_1:def 10;
      [x,y] in (the InternalRel of S)` implies not [x,y] in (the
      InternalRel of S) by XBOOLE_0:def 5;
      then
A39:  not [x,y] in ({[k,k+1] where k is Element of NAT:k+1 < 4} \/ {[l+1,
      l] where l is Element of NAT:l+1 < 4}) by A37,Th18,XBOOLE_0:def 5;
      then
A40:  not [x,y] in {[k+1,k] where k is Element of NAT:k+1 < 4} by
XBOOLE_0:def 3;
A41:  the carrier of T = the carrier of S by Def8
        .= 4 by Th20;
      then x is natural & y is natural by Th3;
      then reconsider i = x, j = y as Element of NAT by ORDINAL1:def 12;
A42:  x in (the carrier of T);
A43:  not [x,y] in {[k,k+1] where k is Element of NAT:k+1 < 4} by A39,
XBOOLE_0:def 3;
A44:  i + 1 <> j & j + 1 <> i & i <> j
      proof
        hereby
          assume
A45:      i+1=j or j+1=i;
          per cases by A45;
          suppose
A46:        i+1 = j;
            then i+1 < 4 by A41,NAT_1:44;
            hence contradiction by A43,A46;
          end;
          suppose
A47:        j+1=i;
            then j+1 < 4 by A41,NAT_1:44;
            hence contradiction by A40,A47;
          end;
        end;
        thus thesis by A38,A42,Def8;
      end;
A48:  h" = (0,2) --> (2,3) by Th10;
      then
A49:  dom (h") = {0,2} by FUNCT_4:62;
      then
A50:  0 in dom (h") by TARSKI:def 2;
A51:  F.0 = (g" +* h").0 by A22,A17,A18,A11,Th7
        .= h".0 by A50,FUNCT_4:13
        .= 2 by A48,FUNCT_4:63;
A52:  g" = (1,3) --> (0,1) by Th10;
      then
A53:  dom (g") = {1,3} by FUNCT_4:62;
      then
A54:  1 in dom (g") by TARSKI:def 2;
A55:  dom (g") misses dom (h")
      proof
        assume dom (g") meets dom (h");
        then consider x being set such that
A56:    x in dom (g") and
A57:    x in dom (h") by XBOOLE_0:3;
        x = 1 or x = 3 by A53,A56,TARSKI:def 2;
        hence contradiction by A49,A57,TARSKI:def 2;
      end;
A58:  F.1 = (g" +* h").1 by A22,A17,A18,A11,Th7
        .= g".1 by A55,A54,FUNCT_4:16
        .= 0 by A52,FUNCT_4:63;
A59:  2 in dom (h") by A49,TARSKI:def 2;
A60:  F.2 = (g" +* h").2 by A22,A17,A18,A11,Th7
        .= h".2 by A59,FUNCT_4:13
        .= 3 by A48,FUNCT_4:63;
A61:  3 in dom (g") by A53,TARSKI:def 2;
A62:  F.3 = (g" +* h").3 by A22,A17,A18,A11,Th7
        .= g".3 by A55,A61,FUNCT_4:16
        .= 1 by A52,FUNCT_4:63;
      let a,b being Element of S such that
A63:  a = F.x and
A64:  b = F.y;
      per cases by A41,CARD_1:52,ENUMSET1:def 2;
      suppose
        x = 0 & y = 0;
        hence thesis by A44;
      end;
      suppose
        x = 0 & y = 1;
        hence thesis by A44;
      end;
      suppose
A65:    x = 0 & y = 2;
        then b = 2+1 by A64,A60;
        then [a,b] in the InternalRel of S by A63,A51,A65,Th25;
        hence thesis by ORDERS_2:def 5;
      end;
      suppose
A66:    x = 0 & y = 3;
        then a = 1+1 by A63,A51;
        then [a,b] in the InternalRel of S by A64,A62,A66,Th25;
        hence thesis by ORDERS_2:def 5;
      end;
      suppose
        x = 1 & y = 0;
        hence thesis by A44;
      end;
      suppose
        x = 1 & y = 1;
        hence thesis by A44;
      end;
      suppose
        x = 1 & y = 2;
        hence thesis by A44;
      end;
      suppose
A67:    x = 1 & y = 3;
        then b = 0+1 by A64,A62;
        then [a,b] in the InternalRel of S by A63,A58,A67,Th25;
        hence thesis by ORDERS_2:def 5;
      end;
      suppose
A68:    x = 2 & y = 0;
        then a = 2+1 by A63,A60;
        then [a,b] in the InternalRel of S by A64,A51,A68,Th25;
        hence thesis by ORDERS_2:def 5;
      end;
      suppose
        x = 2 & y = 1;
        hence thesis by A44;
      end;
      suppose
        x = 2 & y = 2;
        hence thesis by A44;
      end;
      suppose
        x = 2 & y = 3;
        hence thesis by A44;
      end;
      suppose
A69:    x = 3 & y = 0;
        then b = 1+1 by A64,A51;
        then [a,b] in the InternalRel of S by A63,A62,A69,Th25;
        hence thesis by ORDERS_2:def 5;
      end;
      suppose
A70:    x = 3 & y = 1;
        then a = 0+1 by A63,A62;
        then [a,b] in the InternalRel of S by A64,A58,A70,Th25;
        hence thesis by ORDERS_2:def 5;
      end;
      suppose
        x = 3 & y = 2;
        hence thesis by A44;
      end;
      suppose
        x = 3 & y = 3;
        hence thesis by A44;
      end;
    end;
  end;
  case
    S is empty or T is empty;
    hence thesis;
  end;
end;

theorem
  Necklace n, ComplRelStr Necklace n are_isomorphic implies n = 0 or n =
  1 or n = 4
proof
  assume
A1: Necklace n, ComplRelStr Necklace n are_isomorphic;
  set S = Necklace n, T = ComplRelStr S;
  card n = n by CARD_1:def 2;
  then
A2: card [:n,n:] = n*n by CARD_2:46;
  assume
A3: not thesis;
  then n = 2 or n = 3 or n > 4 by NAT_1:28;
  then
A4: card the InternalRel of S = 2*(n-1) by Th27;
A5: n*n - 2*(n-1) - n <> 2*(n-1)
  proof
A6: delta(1,-5,4) = (-5)^2 - 4*1*4 by QUIN_1:def 1
      .= 9;
    assume not thesis;
    then 1*n ^2 + (- 5)*n + 4 = 0;
    then
    n = (- (-5) - sqrt delta(1,-5,4))/(2 * 1) or n = (- (-5) + sqrt delta
    (1,-5,4))/(2 * 1) by A6,QUIN_1:15;
    then n = (5 - sqrt 3^2)/2 or n = (5 + sqrt 3^2)/2 by A6;
    then
A7: n = (5 - 3)/2 or n = (5+3)/2 by SQUARE_1:22;
    per cases by A7;
    suppose
      n =1;
      hence contradiction by A3;
    end;
    suppose
      n=4;
      hence contradiction by A3;
    end;
  end;
A8: id (the carrier of S) misses (the InternalRel of S)
  proof
    assume not thesis;
    then consider x being set such that
A9: x in id (the carrier of S) and
A10: x in the InternalRel of S by XBOOLE_0:3;
    consider i being Element of NAT such that
    i+1 < n and
A11: x = [i,i+1] or x = [i+1,i] by A10,Th19;
    consider x1,x2 being set such that
A12: x = [x1,x2] by A9,RELAT_1:def 1;
A13: x1=x2 by A9,A12,RELAT_1:def 10;
    per cases by A12,A11;
    suppose
      [x1,x2] = [i,i+1];
      then x1 = i & x2 = i+1 by XTUPLE_0:1;
      hence thesis by A13;
    end;
    suppose
      [x1,x2] = [i+1,i];
      then x1 = i+1 & x2 = i by XTUPLE_0:1;
      hence thesis by A13;
    end;
  end;
  the carrier of S = n by Th20;
  then
A14: card (the InternalRel of S)` = n*n - 2*(n-1) by A4,A2,CARD_2:44;
  the carrier of S = n & n = card n by Th20,CARD_1:def 2;
  then
A15: card id (the carrier of S) = n by Th5;
  card (the InternalRel of T) = card ((the InternalRel of S)` \ id (the
  carrier of S)) by Def8
    .= n*n - 2*(n-1) - n by A14,A15,A8,CARD_2:44,XBOOLE_1:86;
  hence thesis by A1,A4,A5,Th17;
end;