:: The Class of Series-Parallel Graphs, {III}
::  by Krzysztof Retel

environ

 vocabularies NUMBERS, RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, RELAT_2, STRUCT_0,
      FINSET_1, ORDERS_2, CARD_1, CAT_1, YELLOW_0, WELLORD1, NECKLA_2,
      NECKLACE, SUBSET_1, FUNCT_1, XXREAL_0, SEQM_3, REWRITE1, FINSEQ_1, NAT_1,
      ARYTM_3, FINSEQ_5, EQREL_1, MSUALG_5, CLASSES2, FUNCOP_1, FUNCT_4,
      ARYTM_1, NECKLA_3, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, RELAT_1, RELAT_2,
      RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, ORDINAL1, CARD_1,
      NUMBERS, XCMPLX_0, XXREAL_0, DOMAIN_1, STRUCT_0, ORDERS_2, WAYBEL_1,
      FUNCOP_1, CLASSES2, NECKLACE, WAYBEL_0, FUNCT_4, REWRITE1, FINSEQ_1,
      FINSEQ_5, EQREL_1, MSUALG_5, YELLOW_0, NECKLA_2, WELLORD1;
 constructors NAT_1, EQREL_1, CLASSES1, TOLER_1, CLASSES2, FINSEQ_5, REWRITE1,
      REALSET2, MSUALG_5, ORDERS_3, WAYBEL_1, NECKLACE, NECKLA_2, RELSET_1,
      FUNCT_4;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, CARD_1, FINSEQ_1, STRUCT_0,
      ORDERS_2, YELLOW_0, NECKLACE, NECKLA_2, ORDINAL1, FUNCT_4, RELSET_1,
      ZFMISC_1;
 requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;
 definitions XBOOLE_0, TARSKI, NECKLACE, RELAT_2;
 equalities TARSKI, FUNCOP_1, WELLORD1, STRUCT_0, ORDINAL1;
 expansions XBOOLE_0, TARSKI, NECKLACE, RELAT_2;
 theorems RELSET_1, NECKLACE, XBOOLE_0, WAYBEL_0, YELLOW_0, FUNCT_1, FUNCT_2,
      ORDERS_2, RELAT_2, SUBSET_1, ZFMISC_1, XBOOLE_1, TARSKI, MCART_1,
      CLASSES2, CLASSES1, NECKLA_2, FUNCOP_1, ENUMSET1, RELAT_1, SYSREL,
      PARTFUN1, GROUP_6, CARD_2, REWRITE1, FINSEQ_1, FINSEQ_3, FINSEQ_5, NAT_1,
      EQREL_1, MSUALG_6, MSUALG_5, CARD_1, NAT_2, FUNCT_4, FUNCT_3, WAYBEL_1,
      YELLOW_6, XREAL_1, XXREAL_0, ORDINAL1, NAT_D, STRUCT_0, XTUPLE_0;
 schemes NAT_1;

begin :: Preliminaries

reserve A,B,a,b,c,d,e,f,g,h for set;

theorem Th1:
  (id A)|B = id A /\ [:B,B:]
proof
  thus (id A)|B c= id A /\ [:B,B:]
  proof
    let a be object;
    assume
A1: a in (id A)|B;
    (id A)|B is Relation of B,A by RELSET_1:18;
    then consider x,y being object such that
A2: a = [x,y] and
A3: x in B and
    y in A by A1,RELSET_1:2;
A4: [x,y] in id A by A1,A2,RELAT_1:def 11;
    then x = y by RELAT_1:def 10;
    then [x,y] in [:B,B:] by A3,ZFMISC_1:87;
    hence thesis by A2,A4,XBOOLE_0:def 4;
  end;
  let a be object;
  assume
A5: a in id A /\ [:B,B:];
  then a in [:B,B:] by XBOOLE_0:def 4;
  then
A6: ex x1,y1 being object st x1 in B & y1 in B & a = [x1,y1]
by ZFMISC_1:def 2;
  a in id A by A5,XBOOLE_0:def 4;
  hence thesis by A6,RELAT_1:def 11;
end;

theorem
  id {a,b,c,d} = {[a,a],[b,b],[c,c],[d,d]}
proof
  set X = {a,b,c,d};
  thus id X c= {[a,a],[b,b],[c,c],[d,d]}
  proof
    let x be object;
    assume
A1: x in id X;
    then consider x1,y1 being object such that
A2: x = [x1,y1] and
A3: x1 in X and
    y1 in X by RELSET_1:2;
A4: x1 = y1 by A1,A2,RELAT_1:def 10;
    per cases by A3,ENUMSET1:def 2;
    suppose
      x1 = a;
      hence thesis by A2,A4,ENUMSET1:def 2;
    end;
    suppose
      x1 = b;
      hence thesis by A2,A4,ENUMSET1:def 2;
    end;
    suppose
      x1 = c;
      hence thesis by A2,A4,ENUMSET1:def 2;
    end;
    suppose
      x1 = d;
      hence thesis by A2,A4,ENUMSET1:def 2;
    end;
  end;
  let x be object;
  assume
A5: x in {[a,a],[b,b],[c,c],[d,d]};
  per cases by A5,ENUMSET1:def 2;
  suppose
A6: x = [a,a];
    a in X by ENUMSET1:def 2;
    hence thesis by A6,RELAT_1:def 10;
  end;
  suppose
A7: x = [b,b];
    b in X by ENUMSET1:def 2;
    hence thesis by A7,RELAT_1:def 10;
  end;
  suppose
A8: x = [c,c];
    c in X by ENUMSET1:def 2;
    hence thesis by A8,RELAT_1:def 10;
  end;
  suppose
A9: x = [d,d];
    d in X by ENUMSET1:def 2;
    hence thesis by A9,RELAT_1:def 10;
  end;
end;

theorem Th3:
  [:{a,b,c,d},{e,f,g,h}:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b
  ,g],[b,h]} \/ {[c,e],[c,f],[d,e],[d,f],[c,g],[c,h],[d,g],[d,h]}
proof
  set X1 = {a,b,c,d}, Y1 = {e,f,g,h}, X11 = {a,b}, X12 = {c,d}, Y11 = {e,f},
  Y12 = {g,h};
A1: [:X12,Y11:] = {[c,e],[c,f],[d,e],[d,f]} & [:X12,Y12:] = {[c,g],[c,h],[d,
  g],[ d,h]} by MCART_1:23;
  X1 = X11 \/ X12 & Y1 = Y11 \/ Y12 by ENUMSET1:5;
  then
A2: [:X1,Y1:] = [:X11,Y11:] \/ [:X11,Y12:] \/ [:X12,Y11:] \/ [:X12,Y12:] by
ZFMISC_1:98;
  [:X11,Y11:] = {[a,e],[a,f],[b,e],[b,f]} & [:X11,Y12:] = {[a,g],[a,h],[b,
  g],[ b,h]} by MCART_1:23;
  then
  [:X1,Y1:] = {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],
  [c,f],[d,e],[d,f]} \/ {[c,g],[c,h],[d,g],[d,h]} by A1,A2,ENUMSET1:25
    .= {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ ({[c,e],[c,f],[d
  ,e],[d,f]} \/ {[c,g],[c,h],[d,g],[d,h]}) by XBOOLE_1:4
    .= {[a,e],[a,f],[b,e],[b,f],[a,g],[a,h],[b,g],[b,h]} \/ {[c,e],[c,f],[d,
  e],[d,f],[c,g],[c,h],[d,g],[d,h]} by ENUMSET1:25;
  hence thesis;
end;

registration
  let X,Y be trivial set;
  cluster -> trivial for Relation of X,Y;
  correctness;
end;

theorem Th4:
  for X be trivial set, R be Relation of X st R is non empty holds
  ex x be object st R = {[x,x]}
proof
  let X be trivial set;
  let R be Relation of X;
  assume R is non empty;
  then consider x be object such that
A1: x in R;
  consider y,z be object such that
A2: x = [y,z] and
A3: y in X and
A4: z in X by A1,RELSET_1:2;
  consider a be object such that
A5: X = {a} by A3,ZFMISC_1:131;
A6: y = a & z = a by A3,A4,A5,TARSKI:def 1;
  R = {[a,a]}
  proof
    thus R c= {[a,a]}
    proof
      let r be object;
      assume r in R;
      then consider y,z be object such that
A7:   r = [y,z] and
A8:   y in X & z in X by RELSET_1:2;
      y = a & z = a by A5,A8,TARSKI:def 1;
      hence thesis by A7,TARSKI:def 1;
    end;
    let z be object;
    assume z in {[a,a]};
    hence thesis by A1,A2,A6,TARSKI:def 1;
  end;
  hence thesis;
end;

registration
  let X be trivial set;
  cluster -> trivial reflexive symmetric transitive strongly_connected
    for Relation of X;
  correctness
  proof
    let R be Relation of X,X;
A1: R is_reflexive_in field R
    proof
      per cases;
      suppose
A2:     R is empty;
        let x be object;
        assume x in field R;
        hence thesis by A2,RELAT_1:40;
      end;
      suppose
        R is non empty;
        then consider z be object such that
A3:     R = {[z,z]} by Th4;
        let x be object;
        assume x in field R;
        then
A4:     x in dom R \/ rng R by RELAT_1:def 6;
        dom R = {z} & rng R = {z} by A3,RELAT_1:9;
        then x = z by A4,TARSKI:def 1;
        hence thesis by A3,TARSKI:def 1;
      end;
    end;
A5: R is_transitive_in field R
    proof
      per cases;
      suppose
A6:     R is empty;
        let x,y,z be object;
        assume that
        x in field R and
        y in field R and
        z in field R and
A7:     [x,y] in R and
        [y,z] in R;
        thus thesis by A6,A7;
      end;
      suppose
A8:     R is non empty;
        let x,y,z be object;
        assume that
        x in field R and
        y in field R and
        z in field R and
A9:     [x,y] in R and
A10:    [y,z] in R;
        consider a be object such that
A11:    R = {[a,a]} by A8,Th4;
        [y,z] = [a,a] by A11,A10,TARSKI:def 1;
        then
A12:    z = a by XTUPLE_0:1;
        [x,y] = [a,a] by A11,A9,TARSKI:def 1;
        then x = a by XTUPLE_0:1;
        hence thesis by A11,A12,TARSKI:def 1;
      end;
    end;
A13: R is_strongly_connected_in field R
    proof
      per cases;
      suppose
A14:    R is empty;
        let x,y be object;
        assume that
A15:    x in field R and
        y in field R;
        thus thesis by A14,A15,RELAT_1:40;
      end;
      suppose
A16:    R is non empty;
        let x,y be object;
        assume that
A17:    x in field R and
A18:    y in field R;
        consider a be object such that
A19:    R = {[a,a]} by A16,Th4;
A20:    dom R = {a} & rng R = {a} by A19,RELAT_1:9;
        y in dom R \/ rng R by A18,RELAT_1:def 6;
        then
A21:    y = a by A20,TARSKI:def 1;
        x in dom R \/ rng R by A17,RELAT_1:def 6;
        then x = a by A20,TARSKI:def 1;
        hence thesis by A19,A21,TARSKI:def 1;
      end;
    end;
    R is_symmetric_in field R
    proof
      per cases;
      suppose
A22:    R is empty;
        let x,y be object;
        assume that
        x in field R and
        y in field R and
A23:    [x,y] in R;
        thus thesis by A22,A23;
      end;
      suppose
A24:    R is non empty;
        let x,y be object;
        assume that
        x in field R and
        y in field R and
A25:    [x,y] in R;
        consider a be object such that
A26:    R = {[a,a]} by A24,Th4;
        [x,y] = [a,a] by A26,A25,TARSKI:def 1;
        then x = a & y = a by XTUPLE_0:1;
        hence thesis by A26,TARSKI:def 1;
      end;
    end;
    hence thesis by A1,A5,A13;
  end;
end;

theorem Th5:
  for X be 1-element set, R be Relation of X holds R is_symmetric_in X
proof
  let X be 1-element set;
  let R be Relation of X;
  consider x be object such that
A1: X = {x} by ZFMISC_1:131;
  let a,b be object;
  assume that
A2: a in X and
A3: b in X & [a,b] in R;
  a = x by A1,A2,TARSKI:def 1;
  hence thesis by A1,A3,TARSKI:def 1;
end;

registration
  cluster non empty strict finite irreflexive symmetric for RelStr;
  correctness
  proof
    set X = {0,1}, r = {[0,1],[1,0]};
    0 in X & 1 in X by TARSKI:def 2;
    then
A1: [0,1] in [:X,X:] & [1,0] in [:X,X:] by ZFMISC_1:def 2;
    r c= [:X,X:]
    by A1,TARSKI:def 2;
    then reconsider r as Relation of X,X;
    take R = RelStr (#X,r#);
A2: for x being set st x in the carrier of R holds not [x,x] in the
    InternalRel of R
    proof
      let x be set;
A3:   not [0,0] in r
      proof
        assume [0,0] in r;
        then [0,0] = [0,1] or [0,0] = [1,0] by TARSKI:def 2;
        hence contradiction by XTUPLE_0:1;
      end;
A4:   not [1,1] in r
      proof
        assume [1,1] in r;
        then [1,1] = [0,1] or [1,1] = [1,0] by TARSKI:def 2;
        hence contradiction by XTUPLE_0:1;
      end;
      assume x in the carrier of R;
      then x = 0 or x = 1 by TARSKI:def 2;
      hence thesis by A3,A4;
    end;
    for x,y be object st x in X & y in X & [x,y] in r holds [y,x] in r
    proof
      let x,y be object;
      assume that
      x in X and
      y in X and
A5:   [x,y] in r;
      per cases by A5,TARSKI:def 2;
      suppose
        [x,y] = [0,1];
        then x = 0 & y = 1 by XTUPLE_0:1;
        hence thesis by TARSKI:def 2;
      end;
      suppose
        [x,y] = [1,0];
        then x = 1 & y = 0 by XTUPLE_0:1;
        hence thesis by TARSKI:def 2;
      end;
    end;
    then r is_symmetric_in X;
    hence thesis by A2;
  end;
end;

registration
  let L be irreflexive RelStr;
  cluster -> irreflexive for full SubRelStr of L;
  correctness
  proof
    let S be full SubRelStr of L;
    let x be set;
    assume
A1: x in the carrier of S;
    the carrier of S c= the carrier of L by YELLOW_0:def 13;
    then the InternalRel of S = (the InternalRel of L) |_2 the carrier of S &
    not [x, x] in the InternalRel of L by A1,NECKLACE:def 5,YELLOW_0:def 14;
    hence thesis by XBOOLE_0:def 4;
  end;
end;

registration
  let L be symmetric RelStr;
  cluster -> symmetric for full SubRelStr of L;
  correctness
  proof
    let S be full SubRelStr of L;
    let x,y be object;
    assume that
A1: x in the carrier of S & y in the carrier of S and
A2: [x,y] in the InternalRel of S;
A3: [y,x] in [:the carrier of S,the carrier of S:] by A1,ZFMISC_1:87;
A4: the carrier of S c= the carrier of L & the InternalRel of L
    is_symmetric_in the carrier of L by NECKLACE:def 3,YELLOW_0:def 13;
A5: the InternalRel of S = (the InternalRel of L) |_2 the carrier of S by
YELLOW_0:def 14;
    then [x,y] in the InternalRel of L by A2,XBOOLE_0:def 4;
    then [y,x] in the InternalRel of L by A1,A4;
    hence thesis by A5,A3,XBOOLE_0:def 4;
  end;
end;

theorem Th6:
  for R be irreflexive symmetric RelStr st card (the carrier of R) = 2
 ex a,b be object st the carrier of R = {a,b} & (the InternalRel of R = {
  [a,b],[b,a]} or the InternalRel of R = {})
proof
  let R be irreflexive symmetric RelStr;
  set Q = the InternalRel of R;
  assume
A1: card (the carrier of R) = 2;
  then reconsider X = the carrier of R as finite set;
  consider a,b be object such that
A2: a <> b and
A3: X = {a,b} by A1,CARD_2:60;
A4: the InternalRel of R c= {[a,b],[b,a]}
  proof
    let x be object;
    assume
A5: x in the InternalRel of R;
    then consider x1,x2 be object such that
A6: x = [x1,x2] and
A7: x1 in X and
A8: x2 in X by RELSET_1:2;
A9: x1 = a or x1 = b by A3,A7,TARSKI:def 2;
    per cases by A3,A6,A8,A9,TARSKI:def 2;
    suppose
A10:  x = [a,a];
      a in the carrier of R by A3,TARSKI:def 2;
      hence thesis by A5,A10,NECKLACE:def 5;
    end;
    suppose
      x = [a,b];
      hence thesis by TARSKI:def 2;
    end;
    suppose
      x = [b,a];
      hence thesis by TARSKI:def 2;
    end;
    suppose
A11:  x = [b,b];
      b in the carrier of R by A3,TARSKI:def 2;
      hence thesis by A5,A11,NECKLACE:def 5;
    end;
  end;
  per cases by A4,ZFMISC_1:36;
  suppose
    Q = {};
    hence thesis by A3;
  end;
  suppose
A12: Q = {[a,b]};
A13: a in X & b in X by A3,TARSKI:def 2;
A14: Q is_symmetric_in X by NECKLACE:def 3;
    [a,b] in Q by A12,TARSKI:def 1;
    then [b,a] in Q by A13,A14;
    then [b,a] = [a,b] by A12,TARSKI:def 1;
    hence thesis by A2,XTUPLE_0:1;
  end;
  suppose
A15: Q = {[b,a]};
A16: a in X & b in X by A3,TARSKI:def 2;
A17: Q is_symmetric_in X by NECKLACE:def 3;
    [b,a] in Q by A15,TARSKI:def 1;
    then [a,b] in Q by A16,A17;
    then [b,a] = [a,b] by A15,TARSKI:def 1;
    hence thesis by A2,XTUPLE_0:1;
  end;
  suppose
    Q = {[a,b],[b,a]};
    hence thesis by A3;
  end;
end;

begin :: Some facts about operations 'union_of' and 'sum_of'

registration
  let R be non empty RelStr,S be RelStr;
  cluster union_of(R,S) -> non empty;
  correctness
  proof
    (the carrier of R) \/ (the carrier of S) is non empty;
    hence thesis by NECKLA_2:def 2;
  end;
  cluster sum_of(R,S) -> non empty;
  correctness
  proof
    (the carrier of R) \/ (the carrier of S) is non empty;
    hence thesis by NECKLA_2:def 3;
  end;
end;

registration
  let R be RelStr, S be non empty RelStr;
  cluster union_of(R,S) -> non empty;
  correctness
  proof
    (the carrier of R) \/ (the carrier of S) is non empty;
    hence thesis by NECKLA_2:def 2;
  end;
  cluster sum_of(R,S) -> non empty;
  correctness
  proof
    (the carrier of R) \/ (the carrier of S) is non empty;
    hence thesis by NECKLA_2:def 3;
  end;
end;

registration
  let R,S be finite RelStr;
  cluster union_of(R,S) -> finite;
  correctness
  proof
    (the carrier of R) \/ the carrier of S is finite;
    hence thesis by NECKLA_2:def 2;
  end;
  cluster sum_of(R,S) -> finite;
  correctness
  proof
    (the carrier of R) \/ the carrier of S is finite;
    hence thesis by NECKLA_2:def 3;
  end;
end;

registration
  let R,S be symmetric RelStr;
  cluster union_of(R,S) -> symmetric;
  correctness
  proof
    let x,y be object;
    set U = union_of(R,S), cU = the carrier of U, IU = the InternalRel of U,
    cR = the carrier of R, cS = the carrier of S;
    assume that
    x in cU and
    y in cU and
A1: [x,y] in IU;
A2: [x,y] in (the InternalRel of R) \/ the InternalRel of S by A1,
NECKLA_2:def 2;
    per cases by A2,XBOOLE_0:def 3;
    suppose
A3:   [x,y] in the InternalRel of R;
A4:   the InternalRel of R is_symmetric_in cR by NECKLACE:def 3;
      x in cR & y in cR by A3,ZFMISC_1:87;
      then [y,x] in the InternalRel of R by A3,A4;
      then [y,x] in (the InternalRel of R) \/ the InternalRel of S by
XBOOLE_0:def 3;
      hence thesis by NECKLA_2:def 2;
    end;
    suppose
A5:   [x,y] in the InternalRel of S;
A6:   the InternalRel of S is_symmetric_in cS by NECKLACE:def 3;
      x in cS & y in cS by A5,ZFMISC_1:87;
      then [y,x] in the InternalRel of S by A5,A6;
      then [y,x] in (the InternalRel of R) \/ the InternalRel of S by
XBOOLE_0:def 3;
      hence thesis by NECKLA_2:def 2;
    end;
  end;
  cluster sum_of(R,S) -> symmetric;
  correctness
  proof
    set SU = sum_of(R,S), cSU = the carrier of sum_of(R,S), ISU = the
InternalRel of SU, cR = the carrier of R, IR = the InternalRel of R, cS = the
    carrier of S, IS = the InternalRel of S;
A7: IS is_symmetric_in cS by NECKLACE:def 3;
A8: IR is_symmetric_in cR by NECKLACE:def 3;
    the InternalRel of sum_of(R,S) is_symmetric_in cSU
    proof
      let x,y be object;
      assume that
      x in cSU and
      y in cSU and
A9:   [x,y] in ISU;
      [x,y] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by A9,NECKLA_2:def 3;
      then [x,y] in IR \/ IS \/ [:cR,cS:] or [x,y] in [:cS,cR:] by
XBOOLE_0:def 3;
      then
A10:  [x,y] in IR \/ IS or [x,y] in [:cR,cS:] or [x,y] in [:cS, cR:] by
XBOOLE_0:def 3;
      per cases by A10,XBOOLE_0:def 3;
      suppose
A11:    [x,y] in IR;
        then x in cR & y in cR by ZFMISC_1:87;
        then [y,x] in IR by A8,A11;
        then [y,x] in IR \/ IS by XBOOLE_0:def 3;
        then [y,x] in IR \/ IS \/ [:cR,cS:] by XBOOLE_0:def 3;
        then [y,x] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_0:def 3;
        hence thesis by NECKLA_2:def 3;
      end;
      suppose
A12:    [x,y] in IS;
        then x in cS & y in cS by ZFMISC_1:87;
        then [y,x] in IS by A7,A12;
        then [y,x] in IR \/ IS by XBOOLE_0:def 3;
        then [y,x] in IR \/ IS \/ [:cR,cS:] by XBOOLE_0:def 3;
        then [y,x] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_0:def 3;
        hence thesis by NECKLA_2:def 3;
      end;
      suppose
        [x,y] in [:cR,cS:];
        then x in cR & y in cS by ZFMISC_1:87;
        then [y,x] in [:cS,cR:] by ZFMISC_1:87;
        then [y,x] in [:cR,cS:] \/ [:cS,cR:] by XBOOLE_0:def 3;
        then [y,x] in IS \/ ([:cR,cS:] \/ [:cS,cR:]) by XBOOLE_0:def 3;
        then [y,x] in IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_1:4;
        then [y,x] in IR \/ (IS \/ [:cR,cS:] \/ [:cS,cR:]) by XBOOLE_0:def 3;
        then [y,x] in IR \/ (IS \/ ([:cR,cS:] \/ [:cS,cR:])) by XBOOLE_1:4;
        then [y,x] in IR \/ IS \/ ([:cR,cS:] \/ [:cS,cR:]) by XBOOLE_1:4;
        then [y,x] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_1:4;
        hence thesis by NECKLA_2:def 3;
      end;
      suppose
        [x,y] in [:cS,cR:];
        then x in cS & y in cR by ZFMISC_1:87;
        then [y,x] in [:cR,cS:] by ZFMISC_1:87;
        then [y,x] in [:cR,cS:] \/ [:cS,cR:] by XBOOLE_0:def 3;
        then [y,x] in IS \/ ([:cR,cS:] \/ [:cS,cR:]) by XBOOLE_0:def 3;
        then [y,x] in IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_1:4;
        then [y,x] in IR \/ (IS \/ [:cR,cS:] \/ [:cS,cR:]) by XBOOLE_0:def 3;
        then [y,x] in IR \/ (IS \/ ([:cR,cS:] \/ [:cS,cR:])) by XBOOLE_1:4;
        then [y,x] in IR \/ IS \/ ([:cR,cS:] \/ [:cS,cR:]) by XBOOLE_1:4;
        then [y,x] in IR \/ IS \/ [:cR,cS:] \/ [:cS,cR:] by XBOOLE_1:4;
        hence thesis by NECKLA_2:def 3;
      end;
    end;
    hence thesis;
  end;
end;

registration
  let R,S be irreflexive RelStr;
  cluster union_of(R,S) -> irreflexive;
  correctness
  proof
    set U = union_of(R,S), cU = the carrier of U, IU = the InternalRel of U,
    cR = the carrier of R, cS = the carrier of S;
    for x be set st x in cU holds not [x,x] in IU
    proof
      let x be set such that
      x in cU;
      assume not thesis;
      then
A1:   [x,x] in (the InternalRel of R) \/ the InternalRel of S by NECKLA_2:def 2
;
      per cases by A1,XBOOLE_0:def 3;
      suppose
A2:     [x,x] in the InternalRel of R;
        then x in cR by ZFMISC_1:87;
        hence thesis by A2,NECKLACE:def 5;
      end;
      suppose
A3:     [x,x] in the InternalRel of S;
        then x in cS by ZFMISC_1:87;
        hence thesis by A3,NECKLACE:def 5;
      end;
    end;
    hence thesis;
  end;
end;

theorem
  for R,S be irreflexive RelStr st the carrier of R misses the carrier
  of S holds sum_of(R,S) is irreflexive
proof
  let R,S be irreflexive RelStr such that
A1: the carrier of R misses the carrier of S;
  for x be set st x in the carrier of sum_of(R,S) holds not [x,x] in the
  InternalRel of sum_of(R,S)
  proof
    set IR = the InternalRel of R, IS = the InternalRel of S, RS = [:the
carrier of R,the carrier of S:], SR = [:the carrier of S,the carrier of R:];
    let x be set;
    assume x in the carrier of sum_of(R,S);
    assume not thesis;
    then [x,x] in IR \/ IS \/ RS \/ SR by NECKLA_2:def 3;
    then [x,x] in IR \/ IS \/ RS or [x,x] in SR by XBOOLE_0:def 3;
    then
A2: [x,x] in IR \/ IS or [x,x] in RS or [x,x] in SR by XBOOLE_0:def 3;
    per cases by A2,XBOOLE_0:def 3;
    suppose
A3:   [x,x] in IR;
      then x in the carrier of R by ZFMISC_1:87;
      hence thesis by A3,NECKLACE:def 5;
    end;
    suppose
A4:   [x,x] in IS;
      then x in the carrier of S by ZFMISC_1:87;
      hence thesis by A4,NECKLACE:def 5;
    end;
    suppose
      [x,x] in RS;
      then x in the carrier of R & x in the carrier of S by ZFMISC_1:87;
      hence thesis by A1,XBOOLE_0:3;
    end;
    suppose
      [x,x] in SR;
      then x in the carrier of S & x in the carrier of R by ZFMISC_1:87;
      hence thesis by A1,XBOOLE_0:3;
    end;
  end;
  hence thesis;
end;

theorem Th8:
  for R1,R2 being RelStr holds union_of(R1,R2) = union_of(R2,R1) &
  sum_of(R1,R2) = sum_of(R2,R1)
proof
  let R1,R2 be RelStr;
  set U1 = union_of(R1,R2), S1 = sum_of(R1,R2);
A1: the carrier of S1 = (the carrier of R2) \/ the carrier of R1 by
NECKLA_2:def 3;
A2: the InternalRel of S1 = (the InternalRel of R1) \/ (the InternalRel of
  R2 ) \/ [:the carrier of R1, the carrier of R2:] \/ [:the carrier of R2, the
  carrier of R1:] by NECKLA_2:def 3
    .= (the InternalRel of R2) \/ (the InternalRel of R1) \/ [:the carrier
  of R2, the carrier of R1:] \/ [:the carrier of R1, the carrier of R2:] by
XBOOLE_1:4;
  the carrier of U1 = (the carrier of R2) \/ the carrier of R1 & the
  InternalRel of U1 = (the InternalRel of R2) \/ the InternalRel of R1 by
NECKLA_2:def 2;
  hence thesis by A1,A2,NECKLA_2:def 2,def 3;
end;

theorem Th9:
  for G being irreflexive RelStr, G1,G2 being RelStr st ( G =
  union_of(G1,G2) or G = sum_of(G1,G2) ) holds G1 is irreflexive & G2 is
  irreflexive
proof
  let G be irreflexive RelStr, G1,G2 be RelStr;
  assume
A1: G = union_of(G1,G2) or G = sum_of(G1,G2);
  per cases by A1;
  suppose
A2: G = union_of(G1,G2);
    assume
A3: not thesis;
    thus thesis
    proof
      per cases by A3;
      suppose
        not G1 is irreflexive;
        then consider x being set such that
A4:     x in the carrier of G1 and
A5:     [x,x] in the InternalRel of G1;
        [x,x] in (the InternalRel of G1) \/ the InternalRel of G2 by A5,
XBOOLE_0:def 3;
        then
A6:     [x,x] in the InternalRel of G by A2,NECKLA_2:def 2;
        x in (the carrier of G1) \/ the carrier of G2 by A4,XBOOLE_0:def 3;
        then x in the carrier of G by A2,NECKLA_2:def 2;
        hence thesis by A6,NECKLACE:def 5;
      end;
      suppose
        not G2 is irreflexive;
        then consider x being set such that
A7:     x in the carrier of G2 and
A8:     [x,x] in the InternalRel of G2;
        [x,x] in (the InternalRel of G1) \/ the InternalRel of G2 by A8,
XBOOLE_0:def 3;
        then
A9:     [x,x] in the InternalRel of G by A2,NECKLA_2:def 2;
        x in (the carrier of G1) \/ the carrier of G2 by A7,XBOOLE_0:def 3;
        then x in the carrier of G by A2,NECKLA_2:def 2;
        hence thesis by A9,NECKLACE:def 5;
      end;
    end;
  end;
  suppose
A10: G = sum_of(G1,G2);
    assume
A11: not thesis;
    thus thesis
    proof
      per cases by A11;
      suppose
        not G1 is irreflexive;
        then consider x being set such that
A12:    x in the carrier of G1 and
A13:    [x,x] in the InternalRel of G1;
        [x,x] in (the InternalRel of G1) \/ the InternalRel of G2 by A13,
XBOOLE_0:def 3;
        then
        [x,x] in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
        the carrier of G1,the carrier of G2:] by XBOOLE_0:def 3;
        then
        [x,x] in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
the carrier of G1,the carrier of G2:] \/ [:the carrier of G2,the carrier of G1
        :] by XBOOLE_0:def 3;
        then
A14:    [x,x] in the InternalRel of G by A10,NECKLA_2:def 3;
        x in (the carrier of G1) \/ the carrier of G2 by A12,XBOOLE_0:def 3;
        then x in the carrier of G by A10,NECKLA_2:def 3;
        hence thesis by A14,NECKLACE:def 5;
      end;
      suppose
        not G2 is irreflexive;
        then consider x being set such that
A15:    x in the carrier of G2 and
A16:    [x,x] in the InternalRel of G2;
        [x,x] in (the InternalRel of G1) \/ the InternalRel of G2 by A16,
XBOOLE_0:def 3;
        then
        [x,x] in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
        the carrier of G1,the carrier of G2:] by XBOOLE_0:def 3;
        then
        [x,x] in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
the carrier of G1,the carrier of G2:] \/ [:the carrier of G2,the carrier of G1
        :] by XBOOLE_0:def 3;
        then
A17:    [x,x] in the InternalRel of G by A10,NECKLA_2:def 3;
        x in (the carrier of G1) \/ the carrier of G2 by A15,XBOOLE_0:def 3;
        then x in the carrier of G by A10,NECKLA_2:def 3;
        hence thesis by A17,NECKLACE:def 5;
      end;
    end;
  end;
end;

theorem Th10:
  for G being non empty RelStr, H1,H2 being RelStr st the carrier
  of H1 misses the carrier of H2 & ( the RelStr of G = union_of(H1,H2) or the
  RelStr of G = sum_of(H1,H2) ) holds H1 is full SubRelStr of G & H2 is full
  SubRelStr of G
proof
  let G be non empty RelStr;
  let H1,H2 be RelStr;
  assume that
A1: the carrier of H1 misses the carrier of H2 and
A2: the RelStr of G = union_of(H1,H2) or the RelStr of G = sum_of(H1,H2);
  set cH1 = the carrier of H1, cH2 = the carrier of H2, IH1 = the InternalRel
  of H1, IH2 = the InternalRel of H2, H1H2 = [:cH1,cH2:], H2H1 = [:cH2,cH1:];
  per cases by A2;
  suppose
A3: the RelStr of G = union_of(H1,H2);
A4: IH2 = (the InternalRel of G)|_2 cH2
    proof
      thus IH2 c= (the InternalRel of G)|_2 cH2
      proof
        let a be object;
        the InternalRel of G = IH1 \/ IH2 by A3,NECKLA_2:def 2;
        then
A5:     IH2 c= the InternalRel of G by XBOOLE_1:7;
        assume a in IH2;
        hence thesis by A5,XBOOLE_0:def 4;
      end;
      let a be object;
      assume
A6:   a in (the InternalRel of G)|_2 cH2;
      then
A7:   a in [:cH2,cH2:] by XBOOLE_0:def 4;
      a in the InternalRel of G by A6,XBOOLE_0:def 4;
      then
A8:   a in IH1 \/ IH2 by A3,NECKLA_2:def 2;
      per cases by A8,XBOOLE_0:def 3;
      suppose
        a in IH1;
        then consider x,y being object such that
A9:     a = [x,y] and
A10:    x in cH1 and
        y in cH1 by RELSET_1:2;
        consider x1,y1 being object such that
A11:    x1 in cH2 and
        y1 in cH2 and
A12:    a = [x1,y1] by A7,ZFMISC_1:def 2;
        x = x1 by A9,A12,XTUPLE_0:1;
        then cH1 /\ cH2 <> {} by A10,A11,XBOOLE_0:def 4;
        hence thesis by A1;
      end;
      suppose
        a in IH2;
        hence thesis;
      end;
    end;
A13: IH1 = (the InternalRel of G)|_2 cH1
    proof
      thus IH1 c= (the InternalRel of G)|_2 cH1
      proof
        let a be object;
        the InternalRel of G = IH1 \/ IH2 by A3,NECKLA_2:def 2;
        then
A14:    IH1 c= the InternalRel of G by XBOOLE_1:7;
        assume a in IH1;
        hence thesis by A14,XBOOLE_0:def 4;
      end;
      let a be object;
      assume
A15:  a in (the InternalRel of G)|_2 cH1;
      then
A16:  a in [:cH1,cH1:] by XBOOLE_0:def 4;
      a in the InternalRel of G by A15,XBOOLE_0:def 4;
      then
A17:  a in IH1 \/ IH2 by A3,NECKLA_2:def 2;
      per cases by A17,XBOOLE_0:def 3;
      suppose
        a in IH1;
        hence thesis;
      end;
      suppose
        a in IH2;
        then consider x,y being object such that
A18:    a = [x,y] and
A19:    x in cH2 and
        y in cH2 by RELSET_1:2;
        ex x1,y1 being object st x1 in cH1 & y1 in cH1 & a = [x1,y1 ] by A16,
ZFMISC_1:def 2;
        then x in cH1 by A18,XTUPLE_0:1;
        hence thesis by A1,A19,XBOOLE_0:3;
      end;
    end;
    the carrier of G = (the carrier of H1) \/ (the carrier of H2) by A3,
NECKLA_2:def 2;
    then
A20: the carrier of H1 c= the carrier of G & the carrier of H2 c= the
    carrier of G by XBOOLE_1:7;
    the InternalRel of G = IH1 \/ IH2 by A3,NECKLA_2:def 2;
    then
    IH1 c= the InternalRel of G & the InternalRel of H2 c= the InternalRel
    of G by XBOOLE_1:7;
    hence thesis by A20,A13,A4,YELLOW_0:def 13,def 14;
  end;
  suppose
A21: the RelStr of G = sum_of(H1,H2);
A22: IH2 = (the InternalRel of G)|_2 cH2
    proof
      thus IH2 c= (the InternalRel of G)|_2 cH2
      proof
        let a be object;
        the InternalRel of G = IH1 \/ IH2 \/ H1H2 \/ H2H1 by A21,NECKLA_2:def 3
;
        then the InternalRel of G = IH2 \/ (IH1 \/ H1H2 \/ H2H1) by
XBOOLE_1:113;
        then
A23:    IH2 c= the InternalRel of G by XBOOLE_1:7;
        assume a in IH2;
        hence thesis by A23,XBOOLE_0:def 4;
      end;
      let a be object;
      assume
A24:  a in (the InternalRel of G)|_2 cH2;
      then
A25:  a in [:cH2,cH2:] by XBOOLE_0:def 4;
      a in the InternalRel of G by A24,XBOOLE_0:def 4;
      then a in IH1 \/ IH2 \/ H1H2 \/ H2H1 by A21,NECKLA_2:def 3;
      then a in IH1 \/ (IH2 \/ H1H2 \/ H2H1) by XBOOLE_1:113;
      then a in IH1 or a in IH2 \/ H1H2 \/ H2H1 by XBOOLE_0:def 3;
      then a in IH1 or a in IH2 \/ (H1H2 \/ H2H1) by XBOOLE_1:4;
      then
A26:  a in IH1 or a in IH2 or a in H1H2 \/ H2H1 by XBOOLE_0:def 3;
      per cases by A26,XBOOLE_0:def 3;
      suppose
        a in IH1;
        then consider x,y being object such that
A27:    a = [x,y] and
A28:    x in cH1 and
        y in cH1 by RELSET_1:2;
        consider x1,y1 being object such that
A29:    x1 in cH2 and
        y1 in cH2 and
A30:    a = [x1,y1] by A25,ZFMISC_1:def 2;
        x = x1 by A27,A30,XTUPLE_0:1;
        then cH1 /\ cH2 <> {} by A28,A29,XBOOLE_0:def 4;
        hence thesis by A1;
      end;
      suppose
        a in IH2;
        hence thesis;
      end;
      suppose
        a in H1H2;
        then consider x,y being object such that
A31:    x in cH1 and
        y in cH2 and
A32:    a = [x,y] by ZFMISC_1:def 2;
        consider x1,y1 being object such that
A33:    x1 in cH2 and
        y1 in cH2 and
A34:    a = [x1,y1] by A25,ZFMISC_1:def 2;
        x = x1 by A32,A34,XTUPLE_0:1;
        then cH1 /\ cH2 <> {} by A31,A33,XBOOLE_0:def 4;
        hence thesis by A1;
      end;
      suppose
        a in H2H1;
        then consider x,y being object such that
        x in cH2 and
A35:    y in cH1 and
A36:    a = [x,y] by ZFMISC_1:def 2;
        consider x1,y1 being object such that
        x1 in cH2 and
A37:    y1 in cH2 and
A38:    a = [x1,y1] by A25,ZFMISC_1:def 2;
        y = y1 by A36,A38,XTUPLE_0:1;
        then cH1 /\ cH2 <> {} by A35,A37,XBOOLE_0:def 4;
        hence thesis by A1;
      end;
    end;
    IH2 c= IH1 \/ IH2 \/ [:cH1, cH2:] by XBOOLE_1:7,10;
    then
A39: IH2 c= IH1 \/ IH2 \/ [:cH1, cH2:] \/ [:cH2, cH1:] by XBOOLE_1:10;
A40: IH1 = (the InternalRel of G)|_2 cH1
    proof
      thus IH1 c= (the InternalRel of G)|_2 cH1
      proof
        let a be object;
        the InternalRel of G = IH1 \/ IH2 \/ H1H2 \/ H2H1 by A21,NECKLA_2:def 3
          .= IH1 \/ (IH2 \/ H1H2 \/ H2H1) by XBOOLE_1:113;
        then
A41:    IH1 c= the InternalRel of G by XBOOLE_1:7;
        assume a in IH1;
        hence thesis by A41,XBOOLE_0:def 4;
      end;
      let a be object;
      assume
A42:  a in (the InternalRel of G)|_2 cH1;
      then
A43:  a in [:cH1,cH1:] by XBOOLE_0:def 4;
      a in the InternalRel of G by A42,XBOOLE_0:def 4;
      then a in IH1 \/ IH2 \/ H1H2 \/ H2H1 by A21,NECKLA_2:def 3;
      then a in IH1 \/ (IH2 \/ H1H2 \/ H2H1) by XBOOLE_1:113;
      then a in IH1 or a in IH2 \/ H1H2 \/ H2H1 by XBOOLE_0:def 3;
      then a in IH1 or a in IH2 \/ (H1H2 \/ H2H1) by XBOOLE_1:4;
      then
A44:  a in IH1 or a in IH2 or a in H1H2 \/ H2H1 by XBOOLE_0:def 3;
      per cases by A44,XBOOLE_0:def 3;
      suppose
        a in IH1;
        hence thesis;
      end;
      suppose
        a in IH2;
        then consider x,y being object such that
A45:    a = [x,y] and
A46:    x in cH2 and
        y in cH2 by RELSET_1:2;
        consider x1,y1 being object such that
A47:    x1 in cH1 and
        y1 in cH1 and
A48:    a = [x1,y1] by A43,ZFMISC_1:def 2;
        x = x1 by A45,A48,XTUPLE_0:1;
        then cH1 /\ cH2 <> {} by A46,A47,XBOOLE_0:def 4;
        hence thesis by A1;
      end;
      suppose
        a in H1H2;
        then consider x,y being object such that
        x in cH1 and
A49:    y in cH2 and
A50:    a = [x,y] by ZFMISC_1:def 2;
        consider x1,y1 being object such that
        x1 in cH1 and
A51:    y1 in cH1 and
A52:    a = [x1,y1] by A43,ZFMISC_1:def 2;
        y = y1 by A50,A52,XTUPLE_0:1;
        then cH1 /\ cH2 <> {} by A49,A51,XBOOLE_0:def 4;
        hence thesis by A1;
      end;
      suppose
        a in H2H1;
        then consider x,y being object such that
A53:    x in cH2 and
        y in cH1 and
A54:    a = [x,y] by ZFMISC_1:def 2;
        consider x1,y1 being object such that
A55:    x1 in cH1 and
        y1 in cH1 and
A56:    a = [x1,y1] by A43,ZFMISC_1:def 2;
        x = x1 by A54,A56,XTUPLE_0:1;
        then cH1 /\ cH2 <> {} by A53,A55,XBOOLE_0:def 4;
        hence thesis by A1;
      end;
    end;
    IH1 c= IH1 \/ (IH2 \/ [:cH1, cH2:]) by XBOOLE_1:7;
    then
A57: IH1 c= IH1 \/ IH2 \/ [:cH1, cH2:] by XBOOLE_1:4;
    the carrier of G = (the carrier of H1) \/ (the carrier of H2) by A21,
NECKLA_2:def 3;
    then
A58: the carrier of H1 c= the carrier of G & the carrier of H2 c= the
    carrier of G by XBOOLE_1:7;
A59: the InternalRel of G = IH1 \/ IH2 \/ [:cH1, cH2:] \/ [:cH2, cH1:] by A21,
NECKLA_2:def 3;
    then IH1 \/ IH2 \/ [:cH1, cH2:] c= the InternalRel of G by XBOOLE_1:7;
    then IH1 c= the InternalRel of G by A57;
    hence thesis by A59,A58,A39,A40,A22,YELLOW_0:def 13,def 14;
  end;
end;

begin :: Theorems relating to the complement of RelStr

theorem Th11:
  the InternalRel of ComplRelStr Necklace 4 = {[0,2],[2,0],[0,3],[
  3,0],[1,3],[3,1]}
proof
  set N4 = Necklace 4, cN4 = the carrier of N4, CmpN4 = ComplRelStr N4;
A1: the carrier of Necklace 4 = {0,1,2,3} by NECKLACE:1,20;
  thus the InternalRel of CmpN4 c= {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]}
  proof
    let x be object;
    assume x in the InternalRel of CmpN4;
    then
A2: x in (the InternalRel of N4)` \ id cN4 by NECKLACE:def 8;
    then
A3: not x in id cN4 by XBOOLE_0:def 5;
    x in (the InternalRel of N4)` by A2,XBOOLE_0:def 5;
    then
A4: x in [:cN4,cN4:] \ (the InternalRel of N4) by SUBSET_1:def 4;
    consider a1,b1 being object such that
A5: a1 in cN4 and
A6: b1 in cN4 and
A7: x = [a1,b1] by A2,ZFMISC_1:def 2;
    per cases by A1,A5,A6,ENUMSET1:def 2;
    suppose
      a1 = 0 & b1 = 0;
      hence thesis by A3,A5,A7,RELAT_1:def 10;
    end;
    suppose
      a1 = 0 & b1 = 1;
      then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
      hence thesis by A4,XBOOLE_0:def 5;
    end;
    suppose
      a1 = 0 & b1 = 2;
      hence thesis by A7,ENUMSET1:def 4;
    end;
    suppose
      a1 = 0 & b1 = 3;
      hence thesis by A7,ENUMSET1:def 4;
    end;
    suppose
      a1 = 1 & b1 = 0;
      then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
      hence thesis by A4,XBOOLE_0:def 5;
    end;
    suppose
      a1 = 2 & b1 = 0;
      hence thesis by A7,ENUMSET1:def 4;
    end;
    suppose
      a1 = 3 & b1 = 0;
      hence thesis by A7,ENUMSET1:def 4;
    end;
    suppose
      a1 = 1 & b1 = 1;
      hence thesis by A3,A5,A7,RELAT_1:def 10;
    end;
    suppose
      a1 = 1 & b1 = 2;
      then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
      hence thesis by A4,XBOOLE_0:def 5;
    end;
    suppose
      a1 = 1 & b1 = 3;
      hence thesis by A7,ENUMSET1:def 4;
    end;
    suppose
      a1 = 2 & b1 = 2;
      hence thesis by A3,A5,A7,RELAT_1:def 10;
    end;
    suppose
      a1 = 2 & b1 = 1;
      then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
      hence thesis by A4,XBOOLE_0:def 5;
    end;
    suppose
      a1 = 2 & b1 = 3;
      then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
      hence thesis by A4,XBOOLE_0:def 5;
    end;
    suppose
      a1 = 3 & b1 = 3;
      hence thesis by A3,A5,A7,RELAT_1:def 10;
    end;
    suppose
      a1 = 3 & b1 = 1;
      hence thesis by A7,ENUMSET1:def 4;
    end;
    suppose
      a1 = 3 & b1 = 2;
      then x in the InternalRel of N4 by A7,ENUMSET1:def 4,NECKLA_2:2;
      hence thesis by A4,XBOOLE_0:def 5;
    end;
  end;
  let a be object;
  assume
A8: a in {[0,2],[2,0],[0,3],[3,0],[1,3],[3,1]};
  per cases by A8,ENUMSET1:def 4;
  suppose
A9: a = [0,2];
A10: not a in the InternalRel of N4
    proof
      assume
A11:  not thesis;
      per cases by A11,ENUMSET1:def 4,NECKLA_2:2;
      suppose
        a = [0,1];
        hence contradiction by A9,XTUPLE_0:1;
      end;
      suppose
        a = [1,0];
        hence contradiction by A9,XTUPLE_0:1;
      end;
      suppose
        a = [1,2];
        hence contradiction by A9,XTUPLE_0:1;
      end;
      suppose
        a = [2,1];
        hence contradiction by A9,XTUPLE_0:1;
      end;
      suppose
        a = [2,3];
        hence contradiction by A9,XTUPLE_0:1;
      end;
      suppose
        a = [3,2];
        hence contradiction by A9,XTUPLE_0:1;
      end;
    end;
    0 in cN4 & 2 in cN4 by A1,ENUMSET1:def 2;
    then a in [:cN4,cN4:] by A9,ZFMISC_1:87;
    then a in [:cN4,cN4:]\ (the InternalRel of N4) by A10,XBOOLE_0:def 5;
    then
A12: a in (the InternalRel of N4)` by SUBSET_1:def 4;
    not a in id cN4 by A9,RELAT_1:def 10;
    then a in (the InternalRel of N4)` \ id cN4 by A12,XBOOLE_0:def 5;
    hence thesis by NECKLACE:def 8;
  end;
  suppose
A13: a = [2,0];
A14: not a in the InternalRel of N4
    proof
      assume
A15:  not thesis;
      per cases by A15,ENUMSET1:def 4,NECKLA_2:2;
      suppose
        a = [0,1];
        hence contradiction by A13,XTUPLE_0:1;
      end;
      suppose
        a = [1,0];
        hence contradiction by A13,XTUPLE_0:1;
      end;
      suppose
        a = [1,2];
        hence contradiction by A13,XTUPLE_0:1;
      end;
      suppose
        a = [2,1];
        hence contradiction by A13,XTUPLE_0:1;
      end;
      suppose
        a = [2,3];
        hence contradiction by A13,XTUPLE_0:1;
      end;
      suppose
        a = [3,2];
        hence contradiction by A13,XTUPLE_0:1;
      end;
    end;
    0 in cN4 & 2 in cN4 by A1,ENUMSET1:def 2;
    then a in [:cN4,cN4:] by A13,ZFMISC_1:87;
    then a in [:cN4,cN4:]\ (the InternalRel of N4) by A14,XBOOLE_0:def 5;
    then
A16: a in (the InternalRel of N4)` by SUBSET_1:def 4;
    not a in id cN4 by A13,RELAT_1:def 10;
    then a in (the InternalRel of N4)` \ id cN4 by A16,XBOOLE_0:def 5;
    hence thesis by NECKLACE:def 8;
  end;
  suppose
A17: a = [0,3];
A18: not a in the InternalRel of N4
    proof
      assume
A19:  not thesis;
      per cases by A19,ENUMSET1:def 4,NECKLA_2:2;
      suppose
        a = [0,1];
        hence contradiction by A17,XTUPLE_0:1;
      end;
      suppose
        a = [1,0];
        hence contradiction by A17,XTUPLE_0:1;
      end;
      suppose
        a = [1,2];
        hence contradiction by A17,XTUPLE_0:1;
      end;
      suppose
        a = [2,1];
        hence contradiction by A17,XTUPLE_0:1;
      end;
      suppose
        a = [2,3];
        hence contradiction by A17,XTUPLE_0:1;
      end;
      suppose
        a = [3,2];
        hence contradiction by A17,XTUPLE_0:1;
      end;
    end;
    0 in cN4 & 3 in cN4 by A1,ENUMSET1:def 2;
    then a in [:cN4,cN4:] by A17,ZFMISC_1:87;
    then a in [:cN4,cN4:]\ (the InternalRel of N4) by A18,XBOOLE_0:def 5;
    then
A20: a in (the InternalRel of N4)` by SUBSET_1:def 4;
    not a in id cN4 by A17,RELAT_1:def 10;
    then a in (the InternalRel of N4)` \ id cN4 by A20,XBOOLE_0:def 5;
    hence thesis by NECKLACE:def 8;
  end;
  suppose
A21: a = [3,0];
A22: not a in the InternalRel of N4
    proof
      assume
A23:  not thesis;
      per cases by A23,ENUMSET1:def 4,NECKLA_2:2;
      suppose
        a = [0,1];
        hence contradiction by A21,XTUPLE_0:1;
      end;
      suppose
        a = [1,0];
        hence contradiction by A21,XTUPLE_0:1;
      end;
      suppose
        a = [1,2];
        hence contradiction by A21,XTUPLE_0:1;
      end;
      suppose
        a = [2,1];
        hence contradiction by A21,XTUPLE_0:1;
      end;
      suppose
        a = [2,3];
        hence contradiction by A21,XTUPLE_0:1;
      end;
      suppose
        a = [3,2];
        hence contradiction by A21,XTUPLE_0:1;
      end;
    end;
    0 in cN4 & 3 in cN4 by A1,ENUMSET1:def 2;
    then a in [:cN4,cN4:] by A21,ZFMISC_1:87;
    then a in [:cN4,cN4:]\ (the InternalRel of N4) by A22,XBOOLE_0:def 5;
    then
A24: a in (the InternalRel of N4)` by SUBSET_1:def 4;
    not a in id cN4 by A21,RELAT_1:def 10;
    then a in (the InternalRel of N4)` \ id cN4 by A24,XBOOLE_0:def 5;
    hence thesis by NECKLACE:def 8;
  end;
  suppose
A25: a = [1,3];
A26: not a in the InternalRel of N4
    proof
      assume
A27:  not thesis;
      per cases by A27,ENUMSET1:def 4,NECKLA_2:2;
      suppose
        a = [0,1];
        hence contradiction by A25,XTUPLE_0:1;
      end;
      suppose
        a = [1,0];
        hence contradiction by A25,XTUPLE_0:1;
      end;
      suppose
        a = [1,2];
        hence contradiction by A25,XTUPLE_0:1;
      end;
      suppose
        a = [2,1];
        hence contradiction by A25,XTUPLE_0:1;
      end;
      suppose
        a = [2,3];
        hence contradiction by A25,XTUPLE_0:1;
      end;
      suppose
        a = [3,2];
        hence contradiction by A25,XTUPLE_0:1;
      end;
    end;
    1 in cN4 & 3 in cN4 by A1,ENUMSET1:def 2;
    then a in [:cN4,cN4:] by A25,ZFMISC_1:87;
    then a in [:cN4,cN4:]\ (the InternalRel of N4) by A26,XBOOLE_0:def 5;
    then
A28: a in (the InternalRel of N4)` by SUBSET_1:def 4;
    not a in id cN4 by A25,RELAT_1:def 10;
    then a in (the InternalRel of N4)` \ id cN4 by A28,XBOOLE_0:def 5;
    hence thesis by NECKLACE:def 8;
  end;
  suppose
A29: a = [3,1];
A30: not a in the InternalRel of N4
    proof
      assume
A31:  not thesis;
      per cases by A31,ENUMSET1:def 4,NECKLA_2:2;
      suppose
        a = [0,1];
        hence contradiction by A29,XTUPLE_0:1;
      end;
      suppose
        a = [1,0];
        hence contradiction by A29,XTUPLE_0:1;
      end;
      suppose
        a = [1,2];
        hence contradiction by A29,XTUPLE_0:1;
      end;
      suppose
        a = [2,1];
        hence contradiction by A29,XTUPLE_0:1;
      end;
      suppose
        a = [2,3];
        hence contradiction by A29,XTUPLE_0:1;
      end;
      suppose
        a = [3,2];
        hence contradiction by A29,XTUPLE_0:1;
      end;
    end;
    1 in cN4 & 3 in cN4 by A1,ENUMSET1:def 2;
    then a in [:cN4,cN4:] by A29,ZFMISC_1:87;
    then a in [:cN4,cN4:]\ (the InternalRel of N4) by A30,XBOOLE_0:def 5;
    then
A32: a in (the InternalRel of N4)` by SUBSET_1:def 4;
    not a in id cN4 by A29,RELAT_1:def 10;
    then a in (the InternalRel of N4)` \ id cN4 by A32,XBOOLE_0:def 5;
    hence thesis by NECKLACE:def 8;
  end;
end;

registration
  let R be RelStr;
  cluster ComplRelStr R -> irreflexive;
  correctness
  proof
    set R1 = ComplRelStr R;
    for x being set st x in the carrier of R1 holds not [x,x] in the
    InternalRel of R1
    proof
      let x be set;
      assume x in the carrier of R1;
      then
A1:   x in the carrier of R by NECKLACE:def 8;
      not [x,x] in the InternalRel of R1
      proof
        assume [x,x] in the InternalRel of R1;
        then [x,x] in (the InternalRel of R)` \ id (the carrier of R) by
NECKLACE:def 8;
        then not [x,x] in id (the carrier of R) by XBOOLE_0:def 5;
        hence contradiction by A1,RELAT_1:def 10;
      end;
      hence thesis;
    end;
    hence thesis;
  end;
end;

registration
  let R be symmetric RelStr;
  cluster ComplRelStr R -> symmetric;
  correctness
  proof
    let x,y be object;
    set S = ComplRelStr R;
    assume that
A1: x in the carrier of S & y in the carrier of S and
A2: [x,y] in the InternalRel of S;
    per cases;
    suppose
      x = y;
      hence thesis by A2;
    end;
    suppose
A3:   x <> y;
A4:   x in the carrier of R & y in the carrier of R by A1,NECKLACE:def 8;
      then
A5:   [y,x] in [:the carrier of R,the carrier of R:] by ZFMISC_1:87;
      [x,y] in (the InternalRel of R)` \ id (the carrier of R) by A2,
NECKLACE:def 8;
      then [x,y] in (the InternalRel of R)` by XBOOLE_0:def 5;
      then
      [x,y] in [:the carrier of R,the carrier of R:] \ (the InternalRel of
      R) by SUBSET_1:def 4;
      then
A6:   not [x,y] in the InternalRel of R by XBOOLE_0:def 5;
      the InternalRel of R is_symmetric_in the carrier of R by NECKLACE:def 3;
      then not [y,x] in the InternalRel of R by A4,A6;
      then [y,x] in [:the carrier of R,the carrier of R:] \ (the InternalRel
      of R) by A5,XBOOLE_0:def 5;
      then
A7:   [y,x] in (the InternalRel of R)` by SUBSET_1:def 4;
      not [y,x] in id (the carrier of R) by A3,RELAT_1:def 10;
      then [y,x] in (the InternalRel of R)` \ id (the carrier of R) by A7,
XBOOLE_0:def 5;
      hence thesis by NECKLACE:def 8;
    end;
  end;
end;

theorem Th12:
  for R be RelStr holds the InternalRel of R misses the
  InternalRel of ComplRelStr R
proof
  let R be RelStr;
  assume not thesis;
  then (the InternalRel of R) /\ the InternalRel of ComplRelStr R <> {};
  then consider a being object such that
A1: a in (the InternalRel of R) /\ the InternalRel of ComplRelStr R by
XBOOLE_0:def 1;
  a in the InternalRel of ComplRelStr R by A1,XBOOLE_0:def 4;
  then a in (the InternalRel of R)` \ id (the carrier of R) by NECKLACE:def 8;
  then a in (the InternalRel of R)` by XBOOLE_0:def 5;
  then a in [:the carrier of R,the carrier of R:] \ (the InternalRel of R) by
SUBSET_1:def 4;
  then not a in the InternalRel of R by XBOOLE_0:def 5;
  hence thesis by A1,XBOOLE_0:def 4;
end;

theorem Th13:
  for R being RelStr holds id the carrier of R misses the
  InternalRel of ComplRelStr R
proof
  let R be RelStr;
  assume not thesis;
  then id (the carrier of R) /\ the InternalRel of ComplRelStr R <> {};
  then consider a being object such that
A1: a in id (the carrier of R) /\ the InternalRel of ComplRelStr R by
XBOOLE_0:def 1;
  a in the InternalRel of ComplRelStr R by A1,XBOOLE_0:def 4;
  then
A2: a in (the InternalRel of R)` \ id the carrier of R by NECKLACE:def 8;
  a in id (the carrier of R) by A1,XBOOLE_0:def 4;
  hence contradiction by A2,XBOOLE_0:def 5;
end;

theorem Th14:
  for G being RelStr holds [:the carrier of G,the carrier of G:] =
  id (the carrier of G) \/ (the InternalRel of G) \/ (the InternalRel of
  ComplRelStr G)
proof
  let G be RelStr;
  set idcG = id the carrier of G, IG = the InternalRel of G, ICmpG = the
  InternalRel of ComplRelStr G, cG = the carrier of G;
  thus [:cG,cG:] c= idcG \/ IG \/ ICmpG
  proof
    let a be object;
    assume
A1: a in [:cG,cG:];
    then consider x,y being object such that
A2: x in cG and
    y in cG and
A3: a = [x,y] by ZFMISC_1:def 2;
    per cases;
    suppose
A4:   x = y;
      [x,x] in id cG by A2,RELAT_1:def 10;
      then a in id cG \/ IG by A3,A4,XBOOLE_0:def 3;
      hence thesis by XBOOLE_0:def 3;
    end;
    suppose
      x <> y;
      then
A5:   not a in id cG by A3,RELAT_1:def 10;
      thus thesis
      proof
        per cases;
        suppose
          a in IG;
          then a in id cG \/ IG by XBOOLE_0:def 3;
          hence thesis by XBOOLE_0:def 3;
        end;
        suppose
          not a in IG;
          then a in [:cG,cG:] \ IG by A1,XBOOLE_0:def 5;
          then a in IG` by SUBSET_1:def 4;
          then a in IG` \ id cG by A5,XBOOLE_0:def 5;
          then a in ICmpG by NECKLACE:def 8;
          then a in IG \/ ICmpG by XBOOLE_0:def 3;
          then a in id cG \/ (IG \/ ICmpG) by XBOOLE_0:def 3;
          hence thesis by XBOOLE_1:4;
        end;
      end;
    end;
  end;
  let a be object;
  assume a in idcG \/ IG \/ ICmpG;
  then
A6: a in id cG \/ IG or a in ICmpG by XBOOLE_0:def 3;
  per cases by A6,XBOOLE_0:def 3;
  suppose
    a in id cG;
    hence thesis;
  end;
  suppose
    a in IG;
    hence thesis;
  end;
  suppose
    a in ICmpG;
    then a in IG` \ id cG by NECKLACE:def 8;
    hence thesis;
  end;
end;

theorem Th15:
  for G being strict irreflexive RelStr st G is trivial holds ComplRelStr G = G
proof
  let G be strict irreflexive RelStr;
  set CG = ComplRelStr G;
  assume
A1: G is trivial;
  per cases by A1,ZFMISC_1:131;
  suppose
A2: the carrier of G is empty;
    the InternalRel of CG = (the InternalRel of G)` \ id (the carrier of G
    ) by NECKLACE:def 8;
    then
A3: the InternalRel of CG = ({} \ {}) \ id {} by A2;
    the InternalRel of G = {} by A2;
    hence thesis by A3,NECKLACE:def 8;
  end;
  suppose
    ex x being object st the carrier of G = {x};
    then consider x being object such that
A4: the carrier of G = {x};
A5: the carrier of CG = {x} by A4,NECKLACE:def 8;
    the InternalRel of G c= [:{x},{x}:] by A4;
    then the InternalRel of G c= {[x,x]} by ZFMISC_1:29;
    then
A6: the InternalRel of G = {} or the InternalRel of G = {[x,x]} by ZFMISC_1:33;
A7: the InternalRel of G <> {[x,x]}
    proof
      assume not thesis;
      then
A8:   [x,x] in the InternalRel of G by TARSKI:def 1;
      x in the carrier of G by A4,TARSKI:def 1;
      hence contradiction by A8,NECKLACE:def 5;
    end;
    the InternalRel of CG = (the InternalRel of G)` \ id (the carrier of
    G) by NECKLACE:def 8;
    then the InternalRel of CG = ([:{x},{x}:] \ {}) \ id {x} by A4,A6,A7,
SUBSET_1:def 4;
    then the InternalRel of CG = {[x,x]} \ id {x} by ZFMISC_1:29;
    then the InternalRel of CG = {[x,x]} \ {[x,x]} by SYSREL:13;
    hence thesis by A4,A6,A7,A5,XBOOLE_1:37;
  end;
end;

theorem Th16:
  for G being strict irreflexive RelStr holds ComplRelStr ( ComplRelStr G) = G
proof
  let G be strict irreflexive RelStr;
  set CCmpG = ComplRelStr (ComplRelStr G), CmpG = ComplRelStr G, cG = the
  carrier of G, IG = the InternalRel of G, ICmpG = the InternalRel of CmpG,
  ICCmpG = the InternalRel of CCmpG;
A1: cG = the carrier of CmpG by NECKLACE:def 8
    .= the carrier of CCmpG by NECKLACE:def 8;
A2: cG = the carrier of CmpG by NECKLACE:def 8;
A3: id cG misses IG
  proof
    assume not thesis;
    then id cG /\ IG <> {};
    then consider a being object such that
A4: a in id cG /\ IG by XBOOLE_0:def 1;
A5: a in IG by A4,XBOOLE_0:def 4;
    consider x,y being object such that
A6: a = [x,y] and
A7: x in cG and
    y in cG by A4,RELSET_1:2;
    a in id cG by A4,XBOOLE_0:def 4;
    then x = y by A6,RELAT_1:def 10;
    hence contradiction by A5,A6,A7,NECKLACE:def 5;
  end;
  ICCmpG = (ICmpG)` \ id the carrier of CmpG by NECKLACE:def 8
    .= [:the carrier of CmpG,the carrier of CmpG:] \ ICmpG \ id the carrier
  of CmpG by SUBSET_1:def 4
    .= ([:cG,cG:] \ (IG` \ id cG)) \ id cG by A2,NECKLACE:def 8
    .= (([:cG,cG:] \ IG`) \/ ([:cG,cG:] /\ id cG)) \ id cG by XBOOLE_1:52
    .= ( ([:cG,cG:] \ IG`) \/ id cG ) \ id cG by XBOOLE_1:28
    .= ([:cG,cG:] \ IG`) \ id cG by XBOOLE_1:40
    .= ([:cG,cG:] \ ([:cG,cG:] \ IG)) \ id cG by SUBSET_1:def 4
    .= ([:cG,cG:] /\ IG) \ id cG by XBOOLE_1:48
    .= IG \ id cG by XBOOLE_1:28
    .= IG by A3,XBOOLE_1:83;
  hence thesis by A1;
end;

theorem Th17:
  for G1,G2 being RelStr st the carrier of G1 misses the carrier
of G2 holds ComplRelStr union_of(G1,G2) = sum_of(ComplRelStr G1, ComplRelStr G2
  )
proof
  let G1,G2 be RelStr;
A1: the carrier of sum_of(ComplRelStr G1, ComplRelStr G2) = (the carrier of
  ComplRelStr G1) \/ (the carrier of ComplRelStr G2) by NECKLA_2:def 3
    .= (the carrier of G1) \/ the carrier of ComplRelStr G2 by NECKLACE:def 8
    .= (the carrier of G1) \/ the carrier of G2 by NECKLACE:def 8;
  set P = the InternalRel of ComplRelStr union_of(G1,G2), R = the InternalRel
  of sum_of(ComplRelStr G1,ComplRelStr G2), X1 = the InternalRel of ComplRelStr
  G1, X2 = the InternalRel of ComplRelStr G2, X3 = [:the carrier of ComplRelStr
  G1,the carrier of ComplRelStr G2:], X4 = [:the carrier of ComplRelStr G2,the
carrier of ComplRelStr G1:], X5 = [:the carrier of G1, the carrier of G1:], X6
  = [:the carrier of G2, the carrier of G2:], X7 = [:the carrier of G1, the
  carrier of G2:], X8 = [:the carrier of G2, the carrier of G1:];
  assume
A2: the carrier of G1 misses the carrier of G2;
A3: for a,b being object holds [a,b] in P iff [a,b] in R
  proof
    let a,b be object;
    set x = [a,b];
    thus x in P implies x in R
    proof
      assume x in P;
      then
A4:   x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
      union_of(G1,G2) by NECKLACE:def 8;
      then x in [:the carrier of union_of(G1,G2),the carrier of union_of( G1,
      G2) :];
      then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
      union_of(G1,G2):] by NECKLA_2:def 2;
      then
A5:   x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of G1
      ) \/ the carrier of G2:] by NECKLA_2:def 2;
      not x in id the carrier of union_of(G1,G2) by A4,XBOOLE_0:def 5;
      then
A6:   not x in id ((the carrier of G1) \/ the carrier of G2) by NECKLA_2:def 2;
A7:   not x in id the carrier of G1 & not x in id the carrier of G2
      proof
        assume not thesis;
        then x in id (the carrier of G1) \/ id (the carrier of G2) by
XBOOLE_0:def 3;
        hence contradiction by A6,SYSREL:14;
      end;
      the carrier of G1 = the carrier of ComplRelStr G1 & the carrier of
      G2 = the carrier of ComplRelStr G2 by NECKLACE:def 8;
      then x in X5 \/ X3 \/ X4 \/ X6 by A5,ZFMISC_1:98;
      then x in X5 \/ (X3 \/ X4 \/ X6) by XBOOLE_1:113;
      then x in X5 or x in (X3 \/ X4 \/ X6) by XBOOLE_0:def 3;
      then x in X5 or x in X3 \/ (X4 \/ X6) by XBOOLE_1:4;
      then
A8:   x in X5 or x in X3 or x in X4 \/ X6 by XBOOLE_0:def 3;
      x in (the InternalRel of union_of(G1,G2))` by A4,XBOOLE_0:def 5;
      then
      x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1, G2
      ):] \ (the InternalRel of union_of(G1,G2)) by SUBSET_1:def 4;
      then not x in (the InternalRel of union_of(G1,G2)) by XBOOLE_0:def 5;
      then
A9:   not x in (the InternalRel of G1) \/ the InternalRel of G2 by
NECKLA_2:def 2;
      then
A10:  not x in the InternalRel of G1 by XBOOLE_0:def 3;
A11:  not x in the InternalRel of G2 by A9,XBOOLE_0:def 3;
      per cases by A8,XBOOLE_0:def 3;
      suppose
        x in [:the carrier of G1,the carrier of G1:];
        then
        x in [:the carrier of G1,the carrier of G1:] \ the InternalRel of
        G1 by A10,XBOOLE_0:def 5;
        then x in (the InternalRel of G1)` by SUBSET_1:def 4;
        then x in (the InternalRel of G1)` \ id the carrier of G1 by A7,
XBOOLE_0:def 5;
        then x in X1 by NECKLACE:def 8;
        then x in X1 \/ (X2 \/ X3 \/ X4) by XBOOLE_0:def 3;
        then x in X1 \/ X2 \/ X3 \/ X4 by XBOOLE_1:113;
        hence thesis by NECKLA_2:def 3;
      end;
      suppose
        x in X3;
        then x in X2 \/ X3 by XBOOLE_0:def 3;
        then x in X2 \/ X3 \/ X4 by XBOOLE_0:def 3;
        then x in X1 \/ (X2 \/ X3 \/ X4) by XBOOLE_0:def 3;
        then x in X1 \/ X2 \/ X3 \/ X4 by XBOOLE_1:113;
        hence thesis by NECKLA_2:def 3;
      end;
      suppose
        x in X4;
        then x in X3 \/ X4 by XBOOLE_0:def 3;
        then x in X2 \/ (X3 \/ X4) by XBOOLE_0:def 3;
        then x in X2 \/ X3 \/ X4 by XBOOLE_1:4;
        then x in X1 \/ (X2 \/ X3 \/ X4) by XBOOLE_0:def 3;
        then x in X1 \/ X2 \/ X3 \/ X4 by XBOOLE_1:113;
        hence thesis by NECKLA_2:def 3;
      end;
      suppose
        x in [:the carrier of G2,the carrier of G2:];
        then
        x in [:the carrier of G2,the carrier of G2:] \ the InternalRel of
        G2 by A11,XBOOLE_0:def 5;
        then x in (the InternalRel of G2)` by SUBSET_1:def 4;
        then x in (the InternalRel of G2)` \ id the carrier of G2 by A7,
XBOOLE_0:def 5;
        then x in the InternalRel of ComplRelStr G2 by NECKLACE:def 8;
        then x in (the InternalRel of ComplRelStr G1) \/ (the InternalRel of
        ComplRelStr G2) by XBOOLE_0:def 3;
        then x in (the InternalRel of ComplRelStr G1) \/ (the InternalRel of
ComplRelStr G2) \/ [:the carrier of ComplRelStr G1, the carrier of ComplRelStr
        G2:] by XBOOLE_0:def 3;
        then x in (the InternalRel of ComplRelStr G1) \/ (the InternalRel of
ComplRelStr G2) \/ [:the carrier of ComplRelStr G1, the carrier of ComplRelStr
G2:] \/ [:the carrier of ComplRelStr G2, the carrier of ComplRelStr G1:] by
XBOOLE_0:def 3;
        hence thesis by NECKLA_2:def 3;
      end;
    end;
    assume x in R;
    then x in X1 \/ X2 \/ X3 \/ X4 by NECKLA_2:def 3;
    then x in X1 \/ X2 \/ X3 or x in X4 by XBOOLE_0:def 3;
    then
A12: x in X1 \/ X2 or x in X3 or x in X4 by XBOOLE_0:def 3;
    per cases by A12,XBOOLE_0:def 3;
    suppose
      x in X1;
      then
A13:  x in (the InternalRel of G1)` \ id the carrier of G1 by NECKLACE:def 8;
      then x in (the InternalRel of G1)` by XBOOLE_0:def 5;
      then x in [:the carrier of G1,the carrier of G1:] \ the InternalRel of
      G1 by SUBSET_1:def 4;
      then
A14:  not x in the InternalRel of G1 by XBOOLE_0:def 5;
A15:  not x in the InternalRel of union_of(G1,G2)
      proof
        assume not thesis;
        then x in (the InternalRel of G1) \/ the InternalRel of G2 by
NECKLA_2:def 2;
        then x in the InternalRel of G2 by A14,XBOOLE_0:def 3;
        then [:the carrier of G1,the carrier of G1:] /\ [:the carrier of G2,
        the carrier of G2:] is non empty by A13,XBOOLE_0:def 4;
        then
        [:the carrier of G1,the carrier of G1:] meets [:the carrier of G2
        ,the carrier of G2:];
        hence contradiction by A2,ZFMISC_1:104;
      end;
A16:  not x in id the carrier of union_of(G1,G2)
      proof
        assume not thesis;
        then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 2;
        then
A17:    x in (id the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
        thus thesis
        proof
          per cases by A17,XBOOLE_0:def 3;
          suppose
            x in id the carrier of G1;
            hence contradiction by A13,XBOOLE_0:def 5;
          end;
          suppose
            x in id the carrier of G2;
            then [:the carrier of G1,the carrier of G1:] /\ [:the carrier of
            G2,the carrier of G2:] is non empty by A13,XBOOLE_0:def 4;
            then [:the carrier of G1,the carrier of G1:] meets [:the carrier
            of G2,the carrier of G2:];
            hence contradiction by A2,ZFMISC_1:104;
          end;
        end;
      end;
      x in X5 \/ X7 by A13,XBOOLE_0:def 3;
      then x in X5 \/ X7 \/ X8 by XBOOLE_0:def 3;
      then x in X5 \/ X7 \/ X8 \/ X6 by XBOOLE_0:def 3;
      then
      x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of G1
      ) \/ the carrier of G2:] by ZFMISC_1:98;
      then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
      union_of(G1,G2):] by NECKLA_2:def 2;
      then x in [:the carrier of union_of(G1,G2), the carrier of union_of(G1,
      G2):] by NECKLA_2:def 2;
      then x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1,
      G2):] \ (the InternalRel of union_of(G1,G2)) by A15,XBOOLE_0:def 5;
      then x in (the InternalRel of union_of(G1,G2))` by SUBSET_1:def 4;
      then x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
      union_of(G1,G2) by A16,XBOOLE_0:def 5;
      hence thesis by NECKLACE:def 8;
    end;
    suppose
      x in X2;
      then
A18:  x in (the InternalRel of G2)` \ id the carrier of G2 by NECKLACE:def 8;
      then x in (the InternalRel of G2)` by XBOOLE_0:def 5;
      then x in [:the carrier of G2,the carrier of G2:] \ the InternalRel of
      G2 by SUBSET_1:def 4;
      then
A19:  not x in the InternalRel of G2 by XBOOLE_0:def 5;
A20:  not x in the InternalRel of union_of(G1,G2)
      proof
        assume not thesis;
        then x in (the InternalRel of G1) \/ the InternalRel of G2 by
NECKLA_2:def 2;
        then x in the InternalRel of G1 by A19,XBOOLE_0:def 3;
        then [:the carrier of G1,the carrier of G1:] /\ [:the carrier of G2,
        the carrier of G2:] is non empty by A18,XBOOLE_0:def 4;
        then [:the carrier of G1,the carrier of G1:] meets [:the carrier of
        G2,the carrier of G2:];
        hence contradiction by A2,ZFMISC_1:104;
      end;
A21:  not x in id the carrier of union_of(G1,G2)
      proof
        assume not thesis;
        then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 2;
        then
A22:    x in (id the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
        per cases by A22,XBOOLE_0:def 3;
        suppose
          x in id the carrier of G2;
          hence contradiction by A18,XBOOLE_0:def 5;
        end;
        suppose
          x in id the carrier of G1;
          then [:the carrier of G1,the carrier of G1:] /\ [:the carrier of G2
          ,the carrier of G2:] is non empty by A18,XBOOLE_0:def 4;
          then [:the carrier of G1,the carrier of G1:] meets [:the carrier of
          G2,the carrier of G2:];
          hence contradiction by A2,ZFMISC_1:104;
        end;
      end;
      x in X8 \/ X6 by A18,XBOOLE_0:def 3;
      then x in X7 \/ (X8 \/ X6) by XBOOLE_0:def 3;
      then x in X7 \/ X8 \/ X6 by XBOOLE_1:4;
      then x in X5 \/ (X7 \/ X8 \/ X6) by XBOOLE_0:def 3;
      then x in X5 \/ X7 \/ X8 \/ X6 by XBOOLE_1:113;
      then
      x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of G1
      ) \/ the carrier of G2:] by ZFMISC_1:98;
      then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
      union_of(G1,G2):] by NECKLA_2:def 2;
      then x in [:the carrier of union_of(G1,G2), the carrier of union_of(G1,
      G2):] by NECKLA_2:def 2;
      then x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1,
      G2):] \ (the InternalRel of union_of(G1,G2)) by A20,XBOOLE_0:def 5;
      then x in (the InternalRel of union_of(G1,G2))` by SUBSET_1:def 4;
      then x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
      union_of(G1,G2) by A21,XBOOLE_0:def 5;
      hence thesis by NECKLACE:def 8;
    end;
    suppose
      x in X3;
      then
A23:  x in [:the carrier of G1,the carrier of ComplRelStr G2:] by
NECKLACE:def 8;
      then
A24:  x in [:the carrier of G1,the carrier of G2:] by NECKLACE:def 8;
A25:  not x in the InternalRel of union_of(G1,G2)
      proof
        assume not thesis;
        then
A26:    x in (the InternalRel of G1) \/ the InternalRel of G2 by NECKLA_2:def 2
;
        per cases by A26,XBOOLE_0:def 3;
        suppose
A27:      x in the InternalRel of G1;
A28:      b in the carrier of G2 by A24,ZFMISC_1:87;
          b in the carrier of G1 by A27,ZFMISC_1:87;
          then b in (the carrier of G1) /\ the carrier of G2 by A28,
XBOOLE_0:def 4;
          hence contradiction by A2;
        end;
        suppose
A29:      x in the InternalRel of G2;
A30:      a in the carrier of G1 by A23,ZFMISC_1:87;
          a in the carrier of G2 by A29,ZFMISC_1:87;
          then a in (the carrier of G1) /\ the carrier of G2 by A30,
XBOOLE_0:def 4;
          hence contradiction by A2;
        end;
      end;
A31:  not x in id the carrier of union_of(G1,G2)
      proof
        assume not thesis;
        then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 2;
        then
A32:    x in (id the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
        per cases by A32,XBOOLE_0:def 3;
        suppose
A33:      x in id the carrier of G1;
A34:      b in the carrier of G2 by A24,ZFMISC_1:87;
          b in the carrier of G1 by A33,ZFMISC_1:87;
          then b in (the carrier of G1) /\ the carrier of G2 by A34,
XBOOLE_0:def 4;
          hence contradiction by A2;
        end;
        suppose
A35:      x in id the carrier of G2;
A36:      a in the carrier of G1 by A23,ZFMISC_1:87;
          a in the carrier of G2 by A35,ZFMISC_1:87;
          then a in (the carrier of G1) /\ the carrier of G2 by A36,
XBOOLE_0:def 4;
          hence contradiction by A2;
        end;
      end;
      x in X7 \/ X8 by A24,XBOOLE_0:def 3;
      then x in X5 \/ (X7 \/ X8) by XBOOLE_0:def 3;
      then x in X5 \/ X7 \/ X8 by XBOOLE_1:4;
      then x in X5 \/ X7 \/ X8 \/ X6 by XBOOLE_0:def 3;
      then x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of
      G1) \/ the carrier of G2:] by ZFMISC_1:98;
      then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
      union_of(G1,G2):] by NECKLA_2:def 2;
      then x in [:the carrier of union_of(G1,G2), the carrier of union_of(G1,
      G2):] by NECKLA_2:def 2;
      then x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1,
      G2):] \ (the InternalRel of union_of(G1,G2)) by A25,XBOOLE_0:def 5;
      then x in (the InternalRel of union_of(G1,G2))` by SUBSET_1:def 4;
      then x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
      union_of(G1,G2) by A31,XBOOLE_0:def 5;
      hence thesis by NECKLACE:def 8;
    end;
    suppose
      x in X4;
      then
A37:  x in [:the carrier of G2,the carrier of ComplRelStr G1:] by
NECKLACE:def 8;
      then
A38:  x in [:the carrier of G2,the carrier of G1:] by NECKLACE:def 8;
A39:  not x in the InternalRel of union_of(G1,G2)
      proof
        assume not thesis;
        then
A40:    x in (the InternalRel of G1) \/ the InternalRel of G2 by NECKLA_2:def 2
;
        per cases by A40,XBOOLE_0:def 3;
        suppose
A41:      x in the InternalRel of G1;
A42:      a in the carrier of G2 by A37,ZFMISC_1:87;
          a in the carrier of G1 by A41,ZFMISC_1:87;
          then a in (the carrier of G1) /\ the carrier of G2 by A42,
XBOOLE_0:def 4;
          hence contradiction by A2;
        end;
        suppose
A43:      x in the InternalRel of G2;
A44:      b in the carrier of G1 by A38,ZFMISC_1:87;
          b in the carrier of G2 by A43,ZFMISC_1:87;
          then b in (the carrier of G1) /\ the carrier of G2 by A44,
XBOOLE_0:def 4;
          hence contradiction by A2;
        end;
      end;
A45:  not x in id the carrier of union_of(G1,G2)
      proof
        assume not thesis;
        then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 2;
        then
A46:    x in (id the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
        per cases by A46,XBOOLE_0:def 3;
        suppose
A47:      x in id the carrier of G1;
A48:      a in the carrier of G2 by A37,ZFMISC_1:87;
          a in the carrier of G1 by A47,ZFMISC_1:87;
          then a in (the carrier of G1) /\ the carrier of G2 by A48,
XBOOLE_0:def 4;
          hence contradiction by A2;
        end;
        suppose
A49:      x in id the carrier of G2;
A50:      b in the carrier of G1 by A38,ZFMISC_1:87;
          b in the carrier of G2 by A49,ZFMISC_1:87;
          then b in (the carrier of G1) /\ the carrier of G2 by A50,
XBOOLE_0:def 4;
          hence contradiction by A2;
        end;
      end;
      x in X7 \/ X8 by A38,XBOOLE_0:def 3;
      then x in X5 \/ (X7 \/ X8) by XBOOLE_0:def 3;
      then x in X5 \/ X7 \/ X8 by XBOOLE_1:4;
      then x in X5 \/ X7 \/ X8 \/ X6 by XBOOLE_0:def 3;
      then x in [:(the carrier of G1) \/ the carrier of G2, (the carrier of
      G1) \/ the carrier of G2:] by ZFMISC_1:98;
      then x in [:(the carrier of G1) \/ the carrier of G2, the carrier of
      union_of(G1,G2):] by NECKLA_2:def 2;
      then x in [:the carrier of union_of(G1,G2), the carrier of union_of(G1,
      G2):] by NECKLA_2:def 2;
      then x in [:the carrier of union_of(G1,G2),the carrier of union_of(G1,
      G2):] \ (the InternalRel of union_of(G1,G2)) by A39,XBOOLE_0:def 5;
      then x in (the InternalRel of union_of(G1,G2))` by SUBSET_1:def 4;
      then x in (the InternalRel of union_of(G1,G2))` \ id the carrier of
      union_of(G1,G2) by A45,XBOOLE_0:def 5;
      hence thesis by NECKLACE:def 8;
    end;
  end;
  the carrier of ComplRelStr union_of(G1,G2) = the carrier of union_of(G1,
  G2) by NECKLACE:def 8
    .= (the carrier of G1) \/ the carrier of G2 by NECKLA_2:def 2;
  hence thesis by A1,A3,RELAT_1:def 2;
end;

theorem Th18:
  for G1,G2 being RelStr st the carrier of G1 misses the carrier
of G2 holds ComplRelStr sum_of(G1,G2) = union_of(ComplRelStr G1, ComplRelStr G2
  )
proof
  let G1,G2 be RelStr;
  assume
A1: the carrier of G1 misses the carrier of G2;
  set P = the InternalRel of ComplRelStr sum_of(G1,G2), R = the InternalRel of
union_of(ComplRelStr G1,ComplRelStr G2), X1 = the InternalRel of ComplRelStr G1
, X2 = the InternalRel of ComplRelStr G2, X5 = [:the carrier of G1, the carrier
  of G1:], X6 = [:the carrier of G2, the carrier of G2:], X7 = [:the carrier of
  G1, the carrier of G2:], X8 = [:the carrier of G2, the carrier of G1:];
A2: [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2):] = [:(the
carrier of G1) \/ the carrier of G2, the carrier of sum_of(G1,G2):] by
NECKLA_2:def 3
    .= [:(the carrier of G1) \/ the carrier of G2, (the carrier of G1) \/
  the carrier of G2:] by NECKLA_2:def 3
    .= X5 \/ X7 \/ X8 \/ X6 by ZFMISC_1:98;
A3: for a,b being object holds [a,b] in P iff [a,b] in R
  proof
    let a,b be object;
    set x = [a,b];
    thus x in P implies x in R
    proof
      assume x in P;
      then
A4:   x in (the InternalRel of sum_of(G1,G2))` \ id (the carrier of sum_of
      (G1,G2)) by NECKLACE:def 8;
      then x in X5 \/ X7 \/ X8 or x in X6 by A2,XBOOLE_0:def 3;
      then
A5:   x in X5 \/ X7 or x in X8 or x in X6 by XBOOLE_0:def 3;
      x in (the InternalRel of sum_of(G1,G2))` by A4,XBOOLE_0:def 5;
      then
      x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2) :]
      \ (the InternalRel of sum_of(G1,G2)) by SUBSET_1:def 4;
      then not x in the InternalRel of sum_of(G1,G2) by XBOOLE_0:def 5;
      then
A6:   not x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:
the carrier of G1,the carrier of G2:] \/ [:the carrier of G2,the carrier of G1
      :] by NECKLA_2:def 3;
A7:   not x in the InternalRel of G1 & not x in the InternalRel of G2 &
not x in [:the carrier of G1,the carrier of G2:] & not x in [:the carrier of G2
      ,the carrier of G1:]
      proof
        assume not thesis;
        then x in (the InternalRel of G1) \/ the InternalRel of G2 or x in [:
the carrier of G1,the carrier of G2:] or x in [:the carrier of G2,the carrier
        of G1:] by XBOOLE_0:def 3;
        then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:the
carrier of G1,the carrier of G2:] or x in [:the carrier of G2,the carrier of G1
        :] by XBOOLE_0:def 3;
        hence contradiction by A6,XBOOLE_0:def 3;
      end;
      not x in id (the carrier of sum_of(G1,G2)) by A4,XBOOLE_0:def 5;
      then not x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 3;
      then
A8:   not x in id (the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
      then
A9:   not x in id the carrier of G1 by XBOOLE_0:def 3;
A10:  not x in id the carrier of G2 by A8,XBOOLE_0:def 3;
      per cases by A5,XBOOLE_0:def 3;
      suppose
        x in X5;
        then x in X5 \ (the InternalRel of G1) by A7,XBOOLE_0:def 5;
        then x in (the InternalRel of G1)` by SUBSET_1:def 4;
        then x in (the InternalRel of G1)` \ id the carrier of G1 by A9,
XBOOLE_0:def 5;
        then x in X1 by NECKLACE:def 8;
        then x in X1 \/ X2 by XBOOLE_0:def 3;
        hence thesis by NECKLA_2:def 2;
      end;
      suppose
        x in X7;
        hence thesis by A7;
      end;
      suppose
        x in X8;
        hence thesis by A7;
      end;
      suppose
        x in X6;
        then x in X6 \ (the InternalRel of G2) by A7,XBOOLE_0:def 5;
        then x in (the InternalRel of G2)` by SUBSET_1:def 4;
        then x in (the InternalRel of G2)` \ id the carrier of G2 by A10,
XBOOLE_0:def 5;
        then x in X2 by NECKLACE:def 8;
        then x in X1 \/ X2 by XBOOLE_0:def 3;
        hence thesis by NECKLA_2:def 2;
      end;
    end;
    assume x in R;
    then
A11: x in (the InternalRel of ComplRelStr G1) \/ the InternalRel of
    ComplRelStr G2 by NECKLA_2:def 2;
    per cases by A11,XBOOLE_0:def 3;
    suppose
      x in the InternalRel of ComplRelStr G1;
      then
A12:  x in (the InternalRel of G1)` \ id the carrier of G1 by NECKLACE:def 8;
      then
A13:  not x in id the carrier of G1 by XBOOLE_0:def 5;
A14:  not x in id (the carrier of sum_of(G1,G2))
      proof
        assume not thesis;
        then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 3;
        then x in id (the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
        then x in id the carrier of G2 by A13,XBOOLE_0:def 3;
        then
A15:    a in the carrier of G2 by ZFMISC_1:87;
        a in the carrier of G1 by A12,ZFMISC_1:87;
        then (the carrier of G1) /\ the carrier of G2 is non empty by A15,
XBOOLE_0:def 4;
        hence contradiction by A1;
      end;
      x in (the InternalRel of G1)` by A12,XBOOLE_0:def 5;
      then x in [:the carrier of G1,the carrier of G1:] \ the InternalRel of
      G1 by SUBSET_1:def 4;
      then
A16:  not x in the InternalRel of G1 by XBOOLE_0:def 5;
A17:  not x in the InternalRel of sum_of(G1,G2)
      proof
        assume not thesis;
        then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ X7 \/
        X8 by NECKLA_2:def 3;
        then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ X7 or
        x in X8 by XBOOLE_0:def 3;
        then
A18:    x in (the InternalRel of G1) \/ the InternalRel of G2 or x in X7
        or x in X8 by XBOOLE_0:def 3;
        per cases by A16,A18,XBOOLE_0:def 3;
        suppose
A19:      x in the InternalRel of G2;
A20:      a in the carrier of G1 by A12,ZFMISC_1:87;
          a in the carrier of G2 by A19,ZFMISC_1:87;
          then (the carrier of G1) /\ the carrier of G2 is non empty by A20,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
        suppose
A21:      x in X7;
A22:      b in the carrier of G1 by A12,ZFMISC_1:87;
          b in the carrier of G2 by A21,ZFMISC_1:87;
          then (the carrier of G1) /\ the carrier of G2 is non empty by A22,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
        suppose
A23:      x in X8;
A24:      a in the carrier of G1 by A12,ZFMISC_1:87;
          a in the carrier of G2 by A23,ZFMISC_1:87;
          then (the carrier of G1) /\ the carrier of G2 is non empty by A24,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
      end;
      x in X5 \/ (X7 \/ X8 \/ X6) by A12,XBOOLE_0:def 3;
      then
      x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2) :]
      by A2,XBOOLE_1:113;
      then
      x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2) :]
      \ (the InternalRel of sum_of(G1,G2)) by A17,XBOOLE_0:def 5;
      then x in (the InternalRel of sum_of(G1,G2))` by SUBSET_1:def 4;
      then x in (the InternalRel of sum_of(G1,G2))` \ id (the carrier of
      sum_of(G1,G2)) by A14,XBOOLE_0:def 5;
      hence thesis by NECKLACE:def 8;
    end;
    suppose
      x in the InternalRel of ComplRelStr G2;
      then
A25:  x in (the InternalRel of G2)` \ id the carrier of G2 by NECKLACE:def 8;
      then
A26:  not x in id the carrier of G2 by XBOOLE_0:def 5;
A27:  not x in id (the carrier of sum_of(G1,G2))
      proof
        assume not thesis;
        then x in id ((the carrier of G1) \/ the carrier of G2) by
NECKLA_2:def 3;
        then x in id (the carrier of G1) \/ id the carrier of G2 by SYSREL:14;
        then x in id the carrier of G1 by A26,XBOOLE_0:def 3;
        then
A28:    b in the carrier of G1 by ZFMISC_1:87;
        b in the carrier of G2 by A25,ZFMISC_1:87;
        then (the carrier of G1) /\ the carrier of G2 is non empty by A28,
XBOOLE_0:def 4;
        hence contradiction by A1;
      end;
      x in (the InternalRel of G2)` by A25,XBOOLE_0:def 5;
      then x in [:the carrier of G2,the carrier of G2:] \ the InternalRel of
      G2 by SUBSET_1:def 4;
      then
A29:  not x in the InternalRel of G2 by XBOOLE_0:def 5;
A30:  not x in the InternalRel of sum_of(G1,G2)
      proof
        assume not thesis;
        then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ X7 \/
        X8 by NECKLA_2:def 3;
        then x in (the InternalRel of G1) \/ (the InternalRel of G2) \/ X7 or
        x in X8 by XBOOLE_0:def 3;
        then
A31:    x in (the InternalRel of G1) \/ the InternalRel of G2 or x in X7
        or x in X8 by XBOOLE_0:def 3;
        per cases by A29,A31,XBOOLE_0:def 3;
        suppose
A32:      x in the InternalRel of G1;
A33:      a in the carrier of G2 by A25,ZFMISC_1:87;
          a in the carrier of G1 by A32,ZFMISC_1:87;
          then (the carrier of G1) /\ the carrier of G2 is non empty by A33,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
        suppose
A34:      x in X7;
A35:      a in the carrier of G2 by A25,ZFMISC_1:87;
          a in the carrier of G1 by A34,ZFMISC_1:87;
          then (the carrier of G1) /\ the carrier of G2 is non empty by A35,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
        suppose
A36:      x in X8;
A37:      b in the carrier of G2 by A25,ZFMISC_1:87;
          b in the carrier of G1 by A36,ZFMISC_1:87;
          then (the carrier of G1) /\ the carrier of G2 is non empty by A37,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
      end;
      x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2):]
      by A2,A25,XBOOLE_0:def 3;
      then x in [:the carrier of sum_of(G1,G2),the carrier of sum_of(G1,G2 )
      :] \ (the InternalRel of sum_of(G1,G2)) by A30,XBOOLE_0:def 5;
      then x in (the InternalRel of sum_of(G1,G2))` by SUBSET_1:def 4;
      then x in (the InternalRel of sum_of(G1,G2))` \ id (the carrier of
      sum_of(G1,G2)) by A27,XBOOLE_0:def 5;
      hence thesis by NECKLACE:def 8;
    end;
  end;
A38: the carrier of union_of(ComplRelStr G1, ComplRelStr G2) = (the carrier
  of ComplRelStr G1) \/ (the carrier of ComplRelStr G2) by NECKLA_2:def 2
    .= (the carrier of G1) \/ the carrier of ComplRelStr G2 by NECKLACE:def 8
    .= (the carrier of G1) \/ the carrier of G2 by NECKLACE:def 8;
  the carrier of ComplRelStr sum_of(G1,G2) = the carrier of sum_of(G1,G2)
  by NECKLACE:def 8
    .= (the carrier of G1) \/ the carrier of G2 by NECKLA_2:def 3;
  hence thesis by A38,A3,RELAT_1:def 2;
end;

theorem
  for G being RelStr, H being full SubRelStr of G holds the InternalRel
  of ComplRelStr H = (the InternalRel of ComplRelStr G)|_2 the carrier of
  ComplRelStr H
proof
  let G be RelStr, H be full SubRelStr of G;
  set IH = the InternalRel of H, ICmpH = the InternalRel of ComplRelStr H, cH
  = the carrier of H, IG = the InternalRel of G, cG = the carrier of G, ICmpG =
  the InternalRel of ComplRelStr G;
A1: ICmpH = IH` \ id cH by NECKLACE:def 8
    .= [:cH,cH:] \ IH \ id cH by SUBSET_1:def 4;
A2: ICmpG = IG` \ id cG by NECKLACE:def 8
    .= [:cG,cG:] \ IG \ id cG by SUBSET_1:def 4;
A3: cH c= cG by YELLOW_0:def 13;
  ICmpG |_2 the carrier of ComplRelStr H = ICmpG |_2 cH by NECKLACE:def 8
    .= ([:cG,cG:] \ IG) /\ [:cH,cH:] \ id cG /\ [:cH,cH:] by A2,XBOOLE_1:50
    .= ([:cG,cG:] /\ [:cH,cH:]) \ (IG /\ [:cH,cH:]) \ (id cG /\ [:cH,cH:])
  by XBOOLE_1:50
    .= ([:cG,cG:] /\ [:cH,cH:]) \ (IG /\ [:cH,cH:]) \ (id cG)|cH by Th1
    .= ([:cG,cG:] /\ [:cH,cH:]) \ IG|_2 cH \ id cH by A3,FUNCT_3:1
    .= ([:cG,cG:] /\ [:cH,cH:]) \ IH \ id cH by YELLOW_0:def 14
    .= [:cG /\ cH, cG /\ cH:] \ IH \ id cH by ZFMISC_1:100
    .= [:cH, cG /\ cH:] \ IH \ id cH by A3,XBOOLE_1:28
    .= ICmpH by A1,A3,XBOOLE_1:28;
  hence thesis;
end;

theorem Th20:
  for G being non empty irreflexive RelStr, x being Element of G,
x9 being Element of ComplRelStr G st x = x9 holds ComplRelStr (subrelstr ([#]G
  \ {x})) = subrelstr ([#](ComplRelStr G) \ {x9})
proof
  let G be non empty irreflexive RelStr, x be Element of G, x9 be Element of
  ComplRelStr G;
  assume
A1: x = x9;
  set R = subrelstr ([#]G \ {x}), cR = the carrier of R, cG = the carrier of G;
A2: [#]ComplRelStr G = cG by NECKLACE:def 8;
A3: [:(cG \ {x}),(cG \ {x}):] = [:cR,([#]G \ {x}):] by YELLOW_0:def 15
    .= [:cR,cR:] by YELLOW_0:def 15;
A4: cR c= cG by YELLOW_0:def 13;
A5: the InternalRel of subrelstr ([#](ComplRelStr G) \ {x9}) = (the
InternalRel of ComplRelStr G)|_2 the carrier of subrelstr ([#](ComplRelStr G) \
  {x9}) by YELLOW_0:def 14
    .= (the InternalRel of ComplRelStr G)|_2 (cG \ {x}) by A1,A2,
YELLOW_0:def 15
    .= ((the InternalRel of G)` \ id cG ) /\ [:(cG \ {x}),(cG \ {x}):] by
NECKLACE:def 8
    .= ( [:cR,cR:] /\ (the InternalRel of G)` ) \ id cG by A3,XBOOLE_1:49
    .= ( [:cR,cR:] /\ ([:cG,cG:] \ the InternalRel of G) ) \ id cG by
SUBSET_1:def 4
    .= ( ([:cR,cR:] /\ [:cG,cG:]) \ the InternalRel of G) \ id cG by
XBOOLE_1:49
    .= ([:cR,cR:] \ (the InternalRel of G)) \ id cG by A4,XBOOLE_1:28
,ZFMISC_1:96;
A6: the InternalRel of ComplRelStr R = (the InternalRel of R)` \ id cR by
NECKLACE:def 8
    .= [:cR,cR:] \ (the InternalRel of R) \ id cR by SUBSET_1:def 4
    .= [:cR,cR:] \ ( (the InternalRel of G)|_2 cR ) \id cR by YELLOW_0:def 14
    .= ( ([:cR,cR:] \ (the InternalRel of G)) \/ ([:cR,cR:] \ [:cR,cR:]) ) \
  id cR by XBOOLE_1:54
    .= ( ([:cR,cR:] \ (the InternalRel of G)) \/ {}) \ id cR by XBOOLE_1:37
    .= ([:cR,cR:] \ (the InternalRel of G)) \ id cR;
A7: [:cR,cR:] = [:[#]G,([#]G \ {x}):] \ [:{x},([#]G \ {x}):] by A3,ZFMISC_1:102
    .= [:[#]G,[#]G:] \ [:[#]G,{x}:] \ [:{x},([#]G\{x}):] by ZFMISC_1:102
    .= [:cG,cG:] \ [:cG,{x}:] \ ([:{x},cG:] \ [:{x},{x}:]) by ZFMISC_1:102
    .= ( ([:cG,cG:] \ [:cG,{x}:]) \ [:{x},cG:] ) \/ ([:cG,cG:] \ [:cG,{x}:])
  /\ [:{x},{x}:] by XBOOLE_1:52
    .= ([:cG,cG:] \ ([:cG,{x}:] \/ [:{x},cG:]) ) \/ ([:cG,cG:] \ [:cG,{x}:])
  /\ [:{x},{x}:] by XBOOLE_1:41;
A8: the InternalRel of subrelstr ([#](ComplRelStr G) \ {x9}) = the
  InternalRel of ComplRelStr R
  proof
    thus the InternalRel of subrelstr ([#](ComplRelStr G) \ {x9}) c= the
    InternalRel of ComplRelStr R
    proof
      let a be object;
      assume
A9:   a in the InternalRel of subrelstr ([#](ComplRelStr G) \ {x9});
      then
A10:  not a in id cG by A5,XBOOLE_0:def 5;
A11:  not a in id cR
      proof
        assume
A12:    not thesis;
        then consider x2,y2 being object such that
A13:    a = [x2,y2] and
A14:    x2 in cR and
        y2 in cR by RELSET_1:2;
A15:    x2 in cG \ {x} by A14,YELLOW_0:def 15;
        x2 = y2 by A12,A13,RELAT_1:def 10;
        hence contradiction by A10,A13,A15,RELAT_1:def 10;
      end;
      a in ([:cR,cR:] \ (the InternalRel of G)) by A5,A9,XBOOLE_0:def 5;
      hence thesis by A6,A11,XBOOLE_0:def 5;
    end;
    let a be object;
    assume
A16: a in the InternalRel of ComplRelStr R;
    then not a in id cR by A6,XBOOLE_0:def 5;
    then not a in id (cG \ {x}) by YELLOW_0:def 15;
    then
A17: not a in (id cG \ id {x}) by SYSREL:14;
    per cases by A17,XBOOLE_0:def 5;
    suppose
A18:  not a in id cG;
      a in ([:cR,cR:] \ (the InternalRel of G)) by A6,A16,XBOOLE_0:def 5;
      hence thesis by A5,A18,XBOOLE_0:def 5;
    end;
    suppose
      a in id {x};
      then
A19:  a in {[x,x]} by SYSREL:13;
      thus thesis
      proof
        per cases by A7,A6,A16,XBOOLE_0:def 3;
        suppose
A20:      a in [:cG,cG:] \ ([:cG,{x}:] \/ [:{x},cG:]);
          x in {x} by TARSKI:def 1;
          then
A21:      [x,x] in [:{x},cG:] by ZFMISC_1:87;
          not a in ([:cG,{x}:] \/ [:{x},cG:]) by A20,XBOOLE_0:def 5;
          then not a in [:{x}, cG:] by XBOOLE_0:def 3;
          hence thesis by A19,A21,TARSKI:def 1;
        end;
        suppose
A22:      a in ([:cG,cG:] \ [:cG,{x}:]) /\ [:{x},{x}:];
          x in {x} by TARSKI:def 1;
          then
A23:      [x,x] in [:cG,{x}:] by ZFMISC_1:87;
          a in [:cG,cG:] \ [:cG,{x}:] by A22,XBOOLE_0:def 4;
          then not a in [:cG,{x}:] by XBOOLE_0:def 5;
          hence thesis by A19,A23,TARSKI:def 1;
        end;
      end;
    end;
  end;
  the carrier of ComplRelStr (subrelstr ([#]G \ {x})) = the carrier of (
  subrelstr ([#]G \ {x})) by NECKLACE:def 8
    .= (the carrier of G) \ {x} by YELLOW_0:def 15
    .= [#](ComplRelStr G) \ {x9} by A1,NECKLACE:def 8
    .= the carrier of subrelstr ([#](ComplRelStr G) \ {x9}) by YELLOW_0:def 15;
  hence thesis by A8;
end;

begin :: Another facts relating to operation 'embeds'

registration
  cluster trivial strict -> N-free for non empty RelStr;
  correctness
  proof
    set Y = Necklace 4;
    let R be non empty RelStr;
    assume R is trivial strict;
    then consider y be object such that
A1: the carrier of R = {y} by GROUP_6:def 2;
    assume not R is N-free;
    then R embeds Y by NECKLA_2:def 1;
    then consider f being Function of Y,R such that
A2: f is one-to-one and
    for x,y being Element of Y holds [x,y] in the InternalRel of Y iff [ f
    .x,f.y] in the InternalRel of R;
A3: dom f = the carrier of Y by FUNCT_2:def 1
      .= {0,1,2,3} by NECKLACE:1,20;
    then
A4: 1 in dom f by ENUMSET1:def 2;
    then f.1 in {y} by A1,PARTFUN1:4;
    then
A5: f.1 = y by TARSKI:def 1;
A6: 0 in dom f by A3,ENUMSET1:def 2;
    then f.0 in {y} by A1,PARTFUN1:4;
    then f.0 = y by TARSKI:def 1;
    hence contradiction by A2,A6,A4,A5,FUNCT_1:def 4;
  end;
end;

theorem
  for R being reflexive antisymmetric RelStr, S being RelStr holds (ex f
  being Function of R,S st 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) iff S embeds R
proof
  let R being reflexive antisymmetric RelStr, S being RelStr;
A1: now
    assume ex f being Function of R,S st 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;
    then consider f being Function of R,S such that
A2: 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;
    for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds
    x1 = x2
    proof
      let x1,x2 be object;
      assume that
A3:   x1 in dom f and
A4:   x2 in dom f and
A5:   f.x1 = f.x2;
      reconsider x1,x2 as Element of R by A3,A4;
A6:   the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 2;
      then [x2,x2] in the InternalRel of R by A3;
      then [f.x2,f.x1] in the InternalRel of S by A2,A5;
      then [x2,x1] in the InternalRel of R by A2;
      then
A7:   x2 <= x1 by ORDERS_2:def 5;
      [x1,x1] in the InternalRel of R by A3,A6;
      then [f.x1,f.x2] in the InternalRel of S by A2,A5;
      then [x1,x2] in the InternalRel of R by A2;
      then x1 <= x2 by ORDERS_2:def 5;
      hence thesis by A7,ORDERS_2:2;
    end;
    then f is one-to-one by FUNCT_1:def 4;
    hence S embeds R by A2;
  end;
  thus thesis by A1;
end;

theorem Th22:
  for G being non empty RelStr, H being non empty full SubRelStr
  of G holds G embeds H
proof
  let G be non empty RelStr;
  let H be non empty full SubRelStr of G;
  reconsider f = id the carrier of H as Function of the carrier of H, the
  carrier of H;
A1: dom f = the carrier of H;
A2: the carrier of H c= the carrier of G by YELLOW_0:def 13;
  for x being object st x in the carrier of H holds f.x in the carrier of G
  proof
    let x be object;
    assume x in the carrier of H;
    then f.x in the carrier of H by FUNCT_1:17;
    hence thesis by A2;
  end;
  then reconsider f = id the carrier of H as Function of the carrier of H, the
  carrier of G by A1,FUNCT_2:3;
  reconsider f as Function of H,G;
  for x,y being Element of H holds [x,y] in the InternalRel of H iff [f.x,
  f.y] in the InternalRel of G
  proof
    set IH = the InternalRel of H, IG = the InternalRel of G, cH = the carrier
    of H;
    let x,y be Element of H;
    thus [x,y] in IH implies [f.x,f.y] in IG
    proof
      assume [x,y] in IH;
      then [x,y] in IG |_2 cH by YELLOW_0:def 14;
      hence thesis by XBOOLE_0:def 4;
    end;
    assume [f.x,f.y] in IG;
    then [x,y] in IG |_2 cH by XBOOLE_0:def 4;
    hence thesis by YELLOW_0:def 14;
  end;
  hence thesis;
end;

theorem Th23:
  for G being non empty RelStr, H being non empty full SubRelStr
  of G st G is N-free holds H is N-free
proof
  let G be non empty RelStr, H be non empty full SubRelStr of G;
  assume
A1: G is N-free;
A2: G embeds H by Th22;
  assume not thesis;
  then H embeds Necklace 4 by NECKLA_2:def 1;
  then G embeds Necklace 4 by A2,NECKLACE:12;
  hence contradiction by A1,NECKLA_2:def 1;
end;

theorem Th24:
  for G being non empty irreflexive RelStr holds G embeds Necklace
  4 iff ComplRelStr G embeds Necklace 4
proof
  let G be non empty irreflexive RelStr;
  set N4 = Necklace 4, CmpN4 = ComplRelStr Necklace 4, CmpG = ComplRelStr G;
A1: the carrier of CmpG = the carrier of G by NECKLACE:def 8;
A2: the carrier of Necklace 4 = {0,1,2,3} by NECKLACE:1,20;
  then
A3: 0 in the carrier of N4 by ENUMSET1:def 2;
A4: the carrier of CmpN4 = the carrier of N4 by NECKLACE:def 8;
  thus G embeds N4 implies CmpG embeds N4
  proof
    CmpN4,N4 are_isomorphic by NECKLACE:29,WAYBEL_1:6;
    then consider g being Function of CmpN4,N4 such that
A5: g is isomorphic by WAYBEL_1:def 8;
    assume G embeds Necklace 4;
    then consider f being Function of N4,G such that
A6: f is one-to-one and
A7: for x,y being Element of N4 holds [x,y] in the InternalRel of N4
    iff [f.x,f.y] in the InternalRel of G;
    reconsider h = f*g as Function of CmpN4,G;
A8: g is one-to-one monotone by A5,WAYBEL_0:def 38;
A9: for x,y being Element of CmpN4 holds [x,y] in the InternalRel of
    CmpN4 iff [h.x,h.y] in the InternalRel of G
    proof
      let x,y be Element of CmpN4;
      thus [x,y] in the InternalRel of CmpN4 implies [h.x,h.y] in the
      InternalRel of G
      proof
        assume [x,y] in the InternalRel of CmpN4;
        then x <= y by ORDERS_2:def 5;
        then g.x <= g.y by A8,WAYBEL_1:def 2;
        then [g.x,g.y] in the InternalRel of N4 by ORDERS_2:def 5;
        then [f.(g.x),f.(g.y)] in the InternalRel of G by A7;
        then [(f*g).x,f.(g.y)] in the InternalRel of G by FUNCT_2:15;
        hence thesis by FUNCT_2:15;
      end;
      assume [h.x,h.y] in the InternalRel of G;
      then [f.(g.x),h.y] in the InternalRel of G by FUNCT_2:15;
      then [f.(g.x),f.(g.y)] in the InternalRel of G by FUNCT_2:15;
      then [g.x,g.y] in the InternalRel of N4 by A7;
      then g.x <= g.y by ORDERS_2:def 5;
      then x <= y by A5,WAYBEL_0:66;
      hence thesis by ORDERS_2:def 5;
    end;
A10: 0 in the carrier of CmpN4 by A2,A4,ENUMSET1:def 2;
A11: 1 in the carrier of CmpN4 by A2,A4,ENUMSET1:def 2;
A12: dom h = the carrier of CmpN4 by FUNCT_2:def 1;
A13: [h.0,h.1] in the InternalRel of CmpG
    proof
      assume
A14:  not thesis;
      [h.0,h.1] in the InternalRel of G
      proof
        h.0 in the carrier of G & h.1 in the carrier of G by A10,A11,FUNCT_2:5;
        then [h.0,h.1] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
        then
        [h.0,h.1] in id (the carrier of G) \/ (the InternalRel of G) \/ (
        the InternalRel of CmpG) by Th14;
        then
A15:    [h.0,h.1] in id (the carrier of G) \/ (the InternalRel of G) or [
        h.0,h.1] in the InternalRel of CmpG by XBOOLE_0:def 3;
        assume not thesis;
        then [h.0,h.1] in id (the carrier of G) by A14,A15,XBOOLE_0:def 3;
        then h.0 = h.1 by RELAT_1:def 10;
        hence contradiction by A6,A8,A12,A10,A11,FUNCT_1:def 4;
      end;
      then
A16:  [0,1] in the InternalRel of CmpN4 by A9,A10,A11;
      [0,1] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
      then [0,1] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A16,XBOOLE_0:def 4;
      then the InternalRel of N4 meets the InternalRel of CmpN4;
      hence thesis by Th12;
    end;
A17: 2 in the carrier of CmpN4 by A2,A4,ENUMSET1:def 2;
A18: [h.1,h.2] in the InternalRel of CmpG
    proof
      assume
A19:  not thesis;
      [h.1,h.2] in the InternalRel of G
      proof
        h.1 in the carrier of G & h.2 in the carrier of G by A11,A17,FUNCT_2:5;
        then [h.1,h.2] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
        then
        [h.1,h.2] in id (the carrier of G) \/ (the InternalRel of G) \/ (
        the InternalRel of CmpG) by Th14;
        then
A20:    [h.1,h.2] in id (the carrier of G) \/ (the InternalRel of G) or [
        h.1,h.2] in the InternalRel of CmpG by XBOOLE_0:def 3;
        assume not thesis;
        then [h.1,h.2] in id (the carrier of G) by A19,A20,XBOOLE_0:def 3;
        then h.1 = h.2 by RELAT_1:def 10;
        hence contradiction by A6,A8,A12,A11,A17,FUNCT_1:def 4;
      end;
      then
A21:  [1,2] in the InternalRel of CmpN4 by A9,A11,A17;
      [1,2] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
      then [1,2] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A21,XBOOLE_0:def 4;
      then the InternalRel of N4 meets the InternalRel of CmpN4;
      hence thesis by Th12;
    end;
A22: 3 in the carrier of CmpN4 by A2,A4,ENUMSET1:def 2;
A23: [h.2,h.3] in the InternalRel of CmpG
    proof
      assume
A24:  not thesis;
      [h.2,h.3] in the InternalRel of G
      proof
        h.2 in the carrier of G & h.3 in the carrier of G by A17,A22,FUNCT_2:5;
        then [h.2,h.3] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
        then [h.2,h.3] in id (the carrier of G) \/ (the InternalRel of G) \/
        (the InternalRel of CmpG) by Th14;
        then
A25:    [h.2,h.3] in id (the carrier of G) \/ (the InternalRel of G) or
        [h.2,h.3] in the InternalRel of CmpG by XBOOLE_0:def 3;
        assume not thesis;
        then [h.2,h.3] in id (the carrier of G) by A24,A25,XBOOLE_0:def 3;
        then h.2 = h.3 by RELAT_1:def 10;
        hence contradiction by A6,A8,A12,A17,A22,FUNCT_1:def 4;
      end;
      then
A26:  [2,3] in the InternalRel of CmpN4 by A9,A17,A22;
      [2,3] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
      then [2,3] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A26,XBOOLE_0:def 4;
      then the InternalRel of N4 meets the InternalRel of CmpN4;
      hence thesis by Th12;
    end;
    [3,1] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then
A27: [h.3,h.1] in the InternalRel of G by A9,A11,A22;
    [1,3] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then
A28: [h.1,h.3] in the InternalRel of G by A9,A11,A22;
    [3,0] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then
A29: [h.3,h.0] in the InternalRel of G by A9,A10,A22;
    [0,3] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then
A30: [h.0,h.3] in the InternalRel of G by A9,A10,A22;
A31: [h.1,h.0] in the InternalRel of CmpG
    proof
      assume
A32:  not thesis;
      [h.1,h.0] in the InternalRel of G
      proof
        h.0 in the carrier of G & h.1 in the carrier of G by A10,A11,FUNCT_2:5;
        then [h.1,h.0] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
        then
        [h.1,h.0] in id (the carrier of G) \/ (the InternalRel of G) \/ (
        the InternalRel of CmpG) by Th14;
        then
A33:    [h.1,h.0] in id (the carrier of G) \/ (the InternalRel of G) or [
        h.1,h.0] in the InternalRel of CmpG by XBOOLE_0:def 3;
        assume not thesis;
        then [h.1,h.0] in id (the carrier of G) by A32,A33,XBOOLE_0:def 3;
        then h.0 = h.1 by RELAT_1:def 10;
        hence contradiction by A6,A8,A12,A10,A11,FUNCT_1:def 4;
      end;
      then
A34:  [1,0] in the InternalRel of CmpN4 by A9,A10,A11;
      [1,0] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
      then [1,0] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A34,XBOOLE_0:def 4;
      then the InternalRel of N4 meets the InternalRel of CmpN4;
      hence thesis by Th12;
    end;
A35: [h.2,h.1] in the InternalRel of CmpG
    proof
      assume
A36:  not thesis;
      [h.2,h.1] in the InternalRel of G
      proof
        h.1 in the carrier of G & h.2 in the carrier of G by A11,A17,FUNCT_2:5;
        then [h.2,h.1] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
        then
        [h.2,h.1] in id (the carrier of G) \/ (the InternalRel of G) \/ (
        the InternalRel of CmpG) by Th14;
        then
A37:    [h.2,h.1] in id (the carrier of G) \/ (the InternalRel of G) or [
        h.2,h.1] in the InternalRel of CmpG by XBOOLE_0:def 3;
        assume not thesis;
        then [h.2,h.1] in id (the carrier of G) by A36,A37,XBOOLE_0:def 3;
        then h.1 = h.2 by RELAT_1:def 10;
        hence contradiction by A6,A8,A12,A11,A17,FUNCT_1:def 4;
      end;
      then
A38:  [2,1] in the InternalRel of CmpN4 by A9,A11,A17;
      [2,1] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
      then [2,1] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A38,XBOOLE_0:def 4;
      then the InternalRel of N4 meets the InternalRel of CmpN4;
      hence thesis by Th12;
    end;
A39: [h.3,h.2] in the InternalRel of CmpG
    proof
      assume
A40:  not thesis;
      [h.3,h.2] in the InternalRel of G
      proof
        h.2 in the carrier of G & h.3 in the carrier of G by A17,A22,FUNCT_2:5;
        then [h.3,h.2] in [:the carrier of G,the carrier of G:] by ZFMISC_1:87;
        then [h.3,h.2] in id (the carrier of G) \/ (the InternalRel of G) \/
        (the InternalRel of CmpG) by Th14;
        then
A41:    [h.3,h.2] in id (the carrier of G) \/ (the InternalRel of G) or
        [h.3,h.2] in the InternalRel of CmpG by XBOOLE_0:def 3;
        assume not thesis;
        then [h.3,h.2] in id (the carrier of G) by A40,A41,XBOOLE_0:def 3;
        then h.2 = h.3 by RELAT_1:def 10;
        hence contradiction by A6,A8,A12,A17,A22,FUNCT_1:def 4;
      end;
      then
A42:  [3,2] in the InternalRel of CmpN4 by A9,A17,A22;
      [3,2] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
      then [3,2] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by
A42,XBOOLE_0:def 4;
      then the InternalRel of N4 meets the InternalRel of CmpN4;
      hence thesis by Th12;
    end;
    [2,0] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then
A43: [h.2,h.0] in the InternalRel of G by A9,A10,A17;
    [0,2] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then
A44: [h.0,h.2] in the InternalRel of G by A9,A10,A17;
    for x,y being Element of N4 holds [x,y] in the InternalRel of N4 iff
    [h.x,h.y] in the InternalRel of CmpG
    proof
      let x,y be Element of N4;
      thus [x,y] in the InternalRel of N4 implies [h.x,h.y] in the InternalRel
      of CmpG
      proof
        assume
A45:    [x,y] in the InternalRel of N4;
        per cases by A45,ENUMSET1:def 4,NECKLA_2:2;
        suppose
A46:      [x,y] = [0,1];
          then x = 0 by XTUPLE_0:1;
          hence thesis by A13,A46,XTUPLE_0:1;
        end;
        suppose
A47:      [x,y] = [1,0];
          then x = 1 by XTUPLE_0:1;
          hence thesis by A31,A47,XTUPLE_0:1;
        end;
        suppose
A48:      [x,y] = [1,2];
          then x = 1 by XTUPLE_0:1;
          hence thesis by A18,A48,XTUPLE_0:1;
        end;
        suppose
A49:      [x,y] = [2,1];
          then x = 2 by XTUPLE_0:1;
          hence thesis by A35,A49,XTUPLE_0:1;
        end;
        suppose
A50:      [x,y] = [2,3];
          then x = 2 by XTUPLE_0:1;
          hence thesis by A23,A50,XTUPLE_0:1;
        end;
        suppose
A51:      [x,y] = [3,2];
          then x = 3 by XTUPLE_0:1;
          hence thesis by A39,A51,XTUPLE_0:1;
        end;
      end;
      assume
A52:  [h.x,h.y] in the InternalRel of CmpG;
      per cases by A2,ENUMSET1:def 2;
      suppose
A53:    x = 0 & y = 0;
        then h.0 in the carrier of CmpG by A52,ZFMISC_1:87;
        hence thesis by A52,A53,NECKLACE:def 5;
      end;
      suppose
        x = 0 & y = 1;
        hence thesis by ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
        x = 0 & y = 2;
        then [h.0,h.2] in (the InternalRel of G) /\ the InternalRel of CmpG
        by A44,A52,XBOOLE_0:def 4;
        then the InternalRel of G meets the InternalRel of CmpG;
        hence thesis by Th12;
      end;
      suppose
        x = 0 & y = 3;
        then [h.0,h.3] in (the InternalRel of G) /\ the InternalRel of CmpG
        by A30,A52,XBOOLE_0:def 4;
        then the InternalRel of G meets the InternalRel of CmpG;
        hence thesis by Th12;
      end;
      suppose
        x = 1 & y = 0;
        hence thesis by ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
A54:    x = 1 & y = 1;
        then h.1 in the carrier of CmpG by A52,ZFMISC_1:87;
        hence thesis by A52,A54,NECKLACE:def 5;
      end;
      suppose
        x = 1 & y = 2;
        hence thesis by ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
        x = 1 & y = 3;
        then [h.1,h.3] in (the InternalRel of G) /\ the InternalRel of CmpG
        by A28,A52,XBOOLE_0:def 4;
        then the InternalRel of G meets the InternalRel of CmpG;
        hence thesis by Th12;
      end;
      suppose
        x = 2 & y = 0;
        then [h.2,h.0] in (the InternalRel of G) /\ the InternalRel of CmpG
        by A43,A52,XBOOLE_0:def 4;
        then the InternalRel of G meets the InternalRel of CmpG;
        hence thesis by Th12;
      end;
      suppose
        x = 2 & y = 1;
        hence thesis by ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
A55:    x = 2 & y = 2;
        then h.2 in the carrier of CmpG by A52,ZFMISC_1:87;
        hence thesis by A52,A55,NECKLACE:def 5;
      end;
      suppose
        x = 2 & y = 3;
        hence thesis by ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
        x = 3 & y = 0;
        then [h.3,h.0] in (the InternalRel of G) /\ the InternalRel of CmpG
        by A29,A52,XBOOLE_0:def 4;
        then the InternalRel of G meets the InternalRel of CmpG;
        hence thesis by Th12;
      end;
      suppose
        x = 3 & y = 1;
        then [h.3,h.1] in (the InternalRel of G) /\ the InternalRel of CmpG
        by A27,A52,XBOOLE_0:def 4;
        then the InternalRel of G meets the InternalRel of CmpG;
        hence thesis by Th12;
      end;
      suppose
        x = 3 & y = 2;
        hence thesis by ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
A56:    x = 3 & y = 3;
        then h.3 in the carrier of CmpG by A52,ZFMISC_1:87;
        hence thesis by A52,A56,NECKLACE:def 5;
      end;
    end;
    hence thesis by A4,A1,A6,A8;
  end;
  assume CmpG embeds N4;
  then consider f being Function of N4, CmpG such that
A57: f is one-to-one and
A58: for x,y being Element of N4 holds [x,y] in the InternalRel of N4
  iff [f.x,f.y] in the InternalRel of CmpG;
  consider g being Function of N4,CmpN4 such that
A59: g is isomorphic by NECKLACE:29,WAYBEL_1:def 8;
A60: 2 in the carrier of N4 by A2,ENUMSET1:def 2;
A61: dom f = the carrier of N4 by FUNCT_2:def 1;
A62: [f.0,f.2] in the InternalRel of G
  proof
    assume
A63: not thesis;
    [f.0,f.2] in the InternalRel of CmpG
    proof
      f.0 in the carrier of CmpG & f.2 in the carrier of CmpG by A3,A60,
FUNCT_2:5;
      then [f.0,f.2] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
      then [f.0,f.2] in id (the carrier of G) \/ (the InternalRel of G) \/ (
      the InternalRel of CmpG) by Th14;
      then
A64:  [f.0,f.2] in id (the carrier of G) \/ (the InternalRel of G) or [f
      .0,f.2] in the InternalRel of CmpG by XBOOLE_0:def 3;
      assume not thesis;
      then [f.0,f.2] in id (the carrier of G) by A63,A64,XBOOLE_0:def 3;
      then f.0 = f.2 by RELAT_1:def 10;
      hence contradiction by A57,A61,A3,A60,FUNCT_1:def 4;
    end;
    then
A65: [0,2] in the InternalRel of N4 by A58,A3,A60;
    [0,2] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then [0,2] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A65,
XBOOLE_0:def 4;
    then the InternalRel of N4 meets the InternalRel of CmpN4;
    hence thesis by Th12;
  end;
A66: 3 in the carrier of N4 by A2,ENUMSET1:def 2;
A67: [f.0,f.3] in the InternalRel of G
  proof
    assume
A68: not [f.0,f.3] in the InternalRel of G;
    [f.0,f.3] in the InternalRel of CmpG
    proof
      f.0 in the carrier of CmpG & f.3 in the carrier of CmpG by A3,A66,
FUNCT_2:5;
      then [f.0,f.3] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
      then [f.0,f.3] in id (the carrier of G) \/ (the InternalRel of G) \/ (
      the InternalRel of CmpG) by Th14;
      then
A69:  [f.0,f.3] in id (the carrier of G) \/ (the InternalRel of G) or [f
      .0,f.3] in the InternalRel of CmpG by XBOOLE_0:def 3;
      assume not thesis;
      then [f.0,f.3] in id (the carrier of G) by A68,A69,XBOOLE_0:def 3;
      then f.0 = f.3 by RELAT_1:def 10;
      hence contradiction by A57,A61,A3,A66,FUNCT_1:def 4;
    end;
    then
A70: [0,3] in the InternalRel of N4 by A58,A3,A66;
    [0,3] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then [0,3] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A70,
XBOOLE_0:def 4;
    then the InternalRel of N4 meets the InternalRel of CmpN4;
    hence thesis by Th12;
  end;
A71: 1 in the carrier of N4 by A2,ENUMSET1:def 2;
A72: [f.1,f.3] in the InternalRel of G
  proof
    assume
A73: not [f.1,f.3] in the InternalRel of G;
    [f.1,f.3] in the InternalRel of CmpG
    proof
      f.1 in the carrier of CmpG & f.3 in the carrier of CmpG by A71,A66,
FUNCT_2:5;
      then [f.1,f.3] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
      then [f.1,f.3] in id (the carrier of G) \/ (the InternalRel of G) \/ (
      the InternalRel of CmpG) by Th14;
      then
A74:  [f.1,f.3] in id (the carrier of G) \/ (the InternalRel of G) or [f
      .1,f.3] in the InternalRel of CmpG by XBOOLE_0:def 3;
      assume not thesis;
      then [f.1,f.3] in id (the carrier of G) by A73,A74,XBOOLE_0:def 3;
      then f.1 = f.3 by RELAT_1:def 10;
      hence contradiction by A57,A61,A71,A66,FUNCT_1:def 4;
    end;
    then
A75: [1,3] in the InternalRel of N4 by A58,A71,A66;
    [1,3] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then [1,3] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A75,
XBOOLE_0:def 4;
    then the InternalRel of N4 meets the InternalRel of CmpN4;
    hence thesis by Th12;
  end;
  [3,2] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
  then
A76: [f.3,f.2] in the InternalRel of CmpG by A58,A60,A66;
  [2,3] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
  then
A77: [f.2,f.3] in the InternalRel of CmpG by A58,A60,A66;
  [1,2] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
  then
A78: [f.1,f.2] in the InternalRel of CmpG by A58,A71,A60;
  [1,0] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
  then
A79: [f.1,f.0] in the InternalRel of CmpG by A58,A3,A71;
A80: [f.2,f.0] in the InternalRel of G
  proof
    assume
A81: not [f.2,f.0] in the InternalRel of G;
    [f.2,f.0] in the InternalRel of CmpG
    proof
      f.0 in the carrier of CmpG & f.2 in the carrier of CmpG by A3,A60,
FUNCT_2:5;
      then [f.2,f.0] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
      then [f.2,f.0] in id (the carrier of G) \/ (the InternalRel of G) \/ (
      the InternalRel of CmpG) by Th14;
      then
A82:  [f.2,f.0] in id (the carrier of G) \/ (the InternalRel of G) or [f
      .2,f.0] in the InternalRel of CmpG by XBOOLE_0:def 3;
      assume not thesis;
      then [f.2,f.0] in id (the carrier of G) by A81,A82,XBOOLE_0:def 3;
      then f.0 = f.2 by RELAT_1:def 10;
      hence contradiction by A57,A61,A3,A60,FUNCT_1:def 4;
    end;
    then
A83: [2,0] in the InternalRel of N4 by A58,A3,A60;
    [2,0] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then [2,0] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A83,
XBOOLE_0:def 4;
    then the InternalRel of N4 meets the InternalRel of CmpN4;
    hence thesis by Th12;
  end;
A84: [f.3,f.0] in the InternalRel of G
  proof
    assume
A85: not [f.3,f.0] in the InternalRel of G;
    [f.3,f.0] in the InternalRel of CmpG
    proof
      f.0 in the carrier of CmpG & f.3 in the carrier of CmpG by A3,A66,
FUNCT_2:5;
      then [f.3,f.0] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
      then [f.3,f.0] in id (the carrier of G) \/ (the InternalRel of G) \/ (
      the InternalRel of CmpG) by Th14;
      then
A86:  [f.3,f.0] in id (the carrier of G) \/ (the InternalRel of G) or [f
      .3,f.0] in the InternalRel of CmpG by XBOOLE_0:def 3;
      assume not thesis;
      then [f.3,f.0] in id (the carrier of G) by A85,A86,XBOOLE_0:def 3;
      then f.0 = f.3 by RELAT_1:def 10;
      hence contradiction by A57,A61,A3,A66,FUNCT_1:def 4;
    end;
    then
A87: [3,0] in the InternalRel of N4 by A58,A3,A66;
    [3,0] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then [3,0] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A87,
XBOOLE_0:def 4;
    then the InternalRel of N4 meets the InternalRel of CmpN4;
    hence thesis by Th12;
  end;
A88: [f.3,f.1] in the InternalRel of G
  proof
    assume
A89: not [f.3,f.1] in the InternalRel of G;
    [f.3,f.1] in the InternalRel of CmpG
    proof
      f.1 in the carrier of CmpG & f.3 in the carrier of CmpG by A71,A66,
FUNCT_2:5;
      then [f.3,f.1] in [:the carrier of G,the carrier of G:] by A1,ZFMISC_1:87
;
      then [f.3,f.1] in id (the carrier of G) \/ (the InternalRel of G) \/ (
      the InternalRel of CmpG) by Th14;
      then
A90:  [f.3,f.1] in id (the carrier of G) \/ (the InternalRel of G) or [f
      .3,f.1] in the InternalRel of CmpG by XBOOLE_0:def 3;
      assume not thesis;
      then [f.3,f.1] in id (the carrier of G) by A89,A90,XBOOLE_0:def 3;
      then f.1 = f.3 by RELAT_1:def 10;
      hence contradiction by A57,A61,A71,A66,FUNCT_1:def 4;
    end;
    then
A91: [3,1] in the InternalRel of N4 by A58,A71,A66;
    [3,1] in the InternalRel of CmpN4 by Th11,ENUMSET1:def 4;
    then [3,1] in (the InternalRel of N4) /\ (the InternalRel of CmpN4) by A91,
XBOOLE_0:def 4;
    then the InternalRel of N4 meets the InternalRel of CmpN4;
    hence thesis by Th12;
  end;
  [2,1] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
  then
A92: [f.2,f.1] in the InternalRel of CmpG by A58,A71,A60;
  [0,1] in the InternalRel of N4 by ENUMSET1:def 4,NECKLA_2:2;
  then
A93: [f.0,f.1] in the InternalRel of CmpG by A58,A3,A71;
A94: for x,y being Element of CmpN4 holds [x,y] in the InternalRel of CmpN4
  iff [f.x,f.y] in the InternalRel of G
  proof
    let x,y be Element of CmpN4;
A95: the carrier of N4 = the carrier of CmpN4 by NECKLACE:def 8;
    thus [x,y] in the InternalRel of CmpN4 implies [f.x,f.y] in the
    InternalRel of G
    proof
      assume
A96:  [x,y] in the InternalRel of CmpN4;
      per cases by A96,Th11,ENUMSET1:def 4;
      suppose
A97:    [x,y] = [0,2];
        then x = 0 by XTUPLE_0:1;
        hence thesis by A62,A97,XTUPLE_0:1;
      end;
      suppose
A98:    [x,y] = [2,0];
        then x = 2 by XTUPLE_0:1;
        hence thesis by A80,A98,XTUPLE_0:1;
      end;
      suppose
A99:    [x,y] = [0,3];
        then x = 0 by XTUPLE_0:1;
        hence thesis by A67,A99,XTUPLE_0:1;
      end;
      suppose
A100:   [x,y] = [3,0];
        then x = 3 by XTUPLE_0:1;
        hence thesis by A84,A100,XTUPLE_0:1;
      end;
      suppose
A101:   [x,y] = [1,3];
        then x = 1 by XTUPLE_0:1;
        hence thesis by A72,A101,XTUPLE_0:1;
      end;
      suppose
A102:   [x,y] = [3,1];
        then x = 3 by XTUPLE_0:1;
        hence thesis by A88,A102,XTUPLE_0:1;
      end;
    end;
    assume
A103: [f.x,f.y] in the InternalRel of G;
    per cases by A2,A95,ENUMSET1:def 2;
    suppose
A104: x = 0 & y = 0;
      then f.0 in the carrier of G by A103,ZFMISC_1:87;
      hence thesis by A103,A104,NECKLACE:def 5;
    end;
    suppose
      x = 0 & y = 1;
      then [f.0,f.1] in (the InternalRel of G) /\ the InternalRel of CmpG by
A93,A103,XBOOLE_0:def 4;
      then the InternalRel of G meets the InternalRel of CmpG;
      hence thesis by Th12;
    end;
    suppose
      x = 0 & y = 2;
      hence thesis by Th11,ENUMSET1:def 4;
    end;
    suppose
      x = 0 & y = 3;
      hence thesis by Th11,ENUMSET1:def 4;
    end;
    suppose
      x = 1 & y = 0;
      then [f.1,f.0] in (the InternalRel of G) /\ the InternalRel of CmpG by
A79,A103,XBOOLE_0:def 4;
      then the InternalRel of G meets the InternalRel of CmpG;
      hence thesis by Th12;
    end;
    suppose
      x = 2 & y = 0;
      hence thesis by Th11,ENUMSET1:def 4;
    end;
    suppose
      x = 3 & y = 0;
      hence thesis by Th11,ENUMSET1:def 4;
    end;
    suppose
A105: x = 1 & y = 1;
      then f.1 in the carrier of G by A103,ZFMISC_1:87;
      hence thesis by A103,A105,NECKLACE:def 5;
    end;
    suppose
      x = 1 & y = 2;
      then [f.1,f.2] in (the InternalRel of G) /\ the InternalRel of CmpG by
A78,A103,XBOOLE_0:def 4;
      then the InternalRel of G meets the InternalRel of CmpG;
      hence thesis by Th12;
    end;
    suppose
      x = 1 & y = 3;
      hence thesis by Th11,ENUMSET1:def 4;
    end;
    suppose
      x = 2 & y = 1;
      then [f.2,f.1] in (the InternalRel of G) /\ the InternalRel of CmpG by
A92,A103,XBOOLE_0:def 4;
      then the InternalRel of G meets the InternalRel of CmpG;
      hence thesis by Th12;
    end;
    suppose
A106: x = 2 & y = 2;
      then f.2 in the carrier of G by A103,ZFMISC_1:87;
      hence thesis by A103,A106,NECKLACE:def 5;
    end;
    suppose
      x = 2 & y = 3;
      then [f.2,f.3] in (the InternalRel of G) /\ the InternalRel of CmpG by
A77,A103,XBOOLE_0:def 4;
      then the InternalRel of G meets the InternalRel of CmpG;
      hence thesis by Th12;
    end;
    suppose
      x = 3 & y = 1;
      hence thesis by Th11,ENUMSET1:def 4;
    end;
    suppose
      x = 3 & y = 2;
      then [f.3,f.2] in (the InternalRel of G) /\ the InternalRel of CmpG by
A76,A103,XBOOLE_0:def 4;
      then the InternalRel of G meets the InternalRel of CmpG;
      hence thesis by Th12;
    end;
    suppose
A107: x = 3 & y = 3;
      then f.3 in the carrier of G by A103,ZFMISC_1:87;
      hence thesis by A103,A107,NECKLACE:def 5;
    end;
  end;
  reconsider f as Function of CmpN4,G by A4,NECKLACE:def 8;
  reconsider h = f*g as Function of N4,G;
A108: g is one-to-one monotone by A59,WAYBEL_0:def 38;
  for x,y being Element of N4 holds [x,y] in the InternalRel of N4 iff [
  h.x,h.y] in the InternalRel of G
  proof
    let x,y be Element of N4;
    thus [x,y] in the InternalRel of N4 implies [h.x,h.y] in the InternalRel
    of G
    proof
      assume [x,y] in the InternalRel of N4;
      then x <= y by ORDERS_2:def 5;
      then g.x <= g.y by A108,WAYBEL_1:def 2;
      then [g.x,g.y] in the InternalRel of CmpN4 by ORDERS_2:def 5;
      then [f.(g.x),f.(g.y)] in the InternalRel of G by A94;
      then [(f*g).x,f.(g.y)] in the InternalRel of G by FUNCT_2:15;
      hence thesis by FUNCT_2:15;
    end;
    assume [h.x,h.y] in the InternalRel of G;
    then [f.(g.x),h.y] in the InternalRel of G by FUNCT_2:15;
    then [f.(g.x),f.(g.y)] in the InternalRel of G by FUNCT_2:15;
    then [g.x,g.y] in the InternalRel of CmpN4 by A94;
    then g.x <= g.y by ORDERS_2:def 5;
    then x <= y by A59,WAYBEL_0:66;
    hence thesis by ORDERS_2:def 5;
  end;
  hence thesis by A57,A108;
end;

theorem Th25:
  for G being non empty irreflexive RelStr holds G is N-free iff
  ComplRelStr G is N-free
proof
  let G be non empty irreflexive RelStr;
  thus G is N-free implies ComplRelStr G is N-free
  proof
    assume
A1: G is N-free;
    assume not thesis;
    then ComplRelStr G embeds Necklace 4 by NECKLA_2:def 1;
    then G embeds Necklace 4 by Th24;
    hence contradiction by A1,NECKLA_2:def 1;
  end;
  assume
A2: ComplRelStr G is N-free;
  assume not thesis;
  then G embeds Necklace 4 by NECKLA_2:def 1;
  then ComplRelStr G embeds Necklace 4 by Th24;
  hence contradiction by A2,NECKLA_2:def 1;
end;

begin :: Connected Graphs

definition
  let R be RelStr;
  mode path of R is RedSequence of the InternalRel of R;
end;

definition
  let R be RelStr;
  attr R is path-connected means

  for x,y being set st x in the carrier
of R & y in the carrier of R & x <> y holds the InternalRel of R reduces x,y or
  the InternalRel of R reduces y,x;
end;

registration
  cluster empty -> path-connected for RelStr;
  correctness;
end;

registration
  cluster connected -> path-connected for non empty RelStr;
  correctness
  proof
    let R be non empty RelStr;
    set cR = the carrier of R, IR = the InternalRel of R;
    assume
A1: R is connected;
    for x,y being set st x in the carrier of R & y in the carrier of R & x
<> y holds (the InternalRel of R) reduces x,y or (the InternalRel of R) reduces
    y,x
    proof
      let x,y being set such that
A2:   x in cR & y in cR and
      x <> y;
      reconsider x,y as Element of R by A2;
A3:   x <= y or y <= x by A1,WAYBEL_0:def 29;
      per cases by A3,ORDERS_2:def 5;
      suppose
A4:     [x,y] in IR;
A5:     len <*x,y*> = 2 & <*x,y*>.1 = x by FINSEQ_1:44;
A6:     <*x,y*>.2 = y by FINSEQ_1:44;
        <*x,y*> is RedSequence of IR by A4,REWRITE1:7;
        hence thesis by A5,A6,REWRITE1:def 3;
      end;
      suppose
A7:     [y,x] in IR;
A8:     len <*y,x*> = 2 & <*y,x*>.1 = y by FINSEQ_1:44;
A9:     <*y,x*>.2 = x by FINSEQ_1:44;
        <*y,x*> is RedSequence of IR by A7,REWRITE1:7;
        hence thesis by A8,A9,REWRITE1:def 3;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th26:
  for R being non empty transitive reflexive RelStr, x,y being
  Element of R holds the InternalRel of R reduces x,y implies [x,y] in the
  InternalRel of R
proof
  let R be non empty transitive reflexive RelStr;
  let x,y be Element of R;
  set cR = the carrier of R, IR = the InternalRel of R;
  assume IR reduces x,y;
  then consider p being RedSequence of IR such that
A1: p.1 = x and
A2: p.len p = y by REWRITE1:def 3;
  reconsider p as FinSequence;
  defpred P[Nat] means $1 in dom p implies [p.1,p.$1] in IR;
A3: IR is_transitive_in cR by ORDERS_2:def 3;
A4: for k be non zero Nat st P[k] holds P[k+1]
  proof
    let k be non zero Nat such that
A5: P[k];
    assume
A6: k+1 in dom p;
    then k <= k+1 & k+1 <= len p by FINSEQ_3:25,NAT_1:11;
    then
A7: 0 + 1 <= k & k <= len p by NAT_1:13;
    then
A8: p.1 in cR by A5,FINSEQ_3:25,ZFMISC_1:87;
    k in dom p by A7,FINSEQ_3:25;
    then
A9: [p.k,p.(k+1)] in IR by A6,REWRITE1:def 2;
    then p.k in cR & p.(k+1) in cR by ZFMISC_1:87;
    hence thesis by A3,A5,A7,A9,A8,FINSEQ_3:25;
  end;
  IR is_reflexive_in cR by ORDERS_2:def 2;
  then
A10: P[1] by A1;
A11: for k be non zero Nat holds P[k] from NAT_1:sch 10(A10,A4);
A12: len p > 0 by REWRITE1:def 2;
  then 0 + 1 <= len p by NAT_1:13;
  then len p in dom p by FINSEQ_3:25;
  hence thesis by A1,A2,A12,A11;
end;

registration
  cluster path-connected -> connected for
non empty transitive reflexive RelStr;
  correctness
  proof
    let R be non empty transitive reflexive RelStr;
    set IR = the InternalRel of R;
    assume
A1: R is path-connected;
    for x,y being Element of R holds x <= y or y <= x
    proof
      let x,y being Element of R;
      per cases;
      suppose
        x = y;
        hence thesis;
      end;
      suppose
        x <> y;
        then IR reduces x,y or IR reduces y,x by A1;
        then [x,y] in IR or [y,x] in IR by Th26;
        hence thesis by ORDERS_2:def 5;
      end;
    end;
    hence thesis by WAYBEL_0:def 29;
  end;
end;

theorem Th27:
  for R be symmetric RelStr,x,y being set holds the InternalRel of
  R reduces x,y implies the InternalRel of R reduces y,x
proof
  let R be symmetric RelStr;
  set IR = the InternalRel of R;
  let x,y be set;
A1: IR = IR~ by RELAT_2:13;
  assume IR reduces x,y;
  then consider p being RedSequence of IR such that
A2: p.1 = x and
A3: p.len p = y by REWRITE1:def 3;
  reconsider p as FinSequence;
A4: (Rev p).len p = x by A2,FINSEQ_5:62;
  IR reduces y,x
  proof
    reconsider q = Rev p as RedSequence of IR by A1,REWRITE1:9;
    q.1 = y & q.len q = x by A3,A4,FINSEQ_5:62,def 3;
    hence thesis by REWRITE1:def 3;
  end;
  hence thesis;
end;

definition
  let R be symmetric RelStr;
  redefine attr R is path-connected means

  for x,y being set st x in the
  carrier of R & y in the carrier of R & x <> y holds (the InternalRel of R)
  reduces x,y;
  compatibility
  proof
    set IR = the InternalRel of R, cR = the carrier of R;
    thus R is path-connected implies for x,y being set st x in the carrier of
    R & y in the carrier of R & x <> y holds (the InternalRel of R) reduces x,y
    proof
      assume
A1:   R is path-connected;
      let x,y being set such that
A2:   x in cR & y in cR & x <> y;
      per cases by A1,A2;
      suppose
        IR reduces x,y;
        hence thesis;
      end;
      suppose
        IR reduces y,x;
        hence thesis by Th27;
      end;
    end;
    assume for x,y be set st x in the carrier of R & y in the carrier of R &
    x <> y holds IR reduces x,y;
    then
    for x,y being set st x in the carrier of R & y in the carrier of R & x
<> y holds (the InternalRel of R) reduces x,y or (the InternalRel of R) reduces
    y,x;
    hence thesis;
  end;
end;

definition
  let R be RelStr;
  let x be Element of R;
  func component x -> Subset of R equals
  Class(EqCl the InternalRel of R, x);
  coherence;
end;

registration
  let R be non empty RelStr;
  let x be Element of R;
  cluster component x -> non empty;
  correctness by EQREL_1:20;
end;

theorem Th28:
  for R being RelStr, x being Element of R, y be set st y in
  component x holds [x,y] in EqCl the InternalRel of R
proof
  let R be RelStr;
  let x be Element of R;
  let y be set;
  set IR = the InternalRel of R;
  assume y in component x;
  then [y,x] in EqCl IR by EQREL_1:19;
  hence thesis by EQREL_1:6;
end;

theorem Th29:
  for R being RelStr, x being Element of R, A being set holds A =
component x iff
  for y being object holds y in A iff [x,y] in EqCl the InternalRel of R
proof
  let R be RelStr;
  let x being Element of R;
  let A be set;
  set IR = the InternalRel of R;
A1: (for y being object
  holds y in A iff [x,y] in EqCl (the InternalRel of R))
  implies A = component x
  proof
    assume
A2: for y being object holds y in A iff [x,y] in EqCl (the InternalRel of R);
A3: component x c= A
    proof
      let a be object;
      assume a in component x;
      then [a,x] in EqCl IR by EQREL_1:19;
      then [x,a] in EqCl IR by EQREL_1:6;
      hence thesis by A2;
    end;
    A c= component x
    proof
      let a be object;
      assume a in A;
      then [x,a] in EqCl IR by A2;
      then [a,x] in EqCl IR by EQREL_1:6;
      hence thesis by EQREL_1:19;
    end;
    hence thesis by A3;
  end;
  A = component x implies
   for y being object holds [x,y] in EqCl IR implies y in A
  proof
    assume
A4: A = component x;
    let y be object;
    assume [x,y] in EqCl IR;
    then [y,x] in EqCl IR by EQREL_1:6;
    hence thesis by A4,EQREL_1:19;
  end;
  hence thesis by A1,Th28;
end;

theorem Th30:
  for R be non empty irreflexive symmetric RelStr holds R is not
  path-connected implies ex G1,G2 being non empty strict irreflexive symmetric
  RelStr st the carrier of G1 misses the carrier of G2 & the RelStr of R =
  union_of(G1,G2)
proof
  let R be non empty irreflexive symmetric RelStr;
  set cR = the carrier of R, IR = the InternalRel of R;
  assume R is not path-connected;
  then consider x,y being set such that
A1: x in cR & y in cR and
  x <> y and
A2: not IR reduces x,y;
  reconsider x,y as Element of R by A1;
  set A1 = component x, A2 = (the carrier of R) \ A1;
  reconsider A2 as Subset of R;
  set G1 = subrelstr A1, G2 = subrelstr A2;
A3: the carrier of G2 = A2 by YELLOW_0:def 15;
  cR c= A1 \/ A2
  proof
    let a be object;
    assume
A4: a in cR;
    assume not thesis;
    then ( not a in A1)& not a in A2 by XBOOLE_0:def 3;
    hence contradiction by A4,XBOOLE_0:def 5;
  end;
  then
A5: cR = A1 \/ A2;
A6: the carrier of G1 = A1 by YELLOW_0:def 15;
  then
A7: (the carrier of G1) misses (the carrier of G2) by A3,XBOOLE_1:79;
A8: the InternalRel of G1 misses the InternalRel of G2
  proof
    set IG1 = the InternalRel of G1, IG2 = the InternalRel of G2;
    assume not thesis;
    then IG1 /\ IG2 <> {};
    then consider a be object such that
A9: a in IG1 /\ IG2 by XBOOLE_0:def 1;
    a in IG1 by A9,XBOOLE_0:def 4;
    then consider c1,c2 be object such that
A10: a = [c1,c2] and
A11: c1 in A1 and
    c2 in A1 by A6,RELSET_1:2;
    ex g1,g2 be object st a = [g1,g2] & g1 in A2 & g2 in A2
by A3,A9,RELSET_1:2;
    then c1 in A2 by A10,XTUPLE_0:1;
    then c1 in A1 /\ A2 by A11,XBOOLE_0:def 4;
    hence contradiction by A6,A3,A7;
  end;
A12: the InternalRel of G2 = IR \ (the InternalRel of G1)
  proof
    set IG1 = the InternalRel of G1, IG2 = the InternalRel of G2;
    thus IG2 c= IR \ IG1
    proof
      let a be object;
      assume
A13:  a in IG2;
      then consider g1,g2 be object such that
A14:  a = [g1,g2] and
A15:  g1 in A2 & g2 in A2 by A3,RELSET_1:2;
      reconsider g1,g2 as Element of G2 by A15,YELLOW_0:def 15;
      reconsider u1 = g1, u2 = g2 as Element of R by A15;
A16:  not a in IG1
      by A13,XBOOLE_0:def 4,A8;
      g1 <= g2 by A13,A14,ORDERS_2:def 5;
      then u1 <= u2 by YELLOW_0:59;
      then a in IR by A14,ORDERS_2:def 5;
      hence thesis by A16,XBOOLE_0:def 5;
    end;
    let a be object;
    assume
A17: a in IR \ IG1;
    then
A18: a in IR by XBOOLE_0:def 5;
A19: not a in IG1 by A17,XBOOLE_0:def 5;
    consider c1,c2 be object such that
A20: a = [c1,c2] and
A21: c1 in cR & c2 in cR by A17,RELSET_1:2;
    reconsider c1,c2 as Element of R by A21;
A22: c1 <= c2 by A18,A20,ORDERS_2:def 5;
    per cases by A5,XBOOLE_0:def 3;
    suppose
A23:  c1 in A1 & c2 in A1;
      then reconsider d2 = c2 as Element of G1 by YELLOW_0:def 15;
      reconsider d1 = c1 as Element of G1 by A23,YELLOW_0:def 15;
      d1 <= d2 by A6,A22,YELLOW_0:60;
      hence thesis by A19,A20,ORDERS_2:def 5;
    end;
    suppose
A24:  c1 in A1 & c2 in A2;
A25:  [:A1,A2:] misses IR
      proof
        assume not thesis;
        then [:A1,A2:] /\ IR <> {};
        then consider b be object such that
A26:    b in [:A1,A2:] /\ IR by XBOOLE_0:def 1;
A27:    b in IR by A26,XBOOLE_0:def 4;
        b in [:A1,A2:] by A26,XBOOLE_0:def 4;
        then consider b1,b2 be object such that
A28:    b1 in A1 and
A29:    b2 in A2 and
A30:    b = [b1,b2] by ZFMISC_1:def 2;
        reconsider b2 as Element of R by A29;
        reconsider b1 as Element of R by A28;
        IR c= EqCl IR & [x,b1] in EqCl IR by A28,Th29,MSUALG_5:def 1;
        then [x,b2] in EqCl IR by A27,A30,EQREL_1:7;
        then b2 in A1 by Th29;
        then b2 in A1 /\ A2 by A29,XBOOLE_0:def 4;
        hence thesis by A6,A3,A7;
      end;
      a in [:A1,A2:] by A20,A24,ZFMISC_1:def 2;
      then a in [:A1,A2:] /\ IR by A18,XBOOLE_0:def 4;
      hence thesis by A25;
    end;
    suppose
A31:  c1 in A2 & c2 in A1;
A32:  [:A2,A1:] misses IR
      proof
        assume not thesis;
        then [:A2,A1:] /\ IR <> {};
        then consider b be object such that
A33:    b in [:A2,A1:] /\ IR by XBOOLE_0:def 1;
        b in [:A2,A1:] by A33,XBOOLE_0:def 4;
        then consider b1,b2 be object such that
A34:    b1 in A2 and
A35:    b2 in A1 and
A36:    b = [b1,b2] by ZFMISC_1:def 2;
        reconsider b1 as Element of R by A34;
        reconsider b2 as Element of R by A35;
A37:    [x,b2] in EqCl IR by A35,Th29;
A38:    IR c= EqCl IR by MSUALG_5:def 1;
        b in IR by A33,XBOOLE_0:def 4;
        then [b2,b1] in EqCl IR by A36,A38,EQREL_1:6;
        then [x,b1] in EqCl IR by A37,EQREL_1:7;
        then b1 in A1 by Th29;
        then b1 in A1 /\ A2 by A34,XBOOLE_0:def 4;
        hence thesis by A6,A3,A7;
      end;
      a in [:A2,A1:] by A20,A31,ZFMISC_1:def 2;
      then a in [:A2,A1:] /\ IR by A18,XBOOLE_0:def 4;
      hence thesis by A32;
    end;
    suppose
A39:  c1 in A2 & c2 in A2;
      then reconsider d2 = c2 as Element of G2 by YELLOW_0:def 15;
      reconsider d1 = c1 as Element of G2 by A39,YELLOW_0:def 15;
      d1 <= d2 by A3,A22,A39,YELLOW_0:60;
      hence thesis by A20,ORDERS_2:def 5;
    end;
  end;
  IR = (the InternalRel of G1) \/ (the InternalRel of G2)
  proof
    set IG1 = the InternalRel of G1, IG2 = the InternalRel of G2;
    thus IR c= IG1 \/ IG2
    proof
      let a be object;
      assume
A40:  a in IR;
      assume not thesis;
      then ( not a in IG1)& not a in IG2 by XBOOLE_0:def 3;
      hence contradiction by A12,A40,XBOOLE_0:def 5;
    end;
    let a be object;
    assume
A41: a in IG1 \/ IG2;
    per cases by A41,XBOOLE_0:def 3;
    suppose
A42:  a in IG1;
      then consider v,w be object such that
A43:  a = [v,w] and
A44:  v in A1 & w in A1 by A6,RELSET_1:2;
      reconsider v,w as Element of G1 by A44,YELLOW_0:def 15;
      reconsider u1 = v, u2 = w as Element of R by A44;
      v <= w by A42,A43,ORDERS_2:def 5;
      then u1 <= u2 by YELLOW_0:59;
      hence thesis by A43,ORDERS_2:def 5;
    end;
    suppose
A45:  a in IG2;
      then consider v,w be object such that
A46:  a = [v,w] and
A47:  v in A2 & w in A2 by A3,RELSET_1:2;
      reconsider v,w as Element of G2 by A47,YELLOW_0:def 15;
      reconsider u1 = v, u2 = w as Element of R by A47;
      v <= w by A45,A46,ORDERS_2:def 5;
      then u1 <= u2 by YELLOW_0:59;
      hence thesis by A46,ORDERS_2:def 5;
    end;
  end;
  then
A48: IR = the InternalRel of union_of(G1,G2) by NECKLA_2:def 2;
  IR = IR~ by RELAT_2:13;
  then not IR \/ IR~ reduces x,y by A2;
  then not x,y are_convertible_wrt IR by REWRITE1:def 4;
  then not [x,y] in EqCl IR by MSUALG_6:41;
  then not y in A1 by Th29;
  then
A49: G2 is non empty strict RelStr by A3,XBOOLE_0:def 5;
  cR = the carrier of union_of(G1,G2) by A6,A3,A5,NECKLA_2:def 2;
  hence thesis by A6,A7,A49,A48;
end;

theorem Th31:
  for R be non empty irreflexive symmetric RelStr holds
  ComplRelStr R is not path-connected implies ex G1,G2 being non empty strict
  irreflexive symmetric RelStr st the carrier of G1 misses the carrier of G2 &
  the RelStr of R = sum_of(G1,G2)
proof
  let R be non empty irreflexive symmetric RelStr;
  set cR = the carrier of R, IR = the InternalRel of R, CR = ComplRelStr R,
  ICR = the InternalRel of ComplRelStr R, cCR = the carrier of ComplRelStr R;
  assume CR is not path-connected;
  then consider x,y being set such that
A1: x in cCR and
A2: y in cCR and
  x <> y and
A3: not ICR reduces x,y;
  reconsider x,y as Element of CR by A1,A2;
  set A1 = component x, A2 = (the carrier of R) \ A1;
  reconsider A1 as Subset of R by NECKLACE:def 8;
  ICR = ICR~ by RELAT_2:13;
  then not ICR \/ ICR~ reduces x,y by A3;
  then not x,y are_convertible_wrt ICR by REWRITE1:def 4;
  then not [x,y] in EqCl ICR by MSUALG_6:41;
  then
A4: not y in A1 by Th29;
  reconsider A2 as Subset of R;
  set G1 = subrelstr A1, G2 = subrelstr A2;
A5: the carrier of G1 = A1 by YELLOW_0:def 15;
  set IG1 = the InternalRel of G1, IG2 = the InternalRel of G2, G1G2 = [:the
carrier of G1,the carrier of G2:], G2G1 = [:the carrier of G2,the carrier of G1
  :];
A6: cR = A1 \/ A2
  proof
    thus cR c= A1 \/ A2
    proof
      let a be object;
      assume
A7:   a in cR;
      assume not thesis;
      then ( not a in A1)& not a in A2 by XBOOLE_0:def 3;
      hence contradiction by A7,XBOOLE_0:def 5;
    end;
    let a be object;
    assume
A8: a in A1 \/ A2;
    per cases by A8,XBOOLE_0:def 3;
    suppose
      a in A1;
      hence thesis;
    end;
    suppose
      a in A2;
      hence thesis;
    end;
  end;
A9: the carrier of G2 = A2 by YELLOW_0:def 15;
  then
A10: (the carrier of G1) misses (the carrier of G2) by A5,XBOOLE_1:79;
A11: the InternalRel of G1 misses the InternalRel of G2
  proof
    assume not thesis;
    then IG1 /\ IG2 <> {};
    then consider a be object such that
A12: a in IG1 /\ IG2 by XBOOLE_0:def 1;
    a in IG1 by A12,XBOOLE_0:def 4;
    then consider c1,c2 be object such that
A13: a = [c1,c2] and
A14: c1 in A1 and
    c2 in A1 by A5,RELSET_1:2;
    ex g1,g2 be object st a = [g1,g2] & g1 in A2 & g2 in A2
by A9,A12,RELSET_1:2;
    then c1 in A2 by A13,XTUPLE_0:1;
    then c1 in A1 /\ A2 by A14,XBOOLE_0:def 4;
    hence contradiction by A5,A9,A10;
  end;
A15: the InternalRel of G2 = IR \ IG1 \ G1G2 \ G2G1
  proof
    thus IG2 c= IR \ IG1 \ G1G2 \ G2G1
    proof
      let a be object;
      assume
A16:  a in IG2;
      then consider g1,g2 be object such that
A17:  a = [g1,g2] and
A18:  g1 in A2 and
A19:  g2 in A2 by A9,RELSET_1:2;
      reconsider g1,g2 as Element of G2 by A18,A19,YELLOW_0:def 15;
      reconsider u1 = g1, u2 = g2 as Element of R by A18,A19;
A20:  not a in IG1
      by A16,XBOOLE_0:def 4,A11;
A21:  not a in G2G1
      proof
        assume a in G2G1;
        then g2 in A1 by A5,A17,ZFMISC_1:87;
        then g2 in A1 /\ A2 by A19,XBOOLE_0:def 4;
        hence thesis by A5,A9,A10;
      end;
A22:  not a in G1G2
      proof
        assume a in G1G2;
        then g1 in A1 by A5,A17,ZFMISC_1:87;
        then g1 in A1 /\ A2 by A18,XBOOLE_0:def 4;
        hence thesis by A5,A9,A10;
      end;
      g1 <= g2 by A16,A17,ORDERS_2:def 5;
      then u1 <= u2 by YELLOW_0:59;
      then a in IR by A17,ORDERS_2:def 5;
      then a in IR \ IG1 by A20,XBOOLE_0:def 5;
      then a in IR \ IG1 \ G1G2 by A22,XBOOLE_0:def 5;
      hence thesis by A21,XBOOLE_0:def 5;
    end;
    let a be object;
    assume
A23: a in IR \ IG1 \ G1G2 \ G2G1;
    then
A24: not a in G2G1 by XBOOLE_0:def 5;
A25: a in IR \ IG1 \ G1G2 by A23,XBOOLE_0:def 5;
    then
A26: a in IR \ IG1 by XBOOLE_0:def 5;
    then
A27: not a in IG1 by XBOOLE_0:def 5;
A28: not a in G1G2 by A25,XBOOLE_0:def 5;
    consider c1,c2 be object such that
A29: a = [c1,c2] and
A30: c1 in cR & c2 in cR by A23,RELSET_1:2;
    reconsider c1,c2 as Element of R by A30;
    a in IR by A26,XBOOLE_0:def 5;
    then
A31: c1 <= c2 by A29,ORDERS_2:def 5;
    per cases by A6,XBOOLE_0:def 3;
    suppose
A32:  c1 in A1 & c2 in A1;
      then reconsider d2 = c2 as Element of G1 by YELLOW_0:def 15;
      reconsider d1 = c1 as Element of G1 by A32,YELLOW_0:def 15;
      d1 <= d2 by A5,A31,YELLOW_0:60;
      hence thesis by A27,A29,ORDERS_2:def 5;
    end;
    suppose
      c1 in A1 & c2 in A2;
      hence thesis by A5,A9,A28,A29,ZFMISC_1:87;
    end;
    suppose
      c1 in A2 & c2 in A1;
      hence thesis by A5,A9,A24,A29,ZFMISC_1:87;
    end;
    suppose
A33:  c1 in A2 & c2 in A2;
      then reconsider d1 = c1,d2 = c2 as Element of G2 by YELLOW_0:def 15;
      d1 <= d2 by A9,A31,A33,YELLOW_0:60;
      hence thesis by A29,ORDERS_2:def 5;
    end;
  end;
  IR = (the InternalRel of G1) \/ (the InternalRel of G2) \/ [:the
  carrier of G1,the carrier of G2:] \/ [:the carrier of G2,the carrier of G1:]
  proof
    set G1G2 = [:the carrier of G1,the carrier of G2:], G2G1 = [:the carrier
    of G2,the carrier of G1:];
    thus IR c= IG1 \/ IG2 \/ G1G2 \/ G2G1
    proof
      let a be object;
      assume
A34:  a in IR;
      assume
A35:  not thesis;
      then
A36:  not a in (IG1 \/ IG2 \/ G1G2) by XBOOLE_0:def 3;
      then
A37:  not a in (IG1 \/ IG2) by XBOOLE_0:def 3;
      then not a in IG2 by XBOOLE_0:def 3;
      then not a in IR \ IG1 \ G1G2 or a in G2G1 by A15,XBOOLE_0:def 5;
      then
A38:  not a in IR \ IG1 or a in G1G2 or a in G2G1 by XBOOLE_0:def 5;
      not a in IG1 by A37,XBOOLE_0:def 3;
      hence thesis by A34,A35,A36,A38,XBOOLE_0:def 3,def 5;
    end;
    let a be object;
    assume a in IG1 \/ IG2 \/ G1G2 \/ G2G1;
    then a in IG1 \/ IG2 \/ G1G2 or a in G2G1 by XBOOLE_0:def 3;
    then
A39: a in IG1 \/ IG2 or a in G1G2 or a in G2G1 by XBOOLE_0:def 3;
    per cases by A39,XBOOLE_0:def 3;
    suppose
A40:  a in IG1;
      then consider v,w be object such that
A41:  a = [v,w] and
A42:  v in A1 & w in A1 by A5,RELSET_1:2;
      reconsider v,w as Element of G1 by A42,YELLOW_0:def 15;
      reconsider u1 = v, u2 = w as Element of R by A42;
      v <= w by A40,A41,ORDERS_2:def 5;
      then u1 <= u2 by YELLOW_0:59;
      hence thesis by A41,ORDERS_2:def 5;
    end;
    suppose
A43:  a in IG2;
      then consider v,w be object such that
A44:  a = [v,w] and
A45:  v in A2 & w in A2 by A9,RELSET_1:2;
      reconsider v,w as Element of G2 by A45,YELLOW_0:def 15;
      reconsider u1 = v, u2 = w as Element of R by A45;
      v <= w by A43,A44,ORDERS_2:def 5;
      then u1 <= u2 by YELLOW_0:59;
      hence thesis by A44,ORDERS_2:def 5;
    end;
    suppose
A46:  a in G1G2;
      assume
A47:  not thesis;
      consider v,w be object such that
A48:  a = [v,w] by A46,RELAT_1:def 1;
A49:  w in A2 by A9,A46,A48,ZFMISC_1:87;
A50:  v in A1 by A5,A46,A48,ZFMISC_1:87;
      then reconsider v,w as Element of CR by A49,NECKLACE:def 8;
      v <> w
      by A5,A9,A10,A50,A49,XBOOLE_0:def 4;
      then
A51:  not a in id cR by A48,RELAT_1:def 10;
      [v,w] in [:cR,cR:] by A50,A49,ZFMISC_1:87;
      then a in [:cR,cR:] \ IR by A48,A47,XBOOLE_0:def 5;
      then a in IR` by SUBSET_1:def 4;
      then a in IR` \ id cR by A51,XBOOLE_0:def 5;
      then [v,w] in ICR by A48,NECKLACE:def 8;
      then v,w are_convertible_wrt ICR by REWRITE1:29;
      then
A52:  [v,w] in EqCl ICR by MSUALG_6:41;
      [x,v] in EqCl ICR by A50,Th29;
      then [x,w] in EqCl ICR by A52,EQREL_1:7;
      then w in component x by Th29;
      then w in A1 /\ A2 by A49,XBOOLE_0:def 4;
      hence thesis by A5,A9,A10;
    end;
    suppose
A53:  a in G2G1;
      assume
A54:  not thesis;
      consider v,w be object such that
A55:  a = [v,w] by A53,RELAT_1:def 1;
A56:  w in A1 by A5,A53,A55,ZFMISC_1:87;
A57:  v in A2 by A9,A53,A55,ZFMISC_1:87;
      then reconsider v,w as Element of CR by A56,NECKLACE:def 8;
      v <> w
      by A5,A9,A10,A57,A56,XBOOLE_0:def 4;
      then
A58:  not a in id cR by A55,RELAT_1:def 10;
      [v,w] in [:cR,cR:] by A57,A56,ZFMISC_1:87;
      then a in [:cR,cR:] \ IR by A55,A54,XBOOLE_0:def 5;
      then a in IR` by SUBSET_1:def 4;
      then a in IR` \ id cR by A58,XBOOLE_0:def 5;
      then [v,w] in ICR by A55,NECKLACE:def 8;
      then v,w are_convertible_wrt ICR by REWRITE1:29;
      then [v,w] in EqCl ICR by MSUALG_6:41;
      then
A59:  [w,v] in EqCl ICR by EQREL_1:6;
      [x,w] in EqCl ICR by A56,Th29;
      then [x,v] in EqCl ICR by A59,EQREL_1:7;
      then v in component x by Th29;
      then v in A1 /\ A2 by A57,XBOOLE_0:def 4;
      hence thesis by A5,A9,A10;
    end;
  end;
  then
A60: IR = the InternalRel of sum_of(G1,G2) by NECKLA_2:def 3;
  y in cR by A2,NECKLACE:def 8;
  then
A61: G2 is non empty strict RelStr by A9,A4,XBOOLE_0:def 5;
  cR = the carrier of sum_of(G1,G2) by A5,A9,A6,NECKLA_2:def 3;
  hence thesis by A5,A10,A61,A60;
end;

Lm1: for X being non empty finite set, A,B being non empty set st X = A \/ B &
A misses B holds card A in Segm card X
proof
  let X be non empty finite set;
  let A,B be non empty set;
  set n = card X;
  assume that
A1: X = A \/ B and
A2: A misses B;
  card B c= n by A1,CARD_1:11,XBOOLE_1:7;
  then reconsider B as finite set;
  card A c= n by A1,CARD_1:11,XBOOLE_1:7;
  then reconsider A as finite set;
A3: card B >= 1 by NAT_1:14;
A4: n = card A + card B by A1,A2,CARD_2:40;
  card A < n
  proof
    assume not thesis;
    then card A + card B >= n+1 by A3,XREAL_1:7;
    hence thesis by A4,NAT_1:13;
  end;
  hence thesis by NAT_1:44;
end;

theorem
  for G being irreflexive RelStr st G in fin_RelStr_sp holds ComplRelStr
  G in fin_RelStr_sp
proof
  defpred P[Nat] means for G being irreflexive RelStr st card the carrier of G
  = $1 & G in fin_RelStr_sp holds ComplRelStr G in fin_RelStr_sp;
  let G be irreflexive RelStr;
A1: for k being Nat st for n being Nat st n < k holds P[n] holds P[k]
  proof
    let k be Nat such that
A2: for n being Nat st n < k holds P[n];
    let G be irreflexive RelStr;
    assume that
A3: card the carrier of G = k and
A4: G in fin_RelStr_sp;
    per cases by A4,NECKLA_2:6;
    suppose
      G is strict 1-element RelStr;
      hence thesis by A4,Th15;
    end;
    suppose
      ex G1,G2 being strict RelStr st (the carrier of G1) misses (the
carrier of G2) & G1 in fin_RelStr_sp & G2 in fin_RelStr_sp & (G = union_of(G1,
      G2) or G = sum_of(G1,G2) );
      then consider G1,G2 being strict RelStr such that
A5:   (the carrier of G1) misses the carrier of G2 and
A6:   G1 in fin_RelStr_sp and
A7:   G2 in fin_RelStr_sp and
A8:   G = union_of(G1,G2) or G = sum_of(G1,G2);
A9:   G2 is non empty finite by A7,NECKLA_2:4;
      then reconsider n2 = card the carrier of G2 as Nat;
A10:  G1 is non empty finite by A6,NECKLA_2:4;
      then reconsider n1 = card the carrier of G1 as Nat;
      thus thesis
      proof
        per cases by A8;
        suppose
A11:      G = union_of(G1,G2);
          then reconsider G2 as irreflexive RelStr by Th9;
          reconsider G1 as irreflexive RelStr by A11,Th9;
          reconsider cG1 = the carrier of G1 as non empty finite set by A10;
          reconsider cG2 = the carrier of G2 as non empty finite set by A9;
          the carrier of G = (the carrier of G1) \/ the carrier of G2 by A11,
NECKLA_2:def 2;
          then
A12:      card the carrier of G = card cG1 + card cG2 by A5,CARD_2:40;
A13:      card cG1 = n1;
          n2 < k
          proof
            assume not thesis;
            then k+0 < n1 + n2 by A13,XREAL_1:8;
            hence thesis by A3,A12;
          end;
          then
A14:      ComplRelStr G2 in fin_RelStr_sp by A2,A7;
A15:      the carrier of ComplRelStr G1 = the carrier of G1 & the carrier
          of ComplRelStr G2 = the carrier of G2 by NECKLACE:def 8;
A16:      card cG2 = n2;
          n1 < k
          proof
            assume not thesis;
            then k+0 < n2 + n1 by A16,XREAL_1:8;
            hence thesis by A3,A12;
          end;
          then
A17:      ComplRelStr G1 in fin_RelStr_sp by A2,A6;
          ComplRelStr G = sum_of(ComplRelStr G1,ComplRelStr G2) by A5,A11,Th17;
          hence thesis by A5,A17,A14,A15,NECKLA_2:def 5;
        end;
        suppose
A18:      G = sum_of(G1,G2);
          then reconsider G2 as irreflexive RelStr by Th9;
          reconsider G1 as irreflexive RelStr by A18,Th9;
          reconsider cG1 = the carrier of G1 as non empty finite set by A10;
          reconsider cG2 = the carrier of G2 as non empty finite set by A9;
          the carrier of G = (the carrier of G1) \/ the carrier of G2 by A18,
NECKLA_2:def 3;
          then
A19:      card the carrier of G = card cG1 + card cG2 by A5,CARD_2:40;
A20:      card cG1 = n1;
          n2 < k
          proof
            assume not thesis;
            then k+0 < n1 + n2 by A20,XREAL_1:8;
            hence thesis by A3,A19;
          end;
          then
A21:      ComplRelStr G2 in fin_RelStr_sp by A2,A7;
A22:      the carrier of ComplRelStr G1 = the carrier of G1 & the carrier
          of ComplRelStr G2 = the carrier of G2 by NECKLACE:def 8;
A23:      card cG2 = n2;
          n1 < k
          proof
            assume not thesis;
            then k+0 < n2 + n1 by A23,XREAL_1:8;
            hence thesis by A3,A19;
          end;
          then
A24:      ComplRelStr G1 in fin_RelStr_sp by A2,A6;
          ComplRelStr G = union_of(ComplRelStr G1,ComplRelStr G2) by A5,A18
,Th18;
          hence thesis by A5,A24,A21,A22,NECKLA_2:def 5;
        end;
      end;
    end;
  end;
A25: for k being Nat holds P[k] from NAT_1:sch 4(A1);
  assume
A26: G in fin_RelStr_sp;
  then G is finite by NECKLA_2:4;
  then card the carrier of G is Nat;
  hence thesis by A26,A25;
end;

theorem Th33:
  for R be irreflexive symmetric RelStr st card (the carrier of R)
  = 2 & the carrier of R in FinSETS holds the RelStr of R in fin_RelStr_sp
proof
  let R be irreflexive symmetric RelStr;
  assume that
A1: card (the carrier of R) = 2 and
A2: the carrier of R in FinSETS;
  consider a,b being object such that
A3: the carrier of R = {a,b} and
A4: the InternalRel of R = {[a,b],[b,a]} or the InternalRel of R = {}
   by A1,Th6;
  set A = {a}, B = {b};
A5: A c= the carrier of R
  proof
    let x be object;
    assume x in A;
    then x = a by TARSKI:def 1;
    hence thesis by A3,TARSKI:def 2;
  end;
A6: B c= the carrier of R
  proof
    let x be object;
    assume x in B;
    then x = b by TARSKI:def 1;
    hence thesis by A3,TARSKI:def 2;
  end;
  then reconsider B as Subset of R;
  reconsider A as Subset of R by A5;
  set H1 = subrelstr A, H2 = subrelstr B;
  reconsider H2 as non empty strict irreflexive symmetric RelStr by
YELLOW_0:def 15;
A7: the carrier of H2 = B by YELLOW_0:def 15;
  then the InternalRel of H2 c= [:{b},{b}:];
  then the InternalRel of H2 c= {[b,b]} by ZFMISC_1:29;
  then
A8: the InternalRel of H2 = {} or the InternalRel of H2 = {[b,b]} by
ZFMISC_1:33;
A9: the InternalRel of H2 = {}
  proof
    b in B by TARSKI:def 1;
    then b in the carrier of H2 by YELLOW_0:def 15;
    then
A10: not [b,b] in the InternalRel of H2 by NECKLACE:def 5;
    assume not thesis;
    hence thesis by A8,A10,TARSKI:def 1;
  end;
  the carrier of H2 c= the carrier of R by A6,YELLOW_0:def 15;
  then the carrier of H2 in FinSETS by A2,CLASSES1:3,CLASSES2:def 2;
  then
A11: H2 in fin_RelStr_sp by A7,NECKLA_2:def 5;
  reconsider H1 as non empty strict irreflexive symmetric RelStr by
YELLOW_0:def 15;
A12: the carrier of H1 = A by YELLOW_0:def 15;
  then
A13: the carrier of R = (the carrier of H1) \/ (the carrier of H2) by A3,A7,
ENUMSET1:1;
  a <> b
  proof
    assume not thesis;
    then the carrier of R = {a} by A3,ENUMSET1:29;
    hence thesis by A1,CARD_1:30;
  end;
  then
A14: A misses B by ZFMISC_1:11;
  then
A15: (the carrier of H1) misses (the carrier of H2) by A7,YELLOW_0:def 15;
  the InternalRel of H1 c= [:{a},{a}:] by A12;
  then the InternalRel of H1 c= {[a,a]} by ZFMISC_1:29;
  then
A16: the InternalRel of H1 = {} or the InternalRel of H1 = {[a,a]} by
ZFMISC_1:33;
A17: the InternalRel of H1 = {}
  proof
    a in A by TARSKI:def 1;
    then a in the carrier of H1 by YELLOW_0:def 15;
    then
A18: not [a,a] in the InternalRel of H1 by NECKLACE:def 5;
    assume not thesis;
    hence thesis by A16,A18,TARSKI:def 1;
  end;
  the carrier of H1 c= the carrier of R by A5,YELLOW_0:def 15;
  then the carrier of H1 in FinSETS by A2,CLASSES1:3,CLASSES2:def 2;
  then
A19: H1 in fin_RelStr_sp by A12,NECKLA_2:def 5;
  per cases by A4;
  suppose
A20: the InternalRel of R = {[a,b],[b,a]};
    set S = sum_of(H1,H2);
    the InternalRel of S = (the InternalRel of H1) \/ (the InternalRel of
    H2) \/ [:A,B:] \/ [:B,A:] by A12,A7,NECKLA_2:def 3;
    then the InternalRel of S = {[a,b]} \/ [:{b},{a}:] by A17,A9,ZFMISC_1:29;
    then the InternalRel of S = {[a,b]} \/ {[b,a]} by ZFMISC_1:29;
    then
A21: the InternalRel of S = the InternalRel of R by A20,ENUMSET1:1;
    the carrier of S = the carrier of R by A13,NECKLA_2:def 3;
    hence thesis by A12,A19,A7,A11,A14,A21,NECKLA_2:def 5;
  end;
  suppose
A22: the InternalRel of R = {};
    set U = union_of(H1,H2);
    the InternalRel of U = (the InternalRel of H1) \/ (the InternalRel of
    H2 ) & the carrier of U = the carrier of R by A13,NECKLA_2:def 2;
    hence thesis by A19,A11,A15,A17,A9,A22,NECKLA_2:def 5;
  end;
end;

theorem
  for R be RelStr st R in fin_RelStr_sp holds R is symmetric
proof
  let X be RelStr;
  assume
A1: X in fin_RelStr_sp;
  per cases;
  suppose
A2: X is trivial;
    thus thesis
    proof
      per cases by A2,ZFMISC_1:131;
      suppose
A3:     the carrier of X is empty;
        let a,b be object;
        assume that
A4:     a in the carrier of X and
        b in the carrier of X and
        [a,b] in the InternalRel of X;
        thus thesis by A3,A4;
      end;
      suppose
        ex x being object st the carrier of X = {x};
        then consider x being object such that
A5:     the carrier of X = {x};
A6:     [:the carrier of X,the carrier of X:] = {[x,x]} by A5,ZFMISC_1:29;
        thus thesis
        proof
          per cases by A6,ZFMISC_1:33;
          suppose
A7:         the InternalRel of X = {};
            let a,b be object;
            assume that
            a in the carrier of X and
            b in the carrier of X and
A8:         [a,b] in the InternalRel of X;
            thus thesis by A7,A8;
          end;
          suppose
A9:         the InternalRel of X = {[x,x]};
            let a,b be object;
            assume that
            a in the carrier of X and
            b in the carrier of X and
A10:        [a,b] in the InternalRel of X;
A11:        [a,b] = [x,x] by A9,A10,TARSKI:def 1;
            then a = x by XTUPLE_0:1;
            hence thesis by A10,A11,XTUPLE_0:1;
          end;
        end;
      end;
    end;
  end;
  suppose
A12: not X is trivial;
    defpred P[Nat] means for X be non empty RelStr st not X is trivial & X in
    fin_RelStr_sp holds card (the carrier of X) c= $1 implies X is symmetric;
A13: ex R be strict RelStr st X = R & the carrier of R in FinSETS by A1,
NECKLA_2:def 4;
    reconsider X as non empty RelStr by A1,NECKLA_2:4;
A14: card the carrier of X is Nat by A13;
A15: for k being Nat st P[k] holds P[k+1]
    proof
      let k be Nat such that
A16:  P[k];
      reconsider k1=k as Element of NAT by ORDINAL1:def 12;
      let Y be non empty RelStr such that
A17:  not Y is trivial and
A18:  Y in fin_RelStr_sp;
      consider H1,H2 be strict RelStr such that
A19:  the carrier of H1 misses the carrier of H2 and
A20:  H1 in fin_RelStr_sp and
A21:  H2 in fin_RelStr_sp and
A22:  Y = union_of(H1,H2) or Y = sum_of(H1,H2) by A17,A18,NECKLA_2:6;
      ex R be strict RelStr st Y = R & the carrier of R in FinSETS by A18,
NECKLA_2:def 4;
      then reconsider cY = the carrier of Y as finite set;
      assume card (the carrier of Y) c= k+1;
      then Segm card cY c= Segm card (k1+1);
      then card cY <= card (k1+1) by NAT_1:39;
      then
A23:  card cY <= k+1;
      set cH1 = the carrier of H1, cH2 = the carrier of H2;
A24:  card cY = card ((cH1) \/ cH2) by A22,NECKLA_2:def 2,def 3;
      ex R2 be strict RelStr st H2 = R2 & the carrier of R2 in FinSETS by A21,
NECKLA_2:def 4;
      then reconsider cH2 as finite set;
      ex R1 be strict RelStr st H1 = R1 & the carrier of R1 in FinSETS by A20,
NECKLA_2:def 4;
      then reconsider cH1 as finite set;
A25:  card cY = card cH1 + card cH2 by A19,A24,CARD_2:40;
      H1 is non empty by A20,NECKLA_2:4;
      then
A26:  card cH1 >= 1 by NAT_1:14;
      H2 is non empty by A21,NECKLA_2:4;
      then
A27:  card cH2 >= 1 by NAT_1:14;
      per cases by A25,A23,A26,A27,NAT_1:8,XXREAL_0:1;
      suppose
        card cY <= k;
        then card cY <= card k1;
        then Segm card cY c= Segm card k by NAT_1:39;
        then card (the carrier of Y) c= k1;
        hence thesis by A16,A17,A18;
      end;
      suppose
A28:    card cY = k+1 & k = 0;
        set x = the set;
        card cY = card {x} by A28,CARD_1:30;
        then cY,{x} are_equipotent by CARD_1:5;
        then ex y being object st cY = {y} by CARD_1:28;
        hence thesis by A17;
      end;
      suppose
A29:    card cH1 + card cH2 = k+1 & k > 0 & card cH1 = 1 & card cH2 = 1;
        then ex x be object st cH1 = {x} by CARD_2:42;
        then the InternalRel of H1 is_symmetric_in cH1 by Th5;
        then reconsider H1 as symmetric RelStr by NECKLACE:def 3;
        ex y be object st cH2 = {y} by A29,CARD_2:42;
        then the InternalRel of H2 is_symmetric_in cH2 by Th5;
        then reconsider H2 as symmetric RelStr by NECKLACE:def 3;
        union_of(H1,H2) is symmetric;
        hence thesis by A22;
      end;
      suppose
A30:    card cH1 + card cH2 = k+1 & k > 0 & card cH1 = 1 & card cH2 > 1;
        then ex x be object st cH1 = {x} by CARD_2:42;
        then the InternalRel of H1 is_symmetric_in cH1 by Th5;
        then reconsider H1 as symmetric RelStr by NECKLACE:def 3;
        card cH2 is non trivial by A30,NAT_2:28;
        then card cH2 >= 2 by NAT_2:29;
        then H2 is non empty non trivial by NAT_D:60;
        then reconsider H2 as symmetric RelStr by A16,A21,A30;
        union_of(H1,H2) is symmetric;
        hence thesis by A22;
      end;
      suppose
A31:    card cH1 + card cH2 = k+1 & k > 0 & card cH1 > 1 & card cH2 = 1;
        then ex x be object st cH2 = {x} by CARD_2:42;
        then the InternalRel of H2 is_symmetric_in cH2 by Th5;
        then reconsider H2 as symmetric RelStr by NECKLACE:def 3;
        card cH1 is non trivial by A31,NAT_2:28;
        then card cH1 >= 2 by NAT_2:29;
        then H1 is non empty non trivial by NAT_D:60;
        then reconsider H1 as symmetric RelStr by A16,A20,A31;
        union_of(H1,H2) is symmetric;
        hence thesis by A22;
      end;
      suppose
A32:    card cH1 + card cH2 = k+1 & k > 0 & card cH1 > 1 & card cH2 > 1;
        then card cH2 is non trivial by NAT_2:28;
        then card cH2 >= 2 by NAT_2:29;
        then
A33:    H2 is non empty non trivial by NAT_D:60;
        card cH2 < k+1
        proof
          assume not thesis;
          then card cH1 + card cH2 >= (k+1)+1 by A26,XREAL_1:7;
          hence thesis by A32,NAT_1:13;
        end;
        then card cH2 <= k by NAT_1:13;
        then card cH2 <= card k1;
        then Segm card cH2 c= Segm card k by NAT_1:39;
        then card cH2 c= k1;
        then reconsider H2 as symmetric RelStr by A16,A21,A33;
        card cH1 is non trivial by A32,NAT_2:28;
        then card cH1 >= 2 by NAT_2:29;
        then
A34:    H1 is non empty non trivial by NAT_D:60;
        card cH1 < k+1
        proof
          assume not thesis;
          then card cH1 + card cH2 >= (k+1)+1 by A27,XREAL_1:7;
          hence thesis by A32,NAT_1:13;
        end;
        then card cH1 <= k by NAT_1:13;
        then card cH1 <= card k1;
        then Segm card cH1 c= Segm card k by NAT_1:39;
        then card cH1 c= k1;
        then reconsider H1 as symmetric RelStr by A16,A20,A34;
        union_of(H1,H2) is symmetric;
        hence thesis by A22;
      end;
    end;
A35: P[0];
    for k being Nat holds P[k] from NAT_1:sch 2(A35,A15);
    hence thesis by A1,A12,A14;
  end;
end;

theorem Th35:
  for G being RelStr, H1,H2 being non empty RelStr, x being
Element of H1, y being Element of H2 st G = union_of(H1,H2) & the carrier of H1
  misses the carrier of H2 holds not [x,y] in the InternalRel of G
proof
  let G be RelStr;
  let H1,H2 be non empty RelStr;
  let x be Element of H1;
  let y be Element of H2;
  assume that
A1: G = union_of(H1,H2) and
A2: (the carrier of H1) misses (the carrier of H2);
  assume not thesis;
  then
A3: [x,y] in (the InternalRel of H1) \/ the InternalRel of H2 by A1,
NECKLA_2:def 2;
  per cases by A3,XBOOLE_0:def 3;
  suppose
    [x,y] in (the InternalRel of H1);
    then y in the carrier of H1 by ZFMISC_1:87;
    then y in (the carrier of H1) /\ the carrier of H2 by XBOOLE_0:def 4;
    hence thesis by A2;
  end;
  suppose
    [x,y] in (the InternalRel of H2);
    then x in the carrier of H2 by ZFMISC_1:87;
    then x in (the carrier of H1) /\ the carrier of H2 by XBOOLE_0:def 4;
    hence thesis by A2;
  end;
end;

theorem
  for G being RelStr, H1,H2 being non empty RelStr, x being Element of
  H1, y being Element of H2 st G = sum_of(H1,H2) holds not [x,y] in the
  InternalRel of ComplRelStr G
proof
  let G being RelStr,H1,H2 being non empty RelStr, x being Element of H1, y
  being Element of H2;
  set cH1 = the carrier of H1, cH2 = the carrier of H2, IH1 = the InternalRel
  of H1, IH2 = the InternalRel of H2;
  [x,y] in [:cH1,cH2:] \/ [:cH2,cH1:] by XBOOLE_0:def 3;
  then [x,y] in IH2 \/ ([:cH1,cH2:] \/ [:cH2,cH1:]) by XBOOLE_0:def 3;
  then [x,y] in IH1 \/ (IH2 \/ ([:cH1,cH2:] \/ [:cH2,cH1:])) by XBOOLE_0:def 3;
  then [x,y] in IH1 \/ (IH2 \/ [:cH1,cH2:] \/ [:cH2,cH1:]) by XBOOLE_1:4;
  then
A1: [x,y] in IH1 \/ IH2 \/ [:cH1,cH2:] \/ [:cH2,cH1:] by XBOOLE_1:113;
  assume G = sum_of(H1,H2);
  then
A2: [x,y] in the InternalRel of G by A1,NECKLA_2:def 3;
  not [x,y] in the InternalRel of ComplRelStr G
  proof
    assume not thesis;
    then [x,y] in (the InternalRel of G) /\ the InternalRel of ComplRelStr G
    by A2,XBOOLE_0:def 4;
    then (the InternalRel of G) meets the InternalRel of ComplRelStr G;
    hence contradiction by Th12;
  end;
  hence thesis;
end;

theorem Th37:
  for G being non empty symmetric RelStr, x being Element of G, R1
  ,R2 being non empty RelStr st the carrier of R1 misses the carrier of R2 &
subrelstr ([#]G \ {x}) = union_of(R1,R2) & G is path-connected holds ex b being
  Element of R1 st [b,x] in the InternalRel of G
proof
  let G be non empty symmetric RelStr;
  let x be Element of G;
  let R1,R2 be non empty RelStr;
  assume that
A1: the carrier of R1 misses the carrier of R2 and
A2: subrelstr ([#]G \ {x}) = union_of(R1,R2) and
A3: G is path-connected;
  set R = subrelstr ([#]G \ {x}), A = the carrier of R;
  the carrier of R1 c= (the carrier of R1) \/ the carrier of R2 by XBOOLE_1:7;
  then
A4: the carrier of R1 c= the carrier of R by A2,NECKLA_2:def 2;
  set a = the Element of R1;
A5: A = [#]G \ {x} by YELLOW_0:def 15;
A6: x <> a
  proof
    assume not thesis;
    then x in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
    then x in (the carrier of G) \ {x} by A2,A5,NECKLA_2:def 2;
    then not x in {x} by XBOOLE_0:def 5;
    hence thesis by TARSKI:def 1;
  end;
  reconsider A as Subset of G by YELLOW_0:def 15;
A7: the carrier of R = A;
  then the carrier of R1 c= the carrier of G by A4,XBOOLE_1:1;
  then a in the carrier of G;
  then (the InternalRel of G) reduces x,a by A3,A6;
  then consider p being FinSequence such that
A8: len p > 0 and
A9: p.1 = x and
A10: p.len p = a and
A11: for i being Nat st i in dom p & i+1 in dom p holds [p.i,
  p.(i+1)] in (the InternalRel of G) by REWRITE1:11;
  defpred P[Nat] means p.$1 in the carrier of R1 & $1 in dom p & for k being
  Nat st k > $1 holds k in dom p implies p.k in the carrier of R1;
  P[len p] by A8,A10,CARD_1:27,FINSEQ_3:25,FINSEQ_5:6;
  then
A12: ex k being Nat st P[k];
  ex n0 being Nat st P[n0] & for n being Nat st P[n] holds n >= n0 from
  NAT_1:sch 5(A12);
  then consider n0 being Element of NAT such that
A13: P[n0] and
A14: for n being Nat st P[n] holds n >= n0;
  n0 <> 0
  proof
    assume not thesis;
    then 0 in Seg (len p) by A13,FINSEQ_1:def 3;
    hence contradiction by FINSEQ_1:1;
  end;
  then consider k0 being Nat such that
A15: n0 = k0 + 1 by NAT_1:6;
A16: n0 <> 1
  proof
    assume not thesis;
    then not x in {x} by A5,A4,A9,A13,XBOOLE_0:def 5;
    hence contradiction by TARSKI:def 1;
  end;
A17: k0 >= 1
  proof
    assume not thesis;
    then k0 = 0 by NAT_1:25;
    hence contradiction by A15,A16;
  end;
  n0 in Seg (len p) by A13,FINSEQ_1:def 3;
  then
A18: n0 <= len p by FINSEQ_1:1;
A19: k0 < n0 by A15,NAT_1:13;
A20: for k being Nat st k > k0 holds k in dom p implies p.k in the carrier
  of R1
  proof
    assume not thesis;
    then consider k being Nat such that
A21: k > k0 and
A22: k in dom p and
A23: not p.k in the carrier of R1;
    k > n0
    proof
      per cases by XXREAL_0:1;
      suppose
        k < n0;
        hence thesis by A15,A21,NAT_1:13;
      end;
      suppose
        n0 < k;
        hence thesis;
      end;
      suppose
        n0 = k;
        hence thesis by A13,A23;
      end;
    end;
    hence contradiction by A13,A22,A23;
  end;
A24: the carrier of G = (the carrier of R) \/ {x}
  proof
    thus the carrier of G c= (the carrier of R) \/ {x}
    proof
      let a be object;
      assume
A25:  a in the carrier of G;
      per cases;
      suppose
        a = x;
        then a in {x} by TARSKI:def 1;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        a <> x;
        then not a in {x} by TARSKI:def 1;
        then a in A by A5,A25,XBOOLE_0:def 5;
        hence thesis by XBOOLE_0:def 3;
      end;
    end;
    let a be object;
    assume
A26: a in (the carrier of R) \/ {x};
    per cases by A26,XBOOLE_0:def 3;
    suppose
      a in the carrier of R;
      hence thesis by A5;
    end;
    suppose
      a in {x};
      hence thesis;
    end;
  end;
  k0 <= n0 by A15,XREAL_1:29;
  then k0 <= len p by A18,XXREAL_0:2;
  then
A27: k0 in dom p by A17,FINSEQ_3:25;
  then
A28: [p.k0,p.(k0+1)] in the InternalRel of G by A11,A13,A15;
  then
A29: p.k0 in the carrier of G by ZFMISC_1:87;
  thus thesis
  proof
    per cases by A29,A24,XBOOLE_0:def 3;
    suppose
A30:  p.k0 in the carrier of R;
      set u = p.k0, v = p.n0;
      [u,v] in [:the carrier of R,the carrier of R:] by A4,A13,A30,ZFMISC_1:87;
      then
A31:  [u,v] in (the InternalRel of G)|_2 the carrier of R by A15,A28,
XBOOLE_0:def 4;
      p.k0 in (the carrier of R1) \/ the carrier of R2 by A2,A30,NECKLA_2:def 2
;
      then p.k0 in the carrier of R1 or p.k0 in the carrier of R2 by
XBOOLE_0:def 3;
      then reconsider u as Element of R2 by A14,A27,A19,A20;
      reconsider v as Element of R1 by A13;
      not [u,v] in the InternalRel of R
      proof
        u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A32:    u in the carrier of R by A2,NECKLA_2:def 2;
A33:    v in the carrier of R1 & the InternalRel of R is_symmetric_in the
        carrier of R by NECKLACE:def 3;
        assume not thesis;
        then [v,u] in the InternalRel of R by A4,A32,A33;
        hence thesis by A1,A2,Th35;
      end;
      hence thesis by A31,YELLOW_0:def 14;
    end;
    suppose
A34:  p.k0 in {x};
      set b = p.n0;
      reconsider b as Element of R1 by A13;
A35:  b in the carrier of R & (the InternalRel of G) is_symmetric_in the
      carrier of G by A4,NECKLACE:def 3;
      p.k0 = x by A34,TARSKI:def 1;
      then [b,x] in (the InternalRel of G) by A7,A15,A28,A35;
      hence thesis;
    end;
  end;
end;

theorem Th38:
  for G being non empty symmetric irreflexive RelStr, a,b,c,d
  being Element of G, Z being Subset of G st Z = {a,b,c,d} & a,b,c,d
  are_mutually_distinct & [a,b] in the InternalRel of G & [b,c] in the
InternalRel of G & [c,d] in the InternalRel of G & not [a,c] in the InternalRel
  of G & not [a,d] in the InternalRel of G & not [b,d] in the InternalRel of G
  holds subrelstr Z embeds Necklace 4
proof
  let G be non empty symmetric irreflexive symmetric RelStr;
  let a,b,c,d be Element of G;
  let Z be Subset of G;
  assume that
A1: Z = {a,b,c,d} and
A2: a,b,c,d are_mutually_distinct and
A3: [a,b] in the InternalRel of G and
A4: [b,c] in the InternalRel of G and
A5: [c,d] in the InternalRel of G and
A6: not [a,c] in the InternalRel of G and
A7: not [a,d] in the InternalRel of G and
A8: not [b,d] in the InternalRel of G;
  set g = (0,1) --> (a,b), h = (2,3) --> (c,d), f = g +* h;
A9: rng h = {c,d} by FUNCT_4:64;
A10: a <> b by A2,ZFMISC_1:def 6;
A11: rng (0 .--> a) misses rng (1 .--> b)
  proof
    assume rng (0 .--> a) meets rng (1 .--> b);
    then consider x being object such that
A12: x in rng (0 .--> a) and
A13: x in rng (1 .--> b) by XBOOLE_0:3;
    rng (0 .--> a) = {a} by FUNCOP_1:8;
    then rng (1 .--> b) = {b} & x = a by A12,FUNCOP_1:8,TARSKI:def 1;
    hence contradiction by A10,A13,TARSKI:def 1;
  end;
  set H = subrelstr Z, N4 = Necklace 4, IH = the InternalRel of H, cH = the
carrier of H, IG = the InternalRel of G, X = {[a,a],[a,b],[b,a],[b,b],[a,c],[a,
  d],[b,c],[b,d]}, Y = {[c,a],[c,b],[d,a],[d,b],[c,c],[c,d],[d,c],[d,d]};
A14: the carrier of H is non empty by A1,YELLOW_0:def 15;
A15: h = (2 .--> c) +* (3 .--> d) by FUNCT_4:def 4;
A16: c <> d by A2,ZFMISC_1:def 6;
  rng (2 .--> c) misses rng (3 .--> d)
  proof
    assume rng (2 .--> c) meets rng (3 .--> d);
    then consider x being object such that
A17: x in rng (2 .--> c) and
A18: x in rng (3 .--> d) by XBOOLE_0:3;
    rng (2 .--> c) = {c} by FUNCOP_1:8;
    then rng (3 .--> d) = {d} & x = c by A17,FUNCOP_1:8,TARSKI:def 1;
    hence contradiction by A16,A18,TARSKI:def 1;
  end;
  then
A19: h is one-to-one by A15,FUNCT_4:92;
A20: rng g = {a,b} by FUNCT_4:64;
A21: rng g misses rng h
  proof
    assume not thesis;
    then consider x being object such that
A22: x in rng g and
A23: x in rng h by XBOOLE_0:3;
A24: x = c or x = d by A9,A23,TARSKI:def 2;
    x = a or x = b by A20,A22,TARSKI:def 2;
    hence contradiction by A2,A24,ZFMISC_1:def 6;
  end;
  dom f = dom g \/ dom h by FUNCT_4:def 1
    .= {0,1} \/ dom h by FUNCT_4:62
    .= {0,1} \/ {2,3} by FUNCT_4:62
    .= {0,1,2,3} by ENUMSET1:5;
  then
A25: dom f = the carrier of N4 by NECKLACE:1,20;
A26: dom g misses dom h
  proof
    assume not thesis;
    then consider x being object such that
A27: x in dom g and
A28: x in dom h by XBOOLE_0:3;
    x=0 or x=1 by A27,TARSKI:def 2;
    hence contradiction by A28,TARSKI:def 2;
  end;
  then rng f = rng g \/ rng h by NECKLACE:6;
  then rng f = {a,b,c,d} by A20,A9,ENUMSET1:5;
  then
A29: rng f = the carrier of H by A1,YELLOW_0:def 15;
  then reconsider f as Function of N4,H by A25,FUNCT_2:def 1,RELSET_1:4;
  g = (0 .--> a) +* (1 .-->b) by FUNCT_4:def 4;
  then
A30: g is one-to-one by A11,FUNCT_4:92;
  then
A31: f is one-to-one by A19,A21,FUNCT_4:92;
A32: the InternalRel of H = {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
  proof
    thus the InternalRel of H c= {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]}
    proof
      let x be object;
A33:  the carrier of H = Z by YELLOW_0:def 15;
      assume
A34:  x in IH;
      then
A35:  x in IG |_2 cH by YELLOW_0:def 14;
      then
A36:  x in IG by XBOOLE_0:def 4;
      x in [:cH,cH:] by A34;
      then
A37:  x in X \/ Y by A1,A33,Th3;
      per cases by A37,XBOOLE_0:def 3;
      suppose
A38:    x in X;
        thus thesis
        proof
          per cases by A38,ENUMSET1:def 6;
          suppose
A39:        x = [a,a];
            not [a,a] in IG by NECKLACE:def 5;
            hence thesis by A35,A39,XBOOLE_0:def 4;
          end;
          suppose
            x =[a,b];
            hence thesis by ENUMSET1:def 4;
          end;
          suppose
            x =[b,a];
            hence thesis by ENUMSET1:def 4;
          end;
          suppose
A40:        x =[b,b];
            not [b,b] in IG by NECKLACE:def 5;
            hence thesis by A35,A40,XBOOLE_0:def 4;
          end;
          suppose
            x = [a,c];
            hence thesis by A6,A35,XBOOLE_0:def 4;
          end;
          suppose
            x = [a,d];
            hence thesis by A7,A35,XBOOLE_0:def 4;
          end;
          suppose
            x = [b,c];
            hence thesis by ENUMSET1:def 4;
          end;
          suppose
            x =[b,d];
            hence thesis by A8,A35,XBOOLE_0:def 4;
          end;
        end;
      end;
      suppose
A41:    x in Y;
A42:    IG is_symmetric_in the carrier of G by NECKLACE:def 3;
        thus thesis
        proof
          per cases by A41,ENUMSET1:def 6;
          suppose
            x = [c,a];
            hence thesis by A6,A36,A42;
          end;
          suppose
            x = [c,b];
            hence thesis by ENUMSET1:def 4;
          end;
          suppose
            x = [d,a];
            hence thesis by A7,A36,A42;
          end;
          suppose
            x = [d,b];
            hence thesis by A8,A36,A42;
          end;
          suppose
A43:        x = [c,c];
            not [c,c] in IG by NECKLACE:def 5;
            hence thesis by A35,A43,XBOOLE_0:def 4;
          end;
          suppose
            x = [c,d];
            hence thesis by ENUMSET1:def 4;
          end;
          suppose
            x = [d,c];
            hence thesis by ENUMSET1:def 4;
          end;
          suppose
A44:        x = [d,d];
            not [d,d] in IG by NECKLACE:def 5;
            hence thesis by A35,A44,XBOOLE_0:def 4;
          end;
        end;
      end;
    end;
    let x be object;
    assume
A45: x in {[a,b],[b,a],[b,c],[c,b],[c,d],[d,c]};
    per cases by A45,ENUMSET1:def 4;
    suppose
A46:  x = [a,b];
      b in Z by A1,ENUMSET1:def 2;
      then
A47:  b in cH by YELLOW_0:def 15;
      a in Z by A1,ENUMSET1:def 2;
      then a in cH by YELLOW_0:def 15;
      then [a,b] in [:cH,cH:] by A47,ZFMISC_1:87;
      then x in IG |_2 cH by A3,A46,XBOOLE_0:def 4;
      hence thesis by YELLOW_0:def 14;
    end;
    suppose
A48:  x = [b,a];
      IG is_symmetric_in the carrier of G by NECKLACE:def 3;
      then
A49:  [b,a] in IG by A3;
      a in Z by A1,ENUMSET1:def 2;
      then
A50:  a in cH by YELLOW_0:def 15;
      b in Z by A1,ENUMSET1:def 2;
      then b in cH by YELLOW_0:def 15;
      then [b,a] in [:cH,cH:] by A50,ZFMISC_1:87;
      then x in IG |_2 cH by A48,A49,XBOOLE_0:def 4;
      hence thesis by YELLOW_0:def 14;
    end;
    suppose
A51:  x = [b,c];
      c in Z by A1,ENUMSET1:def 2;
      then
A52:  c in cH by YELLOW_0:def 15;
      b in Z by A1,ENUMSET1:def 2;
      then b in cH by YELLOW_0:def 15;
      then [b,c] in [:cH,cH:] by A52,ZFMISC_1:87;
      then x in IG |_2 cH by A4,A51,XBOOLE_0:def 4;
      hence thesis by YELLOW_0:def 14;
    end;
    suppose
A53:  x = [c,b];
      IG is_symmetric_in the carrier of G by NECKLACE:def 3;
      then
A54:  [c,b] in IG by A4;
      c in Z by A1,ENUMSET1:def 2;
      then
A55:  c in cH by YELLOW_0:def 15;
      b in Z by A1,ENUMSET1:def 2;
      then b in cH by YELLOW_0:def 15;
      then [c,b] in [:cH,cH:] by A55,ZFMISC_1:87;
      then x in IG |_2 cH by A53,A54,XBOOLE_0:def 4;
      hence thesis by YELLOW_0:def 14;
    end;
    suppose
A56:  x = [c,d];
      d in Z by A1,ENUMSET1:def 2;
      then
A57:  d in cH by YELLOW_0:def 15;
      c in Z by A1,ENUMSET1:def 2;
      then c in cH by YELLOW_0:def 15;
      then [c,d] in [:cH,cH:] by A57,ZFMISC_1:87;
      then x in IG |_2 cH by A5,A56,XBOOLE_0:def 4;
      hence thesis by YELLOW_0:def 14;
    end;
    suppose
A58:  x = [d,c];
      IG is_symmetric_in the carrier of G by NECKLACE:def 3;
      then
A59:  [d,c] in IG by A5;
      d in Z by A1,ENUMSET1:def 2;
      then
A60:  d in cH by YELLOW_0:def 15;
      c in Z by A1,ENUMSET1:def 2;
      then c in cH by YELLOW_0:def 15;
      then [d,c] in [:cH,cH:] by A60,ZFMISC_1:87;
      then x in IG |_2 cH by A58,A59,XBOOLE_0:def 4;
      hence thesis by YELLOW_0:def 14;
    end;
  end;
  for x,y being Element of N4 holds [x,y] in the InternalRel of N4 iff [
  f.x,f.y] in the InternalRel of H
  proof
    let x,y being Element of N4;
    thus [x,y] in the InternalRel of N4 implies [f.x,f.y] in the InternalRel
    of H
    proof
      assume
A61:  [x,y] in the InternalRel of N4;
      per cases by A61,ENUMSET1:def 4,NECKLA_2:2;
      suppose
A62:    [x,y] = [0,1];
        then
A63:    y = 1 by XTUPLE_0:1;
        then y in {0,1} by TARSKI:def 2;
        then y in dom g by FUNCT_4:62;
        then
A64:    f.y = g.1 by A26,A63,FUNCT_4:16
          .= b by FUNCT_4:63;
A65:    x = 0 by A62,XTUPLE_0:1;
        then x in {0,1} by TARSKI:def 2;
        then x in dom g by FUNCT_4:62;
        then f.x = g.0 by A26,A65,FUNCT_4:16
          .= a by FUNCT_4:63;
        hence thesis by A32,A64,ENUMSET1:def 4;
      end;
      suppose
A66:    [x,y] = [1,0];
        then
A67:    y = 0 by XTUPLE_0:1;
        then y in {0,1} by TARSKI:def 2;
        then y in dom g by FUNCT_4:62;
        then
A68:    f.y = g.0 by A26,A67,FUNCT_4:16
          .= a by FUNCT_4:63;
A69:    x = 1 by A66,XTUPLE_0:1;
        then x in {0,1} by TARSKI:def 2;
        then x in dom g by FUNCT_4:62;
        then f.x = g.1 by A26,A69,FUNCT_4:16
          .= b by FUNCT_4:63;
        hence thesis by A32,A68,ENUMSET1:def 4;
      end;
      suppose
A70:    [x,y] = [1,2];
        then
A71:    x = 1 by XTUPLE_0:1;
        then x in {0,1} by TARSKI:def 2;
        then x in dom g by FUNCT_4:62;
        then
A72:    f.x = g.1 by A26,A71,FUNCT_4:16
          .= b by FUNCT_4:63;
A73:    y = 2 by A70,XTUPLE_0:1;
        then y in {2,3} by TARSKI:def 2;
        then
A74:    y in dom h by FUNCT_4:62;
        g +* h = h +* g by A26,FUNCT_4:35;
        then f.y = h.2 by A26,A73,A74,FUNCT_4:16
          .= c by FUNCT_4:63;
        hence thesis by A32,A72,ENUMSET1:def 4;
      end;
      suppose
A75:    [x,y] = [2,1];
        then
A76:    y = 1 by XTUPLE_0:1;
        then y in {0,1} by TARSKI:def 2;
        then y in dom g by FUNCT_4:62;
        then
A77:    f.y = g.1 by A26,A76,FUNCT_4:16
          .= b by FUNCT_4:63;
A78:    x = 2 by A75,XTUPLE_0:1;
        then x in {2,3} by TARSKI:def 2;
        then
A79:    x in dom h by FUNCT_4:62;
        g +* h = h +* g by A26,FUNCT_4:35;
        then f.x = h.2 by A26,A78,A79,FUNCT_4:16
          .= c by FUNCT_4:63;
        hence thesis by A32,A77,ENUMSET1:def 4;
      end;
      suppose
A80:    [x,y] = [2,3];
A81:    g +* h = h +* g by A26,FUNCT_4:35;
A82:    y = 3 by A80,XTUPLE_0:1;
        then y in {2,3} by TARSKI:def 2;
        then y in dom h by FUNCT_4:62;
        then
A83:    f.y = h.3 by A26,A82,A81,FUNCT_4:16
          .= d by FUNCT_4:63;
A84:    x = 2 by A80,XTUPLE_0:1;
        then x in {2,3} by TARSKI:def 2;
        then x in dom h by FUNCT_4:62;
        then f.x = h.2 by A26,A84,A81,FUNCT_4:16
          .= c by FUNCT_4:63;
        hence thesis by A32,A83,ENUMSET1:def 4;
      end;
      suppose
A85:    [x,y] = [3,2];
A86:    g +* h = h +* g by A26,FUNCT_4:35;
A87:    y = 2 by A85,XTUPLE_0:1;
        then y in {3,2} by TARSKI:def 2;
        then y in dom h by FUNCT_4:62;
        then
A88:    f.y = h.2 by A26,A87,A86,FUNCT_4:16
          .= c by FUNCT_4:63;
A89:    x = 3 by A85,XTUPLE_0:1;
        then x in {3,2} by TARSKI:def 2;
        then x in dom h by FUNCT_4:62;
        then f.x = h.3 by A26,A89,A86,FUNCT_4:16
          .= d by FUNCT_4:63;
        hence thesis by A32,A88,ENUMSET1:def 4;
      end;
    end;
    thus [f.x,f.y] in the InternalRel of H implies [x,y] in the InternalRel of
    N4
    proof
      reconsider F=f" as Function of the carrier of H,the carrier of N4 by A29
,A31,FUNCT_2:25;
A90:  dom g = {0,1} by FUNCT_4:62;
A91:  rng g = {a,b} by FUNCT_4:64;
      then reconsider g as Function of {0,1},{a,b} by A90,RELSET_1:4;
      reconsider G = g" as Function of {a,b},{0,1} by A20,A30,FUNCT_2:25;
A92:  dom h = {2,3} by FUNCT_4:62;
A93:  rng h = {c,d} by FUNCT_4:64;
      then reconsider h as Function of {2,3},{c,d} by A92,RELSET_1:4;
      reconsider Hh = h" as Function of {c,d},{2,3} by A9,A19,FUNCT_2:25;
A94:  dom Hh = {c,d} by A19,A93,FUNCT_1:33;
A95:  Hh = (c,d) --> (2,3) by A16,NECKLACE:10;
A96:  F = G +* Hh by A26,A30,A19,A21,NECKLACE:7;
A97:  G = (a,b) --> (0,1) by A10,NECKLACE:10;
A98:  dom G = {a,b} by A30,A91,FUNCT_1:33;
      then G +* Hh = Hh +* G by A20,A9,A21,A94,FUNCT_4:35;
      then
A99:  F = Hh +* G by A26,A30,A19,A21,NECKLACE:7;
      assume
A100: [f.x,f.y] in the InternalRel of H;
      per cases by A32,A100,ENUMSET1:def 4;
      suppose
A101:   [f.x,f.y] = [a,b];
        then
A102:   f.x = a by XTUPLE_0:1;
        then f.x in {a,b} by TARSKI:def 2;
        then F.(f.x) = G.a by A20,A9,A21,A98,A94,A96,A102,FUNCT_4:16
          .= 0 by A10,A97,FUNCT_4:63;
        then
A103:   x = 0 by A14,A31,FUNCT_2:26;
A104:   f.y = b by A101,XTUPLE_0:1;
        then f.y in dom G by A98,TARSKI:def 2;
        then
A105:   F.(f.y) = G.b by A20,A9,A21,A98,A94,A96,A104,FUNCT_4:16
          .= 1 by A97,FUNCT_4:63;
        F.(f.y) = y by A14,A31,FUNCT_2:26;
        hence thesis by A103,A105,ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
A106:   [f.x,f.y] = [b,a];
        then
A107:   f.y = a by XTUPLE_0:1;
        then f.y in {a,b} by TARSKI:def 2;
        then F.(f.y) = G.a by A20,A9,A21,A98,A94,A96,A107,FUNCT_4:16
          .= 0 by A10,A97,FUNCT_4:63;
        then
A108:   y = 0 by A14,A31,FUNCT_2:26;
A109:   f.x = b by A106,XTUPLE_0:1;
        then f.x in dom G by A98,TARSKI:def 2;
        then
A110:   F.(f.x) = G.b by A20,A9,A21,A98,A94,A96,A109,FUNCT_4:16
          .= 1 by A97,FUNCT_4:63;
        F.(f.x) = x by A14,A31,FUNCT_2:26;
        hence thesis by A108,A110,ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
A111:   [f.x,f.y] = [b,c];
        then
A112:   f.x = b by XTUPLE_0:1;
        then f.x in dom G by A98,TARSKI:def 2;
        then F.(f.x) = G.b by A20,A9,A21,A98,A94,A96,A112,FUNCT_4:16
          .= 1 by A97,FUNCT_4:63;
        then
A113:   x = 1 by A14,A31,FUNCT_2:26;
A114:   f.y = c by A111,XTUPLE_0:1;
        then f.y in dom Hh by A94,TARSKI:def 2;
        then
A115:   F.(f.y) = Hh.c by A20,A9,A21,A98,A94,A99,A114,FUNCT_4:16
          .= 2 by A16,A95,FUNCT_4:63;
        F.(f.y) = y by A14,A31,FUNCT_2:26;
        hence thesis by A113,A115,ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
A116:   [f.x,f.y] = [c,b];
        then
A117:   f.y = b by XTUPLE_0:1;
        then f.y in dom G by A98,TARSKI:def 2;
        then F.(f.y) = G.b by A20,A9,A21,A98,A94,A96,A117,FUNCT_4:16
          .= 1 by A97,FUNCT_4:63;
        then
A118:   y = 1 by A14,A31,FUNCT_2:26;
A119:   f.x = c by A116,XTUPLE_0:1;
        then f.x in dom Hh by A94,TARSKI:def 2;
        then
A120:   F.(f.x) = Hh.c by A20,A9,A21,A98,A94,A99,A119,FUNCT_4:16
          .= 2 by A16,A95,FUNCT_4:63;
        F.(f.x) = x by A14,A31,FUNCT_2:26;
        hence thesis by A118,A120,ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
A121:   [f.x,f.y] = [c,d];
        then
A122:   f.x = c by XTUPLE_0:1;
        then f.x in {c,d} by TARSKI:def 2;
        then F.(f.x) = Hh.c by A20,A9,A21,A98,A94,A99,A122,FUNCT_4:16
          .= 2 by A16,A95,FUNCT_4:63;
        then
A123:   x = 2 by A14,A31,FUNCT_2:26;
A124:   f.y = d by A121,XTUPLE_0:1;
        then f.y in dom Hh by A94,TARSKI:def 2;
        then
A125:   F.(f.y) = Hh.d by A20,A9,A21,A98,A94,A99,A124,FUNCT_4:16
          .= 3 by A95,FUNCT_4:63;
        F.(f.y) = y by A14,A31,FUNCT_2:26;
        hence thesis by A123,A125,ENUMSET1:def 4,NECKLA_2:2;
      end;
      suppose
A126:   [f.x,f.y] = [d,c];
        then
A127:   f.y = c by XTUPLE_0:1;
        then f.y in {c,d} by TARSKI:def 2;
        then F.(f.y) = Hh.c by A20,A9,A21,A98,A94,A99,A127,FUNCT_4:16
          .= 2 by A16,A95,FUNCT_4:63;
        then
A128:   y = 2 by A14,A31,FUNCT_2:26;
A129:   f.x = d by A126,XTUPLE_0:1;
        then f.x in dom Hh by A94,TARSKI:def 2;
        then
A130:   F.(f.x) = Hh.d by A20,A9,A21,A98,A94,A99,A129,FUNCT_4:16
          .= 3 by A95,FUNCT_4:63;
        F.(f.x) = x by A14,A31,FUNCT_2:26;
        hence thesis by A128,A130,ENUMSET1:def 4,NECKLA_2:2;
      end;
    end;
  end;
  hence thesis by A31;
end;

theorem Th39:
  for G being non empty irreflexive symmetric RelStr, x being
  Element of G, R1,R2 being non empty RelStr st the carrier of R1 misses the
carrier of R2 & subrelstr ([#]G \ {x}) = union_of(R1,R2) & G is non trivial & G
  is path-connected & ComplRelStr G is path-connected holds G embeds Necklace 4
proof
  let G be non empty irreflexive symmetric RelStr, x be Element of G, R1,R2 be
  non empty RelStr;
  assume that
A1: the carrier of R1 misses the carrier of R2 and
A2: subrelstr ([#]G \ {x}) = union_of(R1,R2) and
A3: G is non trivial and
A4: G is path-connected and
A5: ComplRelStr G is path-connected;
  consider a being Element of R1 such that
A6: [a,x] in the InternalRel of G by A1,A2,A4,Th37;
  set A = (the carrier of G) \ {x}, X = {x};
  reconsider A as Subset of G;
  set R = subrelstr A;
  reconsider R as non empty irreflexive symmetric RelStr by A3,YELLOW_0:def 15;
  R = subrelstr ([#]G \ {x}) & R = union_of(R2,R1) by A2,Th8;
  then consider b being Element of R2 such that
A7: [b,x] in the InternalRel of G by A1,A4,Th37;
  reconsider X1 = {y where y is Element of R1: [y,x] in (the InternalRel of G)
}, Y1 = {y where y is Element of R1: not [y,x] in the InternalRel of G}, X2 = {
  y where y is Element of R2: [y,x] in (the InternalRel of G)}, Y2 = {y where y
  is Element of R2: not [y,x] in the InternalRel of G} as set;
  reconsider X as Subset of G;
  set H = subrelstr X;
A8: X1 misses Y1
  proof
    assume not thesis;
    then consider a being object such that
A9: a in X1 & a in Y1 by XBOOLE_0:3;
    (ex y1 being Element of R1 st y1 = a & [y1,x] in the InternalRel of G
)& ex y2 being Element of R1 st y2 = a & not [y2,x] in the InternalRel of G by
A9;
    hence contradiction;
  end;
A10: a in X1 by A6;
A11: the carrier of R1 = X1 \/ Y1
  proof
    thus the carrier of R1 c= X1 \/ Y1
    proof
      let a be object;
      assume
A12:  a in the carrier of R1;
      per cases;
      suppose
        [a,x] in the InternalRel of G;
        then a in X1 by A12;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        not [a,x] in the InternalRel of G;
        then a in Y1 by A12;
        hence thesis by XBOOLE_0:def 3;
      end;
    end;
    let a be object such that
A13: a in X1 \/ Y1;
    per cases by A13,XBOOLE_0:def 3;
    suppose
      a in X1;
      then ex y being Element of R1 st a = y & [y,x] in (the InternalRel of G);
      hence thesis;
    end;
    suppose
      a in Y1;
      then ex y being Element of R1 st a = y & not [y,x] in the InternalRel of
      G;
      hence thesis;
    end;
  end;
A14: X2 misses Y2
  proof
    assume not thesis;
    then consider a being object such that
A15: a in X2 & a in Y2 by XBOOLE_0:3;
    (ex y1 being Element of R2 st y1 = a & [y1,x] in the InternalRel of G
)& ex y2 being Element of R2 st y2 = a & not [y2,x] in the InternalRel of G by
A15;
    hence contradiction;
  end;
A16: (the carrier of H) misses the carrier of R
  proof
    assume not thesis;
    then (the carrier of H) /\ (the carrier of R) <> {};
    then X /\ (the carrier of R) <> {} by YELLOW_0:def 15;
    then X /\ A <> {} by YELLOW_0:def 15;
    then consider a being object such that
A17: a in X /\ A by XBOOLE_0:def 1;
    a in X & a in A by A17,XBOOLE_0:def 4;
    hence contradiction by XBOOLE_0:def 5;
  end;
  reconsider H as non empty irreflexive symmetric RelStr by YELLOW_0:def 15;
A18: b in X2 by A7;
A19: the carrier of G = (the carrier of R) \/ {x}
  proof
    thus the carrier of G c= (the carrier of R) \/ {x}
    proof
      let a be object;
      assume
A20:  a in the carrier of G;
      per cases;
      suppose
        a = x;
        then a in {x} by TARSKI:def 1;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        a <> x;
        then not a in {x} by TARSKI:def 1;
        then a in (the carrier of G) \ {x} by A20,XBOOLE_0:def 5;
        then a in the carrier of R by YELLOW_0:def 15;
        hence thesis by XBOOLE_0:def 3;
      end;
    end;
    let a be object;
    assume
A21: a in (the carrier of R) \/ {x};
    per cases by A21,XBOOLE_0:def 3;
    suppose
      a in the carrier of R;
      then a in (the carrier of G) \ {x} by YELLOW_0:def 15;
      hence thesis;
    end;
    suppose
      a in {x};
      hence thesis;
    end;
  end;
A22: the carrier of R2 = X2 \/ Y2
  proof
    thus the carrier of R2 c= X2 \/ Y2
    proof
      let a be object;
      assume
A23:  a in the carrier of R2;
      per cases;
      suppose
        [a,x] in the InternalRel of G;
        then a in X2 by A23;
        hence thesis by XBOOLE_0:def 3;
      end;
      suppose
        not [a,x] in the InternalRel of G;
        then a in Y2 by A23;
        hence thesis by XBOOLE_0:def 3;
      end;
    end;
    let a be object such that
A24: a in X2 \/ Y2;
    per cases by A24,XBOOLE_0:def 3;
    suppose
      a in X2;
      then ex y being Element of R2 st a = y & [y,x] in (the InternalRel of G);
      hence thesis;
    end;
    suppose
      a in Y2;
      then ex y being Element of R2 st a = y & not [y,x] in the InternalRel of
      G;
      hence thesis;
    end;
  end;
A25: Y1 \/ Y2 is non empty
  proof
    assume
A26: not thesis;
    then
A27: Y2 is empty;
A28: Y1 is empty by A26;
A29: for a being Element of R holds [a,x] in the InternalRel of G
    proof
      let a be Element of R;
A30:  the carrier of R = (the carrier of R1) \/ the carrier of R2 by A2,
NECKLA_2:def 2;
      per cases by A30,XBOOLE_0:def 3;
      suppose
        a in the carrier of R1;
        then ex y being Element of R1 st a = y & [y,x] in the InternalRel of G
        by A11,A28;
        hence thesis;
      end;
      suppose
        a in the carrier of R2;
        then ex y being Element of R2 st a = y & [y,x] in the InternalRel of G
        by A22,A27;
        hence thesis;
      end;
    end;
    not ComplRelStr G is path-connected
    proof
A31:  a <> x
      proof
        assume not thesis;
        then x in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A32:    x in the carrier of R by A2,NECKLA_2:def 2;
        x in {x} by TARSKI:def 1;
        then x in the carrier of H by YELLOW_0:def 15;
        then x in (the carrier of R) /\ the carrier of H by A32,XBOOLE_0:def 4;
        hence contradiction by A16;
      end;
      a in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
      then
A33:  a in the carrier of R by A2,NECKLA_2:def 2;
      the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
      then
A34:  a is Element of ComplRelStr G by A33,NECKLACE:def 8;
A35:  x is Element of ComplRelStr G by NECKLACE:def 8;
      assume not thesis;
      then (the InternalRel of ComplRelStr G) reduces x,a by A31,A34,A35;
      then consider p being FinSequence such that
A36:  len p > 0 and
A37:  p.1 = x and
A38:  p.len p = a and
A39:  for i being Nat st i in dom p & i+1 in dom p holds [
      p.i, p.(i+1)] in (the InternalRel of ComplRelStr G) by REWRITE1:11;
A40:  0 + 1 <= len p by A36,NAT_1:13;
      then len p > 1 by A31,A37,A38,XXREAL_0:1;
      then 1+1 <= len p by NAT_1:13;
      then
A41:  2 in dom p by FINSEQ_3:25;
      1 in dom p by A40,FINSEQ_3:25;
      then
A42:  [p.1,p.(1+1)] in (the InternalRel of ComplRelStr G) by A39,A41;
A43:  p.2 <> x
      proof
A44:    [x,x] in id the carrier of G by RELAT_1:def 10;
        assume not thesis;
        then [x,x] in (the InternalRel of ComplRelStr G) /\ id the carrier of
        G by A37,A42,A44,XBOOLE_0:def 4;
        then (the InternalRel of ComplRelStr G) meets id the carrier of G;
        hence contradiction by Th13;
      end;
      p.2 in the carrier of ComplRelStr G by A42,ZFMISC_1:87;
      then
A45:  p.2 in the carrier of G by NECKLACE:def 8;
      p.2 in the carrier of R
      proof
        assume not thesis;
        then p.2 in {x} by A19,A45,XBOOLE_0:def 3;
        hence thesis by A43,TARSKI:def 1;
      end;
      then
A46:  [p.2,x] in the InternalRel of G by A29;
A47:  the InternalRel of ComplRelStr G is_symmetric_in the carrier of
      ComplRelStr G by NECKLACE:def 3;
      p.1 in the carrier of ComplRelStr G & p.(1+1) in the carrier of
      ComplRelStr G by A42,ZFMISC_1:87;
      then [p.(1+1),p.1] in the InternalRel of ComplRelStr G by A42,A47;
      then [p.2,x] in (the InternalRel of ComplRelStr G) /\ the InternalRel
      of G by A37,A46,XBOOLE_0:def 4;
      then (the InternalRel of ComplRelStr G) meets the InternalRel of G;
      hence thesis by Th12;
    end;
    hence thesis by A5;
  end;
  thus thesis
  proof
    per cases by A25;
    suppose
A48:  Y1 is non empty;
      ex b being Element of Y1, c being Element of X1 st [b,c] in the
      InternalRel of G
      proof
        set b = the Element of Y1;
        a in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A49:    a in the carrier of R by A2,NECKLA_2:def 2;
        b in Y1 by A48;
        then ex y being Element of R1 st y = b & not [y,x] in the InternalRel
        of G;
        then b in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A50:    b in the carrier of R by A2,NECKLA_2:def 2;
A51:    the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
        then reconsider a as Element of G by A49;
        reconsider b as Element of G by A51,A50;
        a <> b
        proof
          assume
A52:      not thesis;
          a in X1 by A6;
          then a in X1 /\ Y1 by A48,A52,XBOOLE_0:def 4;
          hence contradiction by A8;
        end;
        then (the InternalRel of G) reduces a,b by A4;
        then consider p being FinSequence such that
A53:    len p > 0 and
A54:    p.1 = a and
A55:    p.len p = b and
A56:    for i being Nat st i in dom p & i+1 in dom p
        holds [p.i, p.(i+1)] in (the InternalRel of G) by REWRITE1:11;
        defpred P[Nat] means p.$1 in Y1 & $1 in dom p & for k being Nat st k >
        $1 holds k in dom p implies p.k in Y1;
        for k being Nat st k > len p holds k in dom p implies p.k in Y1
        proof
          let k be Nat such that
A57:      k > len p;
          assume k in dom p;
          then k in Seg (len p) by FINSEQ_1:def 3;
          hence thesis by A57,FINSEQ_1:1;
        end;
        then P[len p] by A48,A53,A55,CARD_1:27,FINSEQ_5:6;
        then
A58:    ex k being Nat st P[k];
        ex n0 being Nat st P[n0] & for n being Nat st P[n] holds n >= n0
        from NAT_1:sch 5(A58);
        then consider n0 being Nat such that
A59:    P[n0] and
A60:    for n being Nat st P[n] holds n >= n0;
        n0 <> 0
        proof
          assume not thesis;
          then 0 in Seg (len p) by A59,FINSEQ_1:def 3;
          hence contradiction by FINSEQ_1:1;
        end;
        then consider k0 being Nat such that
A61:    n0 = k0 + 1 by NAT_1:6;
A62:    n0 <> 1
        proof
          assume
A63:      not thesis;
          a in X1 by A6;
          then X1 /\ Y1 is non empty by A54,A59,A63,XBOOLE_0:def 4;
          hence contradiction by A8;
        end;
A64:    k0 >= 1
        proof
          assume not thesis;
          then k0 = 0 by NAT_1:25;
          hence contradiction by A61,A62;
        end;
        n0 in Seg (len p) by A59,FINSEQ_1:def 3;
        then k0 <= k0 + 1 & n0 <= len p by FINSEQ_1:1,XREAL_1:29;
        then
A65:    k0 <= len p by A61,XXREAL_0:2;
        then
A66:    k0 in dom p by A64,FINSEQ_3:25;
        then
A67:    [p.k0,p.(k0+1)] in the InternalRel of G by A56,A59,A61;
        then
A68:    the InternalRel of G is_symmetric_in the carrier of G & p.k0 in
        the carrier of G by NECKLACE:def 3,ZFMISC_1:87;
        p.n0 in the carrier of G by A61,A67,ZFMISC_1:87;
        then
A69:    [p.n0,p.k0] in the InternalRel of G by A61,A67,A68;
A70:    for k being Nat st k > k0 holds k in dom p implies p.k in Y1
        proof
          assume not thesis;
          then consider k being Nat such that
A71:      k > k0 and
A72:      k in dom p and
A73:      not p.k in Y1;
          k > n0
          proof
            per cases by XXREAL_0:1;
            suppose
              k < n0;
              hence thesis by A61,A71,NAT_1:13;
            end;
            suppose
              n0 < k;
              hence thesis;
            end;
            suppose
              n0 = k;
              hence thesis by A59,A73;
            end;
          end;
          hence contradiction by A59,A72,A73;
        end;
        k0 < n0 by A61,NAT_1:13;
        then
A74:    not P[k0] by A60;
        p.k0 in the carrier of G by A67,ZFMISC_1:87;
        then p.k0 in the carrier of R or p.k0 in {x} by A19,XBOOLE_0:def 3;
        then
A75:    p.k0 in (the carrier of R1) \/ the carrier of R2 or p.k0 in {x}
        by A2,NECKLA_2:def 2;
        thus thesis
        proof
          per cases by A61,A67,A75,XBOOLE_0:def 3,ZFMISC_1:87;
          suppose
A76:        p.k0 in the carrier of R1 & p.n0 in the carrier of G;
            then reconsider
            m=p.k0 as Element of X1 by A11,A64,A65,A74,A70,FINSEQ_3:25
,XBOOLE_0:def 3;
            m in (the carrier of R1) \/ the carrier of R2 by A76,XBOOLE_0:def 3
;
            then
A77:        m in the carrier of R by A2,NECKLA_2:def 2;
            reconsider l=p.n0 as Element of Y1 by A59;
A78:        the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
            l in the carrier of R1 by A11,A59,XBOOLE_0:def 3;
            then l in (the carrier of R1) \/ the carrier of R2 by
XBOOLE_0:def 3;
            then
A79:        l in the carrier of R by A2,NECKLA_2:def 2;
            [m,l] in the InternalRel of G & the InternalRel of G
            is_symmetric_in the carrier of G by A56,A59,A61,A66,NECKLACE:def 3;
            then [l,m] in the InternalRel of G by A79,A77,A78;
            hence thesis;
          end;
          suppose
            p.k0 in the carrier of R2 & p.n0 in the carrier of G;
            then reconsider m=p.k0 as Element of R2;
            reconsider l=p.n0 as Element of R1 by A11,A59,XBOOLE_0:def 3;
            m in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
            then
A80:        m in the carrier of R by A2,NECKLA_2:def 2;
            l in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
            then l in the carrier of R by A2,NECKLA_2:def 2;
            then [l,m] in [:the carrier of R,the carrier of R:] by A80,
ZFMISC_1:87;
            then [l,m] in (the InternalRel of G)|_2 the carrier of R by A69,
XBOOLE_0:def 4;
            then [l,m] in the InternalRel of R by YELLOW_0:def 14;
            hence thesis by A1,A2,Th35;
          end;
          suppose
A81:        p.k0 in {x} & p.n0 in the carrier of G;
            ex y1 being Element of R1 st p.n0 = y1 & not [y1,x] in the
            InternalRel of G by A59;
            hence thesis by A69,A81,TARSKI:def 1;
          end;
        end;
      end;
      then consider u being Element of Y1, v being Element of X1 such that
A82:  [u,v] in the InternalRel of G;
      set w = the Element of X2;
      w in X2 by A18;
      then
A83:  ex y being Element of R2 st y = w & [y,x] in the InternalRel of G;
      set Z = {u,v,x,w};
      Z c= the carrier of G
      proof
        w in X2 by A18;
        then ex y2 being Element of R2 st y2 = w & [y2,x] in the InternalRel
        of G;
        then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A84:    w in the carrier of R by A2,NECKLA_2:def 2;
        v in X1 by A10;
        then ex y1 being Element of R1 st y1 = v & [y1,x] in the InternalRel
        of G;
        then v in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A85:    v in the carrier of R by A2,NECKLA_2:def 2;
        u in the carrier of R1 by A11,A48,XBOOLE_0:def 3;
        then u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A86:    u in the carrier of R by A2,NECKLA_2:def 2;
        let q be object;
        assume q in Z;
        then
A87:    q = u or q = v or q = x or q = w by ENUMSET1:def 2;
        the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
        hence thesis by A87,A86,A85,A84;
      end;
      then reconsider Z as Subset of G;
      reconsider H = subrelstr Z as non empty full SubRelStr of G by
YELLOW_0:def 15;
A88:  w in X2 by A18;
      reconsider w as Element of G by A83,ZFMISC_1:87;
A89:  v in X1 by A10;
A90:  [x,w] in the InternalRel of G
      proof
        (ex y1 being Element of R2 st w = y1 & [y1,x] in the InternalRel
of G )& the InternalRel of G is_symmetric_in the carrier of G by A88,
NECKLACE:def 3;
        hence thesis;
      end;
A91:  u in Y1 by A48;
      reconsider u,v as Element of G by A82,ZFMISC_1:87;
A92:  [v,x] in the InternalRel of G
      proof
        ex y1 being Element of R1 st v = y1 & [y1,x] in the InternalRel
        of G by A89;
        hence thesis;
      end;
A93:  w <> u
      proof
        assume
A94:    not thesis;
        (ex y1 being Element of R2 st w = y1 & [y1,x] in the InternalRel
of G )& ex y2 being Element of R1 st u = y2 & not [y2,x] in the InternalRel of
        G by A91,A88;
        hence contradiction by A94;
      end;
A95:  not [u,x] in the InternalRel of G
      proof
        ex y1 being Element of R1 st u = y1 & not [y1,x] in the
        InternalRel of G by A91;
        hence thesis;
      end;
A96:  not [v,w] in the InternalRel of G
      proof
A97:    ex y2 being Element of R2 st w = y2 & [y2,x] in the InternalRel
        of G by A88;
        then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then reconsider w as Element of R by A2,NECKLA_2:def 2;
A98:    ex y1 being Element of R1 st v = y1 & [y1,x] in the InternalRel
        of G by A89;
        then v in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then reconsider v as Element of R by A2,NECKLA_2:def 2;
        assume not thesis;
        then [v,w] in (the InternalRel of G)|_2 the carrier of R by
XBOOLE_0:def 4;
        then [v,w] in the InternalRel of R by YELLOW_0:def 14;
        then
A99:    [v,w] in (the InternalRel of R1) \/ (the InternalRel of R2 ) by A2,
NECKLA_2:def 2;
        per cases by A99,XBOOLE_0:def 3;
        suppose
          [v,w] in the InternalRel of R1;
          then w in the carrier of R1 by ZFMISC_1:87;
          then w in (the carrier of R1) /\ the carrier of R2 by A97,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
        suppose
          [v,w] in the InternalRel of R2;
          then v in the carrier of R2 by ZFMISC_1:87;
          then v in (the carrier of R1) /\ the carrier of R2 by A98,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
      end;
A100: w <> x
      proof
        assume
A101:   not thesis;
        ex y1 being Element of R2 st w = y1 & [y1,x] in the InternalRel
        of G by A88;
        then x in (the carrier of R1) \/ the carrier of R2 by A101,
XBOOLE_0:def 3;
        then x in the carrier of R by A2,NECKLA_2:def 2;
        then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
        then not x in {x} by XBOOLE_0:def 5;
        hence contradiction by TARSKI:def 1;
      end;
A102: not [u,w] in the InternalRel of G
      proof
A103:   ex y2 being Element of R2 st w = y2 & [y2,x] in the InternalRel
        of G by A88;
        then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then reconsider w as Element of R by A2,NECKLA_2:def 2;
A104:   ex y1 being Element of R1 st u = y1 & not [y1,x] in the
        InternalRel of G by A91;
        then u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then reconsider u as Element of R by A2,NECKLA_2:def 2;
        assume not thesis;
        then [u,w] in (the InternalRel of G)|_2 the carrier of R by
XBOOLE_0:def 4;
        then [u,w] in the InternalRel of R by YELLOW_0:def 14;
        then
A105:   [u,w] in (the InternalRel of R1) \/ (the InternalRel of R2 ) by A2,
NECKLA_2:def 2;
        per cases by A105,XBOOLE_0:def 3;
        suppose
          [u,w] in the InternalRel of R1;
          then w in the carrier of R1 by ZFMISC_1:87;
          then w in (the carrier of R1) /\ the carrier of R2 by A103,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
        suppose
          [u,w] in the InternalRel of R2;
          then u in the carrier of R2 by ZFMISC_1:87;
          then u in (the carrier of R1) /\ the carrier of R2 by A104,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
      end;
A106: x <> u
      proof
        assume
A107:   not thesis;
        ex y1 being Element of R1 st u = y1 & not [y1,x] in the
        InternalRel of G by A91;
        then x in (the carrier of R1) \/ (the carrier of R2) by A107,
XBOOLE_0:def 3;
        then x in the carrier of R by A2,NECKLA_2:def 2;
        then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
        then not x in {x} by XBOOLE_0:def 5;
        hence contradiction by TARSKI:def 1;
      end;
A108: w <> v
      proof
        consider y1 being Element of R2 such that
A109:   w = y1 and
        [y1,x] in the InternalRel of G by A88;
        assume
A110:   not thesis;
        ex y2 being Element of R1 st v = y2 & [y2,x] in the InternalRel
        of G by A89;
        then y1 in (the carrier of R1) /\ (the carrier of R2) by A110,A109,
XBOOLE_0:def 4;
        hence contradiction by A1;
      end;
A111: v <> x
      proof
        assume
A112:   not thesis;
        ex y1 being Element of R1 st v = y1 & [y1,x] in the InternalRel
        of G by A89;
        then x in (the carrier of R1) \/ the carrier of R2 by A112,
XBOOLE_0:def 3;
        then x in the carrier of R by A2,NECKLA_2:def 2;
        then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
        then not x in {x} by XBOOLE_0:def 5;
        hence contradiction by TARSKI:def 1;
      end;
      u <> v
      proof
        assume
A113:   not thesis;
        (ex y1 being Element of R1 st u = y1 & not [y1,x] in the
        InternalRel of G )& ex y2 being Element of R1 st v = y2 & [y2,x] in the
        InternalRel of G by A91,A89;
        hence contradiction by A113;
      end;
      then u,v,x,w are_mutually_distinct by A111,A106,A93,A108,A100,
ZFMISC_1:def 6;
      then
A114: subrelstr Z embeds Necklace 4 by A82,A92,A90,A95,A102,A96,Th38;
      G embeds Necklace 4
      proof
        assume not thesis;
        then G is N-free by NECKLA_2:def 1;
        then H is N-free by Th23;
        hence thesis by A114,NECKLA_2:def 1;
      end;
      hence thesis;
    end;
    suppose
A115: Y2 is non empty;
      ex c being Element of Y2, d being Element of X2 st [c,d] in the
      InternalRel of G
      proof
        set c = the Element of Y2;
        b in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A116:   b in the carrier of R by A2,NECKLA_2:def 2;
        c in Y2 by A115;
        then ex y being Element of R2 st y = c & not [y,x] in the InternalRel
        of G;
        then c in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A117:   c in the carrier of R by A2,NECKLA_2:def 2;
A118:   the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
        then reconsider b as Element of G by A116;
        reconsider c as Element of G by A118,A117;
        b <> c
        proof
          assume not thesis;
          then c in X2 by A7;
          then c in X2 /\ Y2 by A115,XBOOLE_0:def 4;
          hence contradiction by A14;
        end;
        then (the InternalRel of G) reduces b,c by A4;
        then consider p being FinSequence such that
A119:   len p > 0 and
A120:   p.1 = b and
A121:   p.len p = c and
A122:   for i being Nat st i in dom p & i+1 in dom p
        holds [p.i, p.(i+1)] in (the InternalRel of G) by REWRITE1:11;
        defpred P[Nat] means p.$1 in Y2 & $1 in dom p & for k being Nat st k >
        $1 holds k in dom p implies p.k in Y2;
        for k being Nat st k > len p holds k in dom p implies p.k in Y2
        proof
          let k be Nat such that
A123:     k > len p;
          assume k in dom p;
          then k in Seg (len p) by FINSEQ_1:def 3;
          hence thesis by A123,FINSEQ_1:1;
        end;
        then P[len p] by A115,A119,A121,CARD_1:27,FINSEQ_5:6;
        then
A124:   ex k being Nat st P[k];
        ex n0 being Nat st P[n0] & for n being Nat st P[n] holds n >= n0
        from NAT_1:sch 5(A124);
        then consider n0 being Nat such that
A125:   P[n0] and
A126:   for n being Nat st P[n] holds n >= n0;
        n0 <> 0
        proof
          assume not thesis;
          then 0 in Seg (len p) by A125,FINSEQ_1:def 3;
          hence contradiction by FINSEQ_1:1;
        end;
        then consider k0 being Nat such that
A127:   n0 = k0 + 1 by NAT_1:6;
A128:   n0 <> 1
        proof
          assume
A129:     not thesis;
          b in X2 by A7;
          then X2 /\ Y2 is non empty by A120,A125,A129,XBOOLE_0:def 4;
          hence contradiction by A14;
        end;
A130:   k0 >= 1
        proof
          assume not thesis;
          then k0 = 0 by NAT_1:25;
          hence contradiction by A127,A128;
        end;
        n0 in Seg (len p) by A125,FINSEQ_1:def 3;
        then k0 <= k0 + 1 & n0 <= len p by FINSEQ_1:1,XREAL_1:29;
        then k0 <= len p by A127,XXREAL_0:2;
        then
A131:   k0 in Seg (len p) by A130,FINSEQ_1:1;
        then
A132:   k0 in dom p by FINSEQ_1:def 3;
        then
A133:   [p.k0,p.(k0+1)] in the InternalRel of G by A122,A125,A127;
        then
A134:   the InternalRel of G is_symmetric_in the carrier of G & p.k0 in
        the carrier of G by NECKLACE:def 3,ZFMISC_1:87;
        p.n0 in the carrier of G by A127,A133,ZFMISC_1:87;
        then
A135:   [p.n0,p.k0] in the InternalRel of G by A127,A133,A134;
A136:   for k being Nat st k > k0 holds k in dom p implies p.k in Y2
        proof
          assume not thesis;
          then consider k being Nat such that
A137:     k > k0 and
A138:     k in dom p and
A139:     not p.k in Y2;
          k > n0
          proof
            per cases by XXREAL_0:1;
            suppose
              k < n0;
              hence thesis by A127,A137,NAT_1:13;
            end;
            suppose
              n0 < k;
              hence thesis;
            end;
            suppose
              n0 = k;
              hence thesis by A125,A139;
            end;
          end;
          hence contradiction by A125,A138,A139;
        end;
        k0 < n0 by A127,NAT_1:13;
        then
A140:   not P[k0] by A126;
        p.k0 in the carrier of G by A133,ZFMISC_1:87;
        then p.k0 in the carrier of R or p.k0 in {x} by A19,XBOOLE_0:def 3;
        then
A141:   p.k0 in (the carrier of R1) \/ the carrier of R2 or p.k0 in {x}
        by A2,NECKLA_2:def 2;
        thus thesis
        proof
          per cases by A127,A133,A141,XBOOLE_0:def 3,ZFMISC_1:87;
          suppose
            p.k0 in the carrier of R2 & p.n0 in the carrier of G;
            then reconsider m=p.k0 as Element of X2 by A22,A131,A140,A136,
FINSEQ_1:def 3,XBOOLE_0:def 3;
            reconsider l=p.n0 as Element of Y2 by A125;
            [m,l] in the InternalRel of G by A122,A125,A127,A132;
            hence thesis by A135;
          end;
          suppose
            p.k0 in the carrier of R1 & p.n0 in the carrier of G;
            then reconsider m=p.k0 as Element of R1;
            reconsider l=p.n0 as Element of R2 by A22,A125,XBOOLE_0:def 3;
A142:       the InternalRel of R is_symmetric_in the carrier of R by
NECKLACE:def 3;
            m in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
            then
A143:       m in the carrier of R by A2,NECKLA_2:def 2;
            l in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
            then
A144:       l in the carrier of R by A2,NECKLA_2:def 2;
            then [l,m] in [:the carrier of R,the carrier of R:] by A143,
ZFMISC_1:87;
            then [l,m] in (the InternalRel of G)|_2 the carrier of R by A135,
XBOOLE_0:def 4;
            then [l,m] in the InternalRel of R by YELLOW_0:def 14;
            then [m,l] in the InternalRel of R by A144,A143,A142;
            hence thesis by A1,A2,Th35;
          end;
          suppose
A145:       p.k0 in {x} & p.n0 in the carrier of G;
            ex y1 being Element of R2 st p.n0 = y1 & not [y1,x] in the
            InternalRel of G by A125;
            hence thesis by A135,A145,TARSKI:def 1;
          end;
        end;
      end;
      then consider u being Element of Y2, v being Element of X2 such that
A146: [u,v] in the InternalRel of G;
      set w = the Element of X1;
      w in X1 by A10;
      then
A147: ex y being Element of R1 st y = w & [y,x] in the InternalRel of G;
      set Z = {u,v,x,w};
      Z c= the carrier of G
      proof
        w in X1 by A10;
        then ex y2 being Element of R1 st y2 = w & [y2,x] in the InternalRel
        of G;
        then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A148:   w in the carrier of R by A2,NECKLA_2:def 2;
        v in X2 by A18;
        then ex y1 being Element of R2 st y1 = v & [y1,x] in the InternalRel
        of G;
        then v in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A149:   v in the carrier of R by A2,NECKLA_2:def 2;
        u in the carrier of R2 by A22,A115,XBOOLE_0:def 3;
        then u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then
A150:   u in the carrier of R by A2,NECKLA_2:def 2;
        let q be object;
        assume q in Z;
        then
A151:   q = u or q = v or q = x or q = w by ENUMSET1:def 2;
        the carrier of R c= the carrier of G by A19,XBOOLE_1:7;
        hence thesis by A151,A150,A149,A148;
      end;
      then reconsider Z as Subset of G;
      reconsider H = subrelstr Z as non empty full SubRelStr of G by
YELLOW_0:def 15;
A152: w in X1 by A10;
      reconsider w as Element of G by A147,ZFMISC_1:87;
A153: v in X2 by A18;
A154: [x,w] in the InternalRel of G
      proof
        (ex y1 being Element of R1 st w = y1 & [y1,x] in the InternalRel
of G )& the InternalRel of G is_symmetric_in the carrier of G by A152,
NECKLACE:def 3;
        hence thesis;
      end;
A155: u in Y2 by A115;
      reconsider u,v as Element of G by A146,ZFMISC_1:87;
A156: [v,x] in the InternalRel of G
      proof
        ex y1 being Element of R2 st v = y1 & [y1,x] in the InternalRel
        of G by A153;
        hence thesis;
      end;
A157: w <> u
      proof
        assume
A158:   not thesis;
        (ex y1 being Element of R1 st w = y1 & [y1,x] in the InternalRel
of G )& ex y2 being Element of R2 st u = y2 & not [y2,x] in the InternalRel of
        G by A155,A152;
        hence contradiction by A158;
      end;
A159: not [u,x] in the InternalRel of G
      proof
        ex y1 being Element of R2 st u = y1 & not [y1,x] in the
        InternalRel of G by A155;
        hence thesis;
      end;
A160: not [v,w] in the InternalRel of G
      proof
A161:   ex y2 being Element of R1 st w = y2 & [y2,x] in the InternalRel
        of G by A152;
        then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then reconsider w as Element of R by A2,NECKLA_2:def 2;
A162:   ex y1 being Element of R2 st v = y1 & [y1,x] in the InternalRel
        of G by A153;
        then v in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then reconsider v as Element of R by A2,NECKLA_2:def 2;
        assume not thesis;
        then [v,w] in (the InternalRel of G)|_2 the carrier of R by
XBOOLE_0:def 4;
        then [v,w] in the InternalRel of R by YELLOW_0:def 14;
        then
A163:   [v,w] in (the InternalRel of R1) \/ (the InternalRel of R2 ) by A2,
NECKLA_2:def 2;
        per cases by A163,XBOOLE_0:def 3;
        suppose
          [v,w] in the InternalRel of R1;
          then v in the carrier of R1 by ZFMISC_1:87;
          then v in (the carrier of R1) /\ the carrier of R2 by A162,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
        suppose
          [v,w] in the InternalRel of R2;
          then w in the carrier of R2 by ZFMISC_1:87;
          then w in (the carrier of R1) /\ the carrier of R2 by A161,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
      end;
A164: w <> x
      proof
        assume
A165:   not thesis;
        ex y1 being Element of R1 st w = y1 & [y1,x] in the InternalRel
        of G by A152;
        then x in (the carrier of R1) \/ the carrier of R2 by A165,
XBOOLE_0:def 3;
        then x in the carrier of R by A2,NECKLA_2:def 2;
        then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
        then not x in {x} by XBOOLE_0:def 5;
        hence contradiction by TARSKI:def 1;
      end;
A166: not [u,w] in the InternalRel of G
      proof
A167:   ex y2 being Element of R1 st w = y2 & [y2,x] in the InternalRel
        of G by A152;
        then w in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then reconsider w as Element of R by A2,NECKLA_2:def 2;
A168:   ex y1 being Element of R2 st u = y1 & not [y1,x] in the
        InternalRel of G by A155;
        then u in (the carrier of R1) \/ the carrier of R2 by XBOOLE_0:def 3;
        then reconsider u as Element of R by A2,NECKLA_2:def 2;
        assume not thesis;
        then [u,w] in (the InternalRel of G)|_2 the carrier of R by
XBOOLE_0:def 4;
        then [u,w] in the InternalRel of R by YELLOW_0:def 14;
        then
A169:   [u,w] in (the InternalRel of R1) \/ (the InternalRel of R2 ) by A2,
NECKLA_2:def 2;
        per cases by A169,XBOOLE_0:def 3;
        suppose
          [u,w] in the InternalRel of R1;
          then u in the carrier of R1 by ZFMISC_1:87;
          then u in (the carrier of R1) /\ the carrier of R2 by A168,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
        suppose
          [u,w] in the InternalRel of R2;
          then w in the carrier of R2 by ZFMISC_1:87;
          then w in (the carrier of R1) /\ the carrier of R2 by A167,
XBOOLE_0:def 4;
          hence contradiction by A1;
        end;
      end;
A170: x <> u
      proof
        assume
A171:   not thesis;
        ex y1 being Element of R2 st u = y1 & not [y1,x] in the
        InternalRel of G by A155;
        then x in (the carrier of R1) \/ (the carrier of R2) by A171,
XBOOLE_0:def 3;
        then x in the carrier of R by A2,NECKLA_2:def 2;
        then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
        then not x in {x} by XBOOLE_0:def 5;
        hence contradiction by TARSKI:def 1;
      end;
A172: w <> v
      proof
        consider y1 being Element of R1 such that
A173:   w = y1 and
        [y1,x] in the InternalRel of G by A152;
        assume
A174:   not thesis;
        ex y2 being Element of R2 st v = y2 & [y2,x] in the InternalRel
        of G by A153;
        then y1 in (the carrier of R1) /\ (the carrier of R2) by A174,A173,
XBOOLE_0:def 4;
        hence contradiction by A1;
      end;
A175: v <> x
      proof
        assume
A176:   not thesis;
        ex y1 being Element of R2 st v = y1 & [y1,x] in the InternalRel
        of G by A153;
        then x in (the carrier of R1) \/ the carrier of R2 by A176,
XBOOLE_0:def 3;
        then x in the carrier of R by A2,NECKLA_2:def 2;
        then x in (the carrier of G) \ {x} by YELLOW_0:def 15;
        then not x in {x} by XBOOLE_0:def 5;
        hence contradiction by TARSKI:def 1;
      end;
      u <> v
      proof
        assume
A177:   not thesis;
        (ex y1 being Element of R2 st u = y1 & not [y1,x] in the
        InternalRel of G )& ex y2 being Element of R2 st v = y2 & [y2,x] in the
        InternalRel of G by A155,A153;
        hence contradiction by A177;
      end;
      then u,v,x,w are_mutually_distinct by A175,A170,A157,A172,A164,
ZFMISC_1:def 6;
      then
A178: subrelstr Z embeds Necklace 4 by A146,A156,A154,A159,A166,A160,Th38;
      G embeds Necklace 4
      proof
        assume not thesis;
        then G is N-free by NECKLA_2:def 1;
        then H is N-free by Th23;
        hence thesis by A178,NECKLA_2:def 1;
      end;
      hence thesis;
    end;
  end;
end;

theorem
  for G being non empty strict finite irreflexive symmetric RelStr st G
is N-free & the carrier of G in FinSETS holds the RelStr of G in fin_RelStr_sp
proof
  let R be non empty strict finite irreflexive symmetric RelStr;
  defpred P[Nat] means for G be non empty strict finite irreflexive symmetric
  RelStr st G is N-free & card the carrier of G = $1 & the carrier of G in
  FinSETS holds (the RelStr of G) in fin_RelStr_sp;
A1: for n be Nat st for k be Nat st k < n holds P[k] holds P[n]
  proof
    let n be Nat such that
A2: for k be Nat st k < n holds P[k];
    let G be non empty strict finite irreflexive symmetric RelStr;
    set CG = ComplRelStr G;
    assume that
A3: G is N-free and
A4: card (the carrier of G) = n and
A5: (the carrier of G) in FinSETS;
    per cases;
    suppose
      G is trivial;
      then the carrier of G is 1-element;
      then reconsider G as 1-element RelStr by STRUCT_0:def 19;
      (the RelStr of G) in fin_RelStr_sp by A5,NECKLA_2:def 5;
      hence thesis;
    end;
    suppose
      G is not path-connected & G is non trivial;
      then consider
      G1,G2 being non empty strict irreflexive symmetric RelStr such
      that
A6:   (the carrier of G1) misses (the carrier of G2) and
A7:   the RelStr of G = union_of(G1,G2) by Th30;
      set cG1 = the carrier of G1, cG2 = the carrier of G2, R = the RelStr of
      G, cR = the carrier of R;
      reconsider cR as finite set;
A8:   cR = cG1 \/ cG2 by A7,NECKLA_2:def 2;
      then
A9:   card cG1 in Segm card cR by A6,Lm1;
      then reconsider
      G1 as non empty strict finite irreflexive symmetric RelStr;
      reconsider cR as finite set;
A10:  card cG2 in Segm card cR by A6,A8,Lm1;
      then reconsider
      G2 as non empty strict finite irreflexive symmetric RelStr;
      reconsider cG2 as finite set by A10;
A11:  card cG2 < card cR by A10,NAT_1:44;
      G2 is full SubRelStr of G by A6,A7,Th10;
      then
A12:  G2 is N-free by A3,Th23;
      the carrier of G2 in FinSETS by A5,A8,CLASSES1:3,CLASSES2:def 2
,XBOOLE_1:7;
      then
A13:  G2 in fin_RelStr_sp by A2,A4,A11,A12;
      G1 is full SubRelStr of G by A6,A7,Th10;
      then
A14:  G1 is N-free by A3,Th23;
      reconsider cG1 as finite set by A9;
A15:  card cG1 < card cR by A9,NAT_1:44;
      the carrier of G1 in FinSETS by A5,A8,CLASSES1:3,CLASSES2:def 2
,XBOOLE_1:7;
      then G1 in fin_RelStr_sp by A2,A4,A15,A14;
      hence thesis by A6,A7,A13,NECKLA_2:def 5;
    end;
    suppose
      CG is not path-connected & G is non trivial;
      then consider
      G1,G2 being non empty strict irreflexive symmetric RelStr such
      that
A16:  (the carrier of G1) misses (the carrier of G2) and
A17:  (the RelStr of G) = sum_of(G1,G2) by Th31;
      set cG1 = the carrier of G1, cG2 = the carrier of G2, R = the RelStr of
      G, cR = the carrier of R;
      reconsider cR as finite set;
A18:  cR = cG1 \/ cG2 by A17,NECKLA_2:def 3;
      then
A19:  card cG1 in Segm card cR by A16,Lm1;
      then reconsider
      G1 as non empty strict finite irreflexive symmetric RelStr;
A20:  card cG2 in Segm card cR by A16,A18,Lm1;
      then reconsider
      G2 as non empty strict finite irreflexive symmetric RelStr;
      reconsider cG2 as finite set by A20;
A21:  card cG2 < card cR by A20,NAT_1:44;
      G2 is full SubRelStr of G by A16,A17,Th10;
      then
A22:  G2 is N-free by A3,Th23;
      the carrier of G2 in FinSETS by A5,A18,CLASSES1:3,CLASSES2:def 2
,XBOOLE_1:7;
      then
A23:  G2 in fin_RelStr_sp by A2,A4,A21,A22;
      G1 is full SubRelStr of G by A16,A17,Th10;
      then
A24:  G1 is N-free by A3,Th23;
      reconsider cG1 as finite set by A19;
A25:  card cG1 < card cR by A19,NAT_1:44;
      the carrier of G1 in FinSETS by A5,A18,CLASSES1:3,CLASSES2:def 2
,XBOOLE_1:7;
      then G1 in fin_RelStr_sp by A2,A4,A25,A24;
      hence thesis by A16,A17,A23,NECKLA_2:def 5;
    end;
    suppose
A26:  G is non trivial & G is path-connected & CG is path-connected;
      consider x be object such that
A27:  x in the carrier of G by XBOOLE_0:def 1;
      reconsider x as Element of G by A27;
      set A = (the carrier of G) \ {x};
A28:  A c= the carrier of G;
      reconsider A as Subset of G;
      set R = subrelstr A;
      reconsider R as non empty finite irreflexive symmetric RelStr by A26,
YELLOW_0:def 15;
A29:  the carrier of R c= the carrier of G by A28,YELLOW_0:def 15;
      card A = card (the carrier of G) - card {x} by CARD_2:44;
      then
A30:  card A = n - 1 by A4,CARD_2:42;
      n - 1 < n - 1 + 1 by XREAL_1:29;
      then
A31:  card the carrier of R < n by A30,YELLOW_0:def 15;
      R is N-free by A3,Th23;
      then
A32:  R in fin_RelStr_sp by A2,A5,A31,A29,CLASSES1:3,CLASSES2:def 2;
      thus thesis
      proof
        per cases by A32,NECKLA_2:6;
        suppose
A33:      R is trivial RelStr;
          the carrier of R is non empty;
          then
A34:      A is non empty by YELLOW_0:def 15;
          A is trivial by A33,YELLOW_0:def 15;
          then consider a be object such that
A35:      A = {a} by A34,ZFMISC_1:131;
A36:      (the carrier of G) \/ {x} = the carrier of G
          proof
            thus (the carrier of G) \/ {x} c= the carrier of G
            proof
              let c be object;
              assume c in (the carrier of G) \/ {x};
              then c in the carrier of G or c in {x} by XBOOLE_0:def 3;
              hence thesis;
            end;
            let c be object;
            assume c in the carrier of G;
            hence thesis by XBOOLE_0:def 3;
          end;
          {a} \/ {x} = (the carrier of G) \/ {x} by A35,XBOOLE_1:39;
          then the carrier of G = {a,x} & a <> x by A26,A36,ENUMSET1:1;
          then card (the carrier of G) = 2 by CARD_2:57;
          hence thesis by A5,Th33;
        end;
        suppose
          ex R1,R2 being strict RelStr st (the carrier of R1) misses
(the carrier of R2) & R1 in fin_RelStr_sp & R2 in fin_RelStr_sp & (R = union_of
          (R1,R2) or R = sum_of(R1,R2) );
          then consider R1,R2 being strict RelStr such that
A37:      (the carrier of R1) misses (the carrier of R2) and
A38:      R1 in fin_RelStr_sp and
A39:      R2 in fin_RelStr_sp and
A40:      R = union_of(R1,R2) or R = sum_of(R1,R2);
          thus thesis
          proof
            per cases by A40;
            suppose
A41:          R = union_of(R1,R2);
              R2 is SubRelStr of R by A37,A40,Th10;
              then reconsider R2 as non empty SubRelStr of G by A39,NECKLA_2:4
,YELLOW_6:7;
              R1 is SubRelStr of R by A37,A40,Th10;
              then reconsider R1 as non empty SubRelStr of G by A38,NECKLA_2:4
,YELLOW_6:7;
              subrelstr ([#]G \ {x}) = union_of(R1,R2) by A41;
              then G embeds Necklace 4 by A26,A37,Th39;
              hence thesis by A3,NECKLA_2:def 1;
            end;
            suppose
A42:          R = sum_of(R1,R2);
              ComplRelStr R2 is non empty
              proof
                assume not thesis;
                then R2 is empty;
                hence contradiction by A39,NECKLA_2:4;
              end;
              then reconsider R22 = ComplRelStr R2 as non empty RelStr;
              ComplRelStr R1 is non empty
              proof
                assume not thesis;
                then R1 is empty;
                hence contradiction by A38,NECKLA_2:4;
              end;
              then reconsider R11 = ComplRelStr R1 as non empty RelStr;
              reconsider G9 = ComplRelStr G as non empty irreflexive symmetric
              RelStr;
              reconsider x9 = x as Element of G9 by NECKLACE:def 8;
A43:          the carrier of R11 = the carrier of R1 & the carrier of R22
              = the carrier of R2 by NECKLACE:def 8;
A44:          ComplRelStr R = ComplRelStr (subrelstr ([#]G \ {x}))
                .= subrelstr ([#](G9) \ {x9}) by Th20;
A45:          G9 is N-free by A3,Th25;
A46:          ComplRelStr G9 is path-connected & G9 is non trivial by A26,Th16,
NECKLACE:def 8;
              ComplRelStr R = union_of(ComplRelStr R1, ComplRelStr R2) by A37
,A42,Th18;
              then G9 embeds Necklace 4 by A26,A37,A43,A46,A44,Th39;
              hence thesis by A45,NECKLA_2:def 1;
            end;
          end;
        end;
      end;
    end;
  end;
A47: for k be Nat holds P[k] from NAT_1:sch 4(A1);
  card the carrier of R is Nat;
  hence thesis by A47;
end;

{"subset_name": "curated", "file": "formal/mizar/neckla_3.miz"}