necklace.miz



    begin

    reserve i,j,k,n for Nat;

    reserve x,x1,x2,x3,y1,y2,y3 for set;

    theorem :: NECKLACE:1

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

    theorem :: NECKLACE:2

     [: {x1, x2, x3}, {y1, y2, y3}:] = { [x1, y1], [x1, y2], [x1, y3], [x2, y1], [x2, y2], [x2, y3], [x3, y1], [x3, y2], [x3, y3]}

    proof

      

      thus [: {x1, x2, x3}, {y1, y2, y3}:] = [:( {x1} \/ {x2, x3}), {y1, y2, y3}:] by ENUMSET1: 2

      .= [:( {x1} \/ {x2, x3}), ( {y1} \/ {y2, y3}):] by ENUMSET1: 2

      .= ((( [: {x1}, {y1}:] \/ [: {x1}, {y2, y3}:]) \/ [: {x2, x3}, {y1}:]) \/ [: {x2, x3}, {y2, y3}:]) by ZFMISC_1: 98

      .= ((( [: {x1}, {y1}:] \/ [: {x1}, {y2, y3}:]) \/ [: {x2, x3}, {y1}:]) \/ ( [: {x2}, {y2, y3}:] \/ [: {x3}, {y2, y3}:])) by ZFMISC_1: 109

      .= ((( { [x1, y1]} \/ [: {x1}, {y2, y3}:]) \/ [: {x2, x3}, {y1}:]) \/ ( [: {x2}, {y2, y3}:] \/ [: {x3}, {y2, y3}:])) by ZFMISC_1: 29

      .= ((( { [x1, y1]} \/ { [x1, y2], [x1, y3]}) \/ [: {x2, x3}, {y1}:]) \/ ( [: {x2}, {y2, y3}:] \/ [: {x3}, {y2, y3}:])) by ZFMISC_1: 30

      .= ((( { [x1, y1]} \/ { [x1, y2], [x1, y3]}) \/ { [x2, y1], [x3, y1]}) \/ ( [: {x2}, {y2, y3}:] \/ [: {x3}, {y2, y3}:])) by ZFMISC_1: 30

      .= ((( { [x1, y1]} \/ { [x1, y2], [x1, y3]}) \/ { [x2, y1], [x3, y1]}) \/ ( { [x2, y2], [x2, y3]} \/ [: {x3}, {y2, y3}:])) by ZFMISC_1: 30

      .= ((( { [x1, y1]} \/ { [x1, y2], [x1, y3]}) \/ { [x2, y1], [x3, y1]}) \/ ( { [x2, y2], [x2, y3]} \/ { [x3, y2], [x3, y3]})) by ZFMISC_1: 30

      .= (( { [x1, y1], [x1, y2], [x1, y3]} \/ { [x2, y1], [x3, y1]}) \/ ( { [x2, y2], [x2, y3]} \/ { [x3, y2], [x3, y3]})) by ENUMSET1: 2

      .= ( { [x1, y1], [x1, y2], [x1, y3], [x2, y1], [x3, y1]} \/ ( { [x2, y2], [x2, y3]} \/ { [x3, y2], [x3, y3]})) by ENUMSET1: 9

      .= ( { [x1, y1], [x1, y2], [x1, y3], [x2, y1], [x3, y1]} \/ { [x2, y2], [x2, y3], [x3, y2], [x3, y3]}) by ENUMSET1: 5

      .= { [x1, y1], [x1, y2], [x1, y3], [x2, y1], [x3, y1], [x2, y2], [x2, y3], [x3, y2], [x3, y3]} by ENUMSET1: 81

      .= ( { [x1, y1], [x1, y2], [x1, y3], [x2, y1]} \/ { [x3, y1], [x2, y2], [x2, y3], [x3, y2], [x3, y3]}) by ENUMSET1: 80

      .= ( { [x1, y1], [x1, y2], [x1, y3], [x2, y1]} \/ ( { [x3, y1], [x2, y2], [x2, y3]} \/ { [x3, y2], [x3, y3]})) by ENUMSET1: 9

      .= ( { [x1, y1], [x1, y2], [x1, y3], [x2, y1]} \/ ( { [x2, y2], [x2, y3], [x3, y1]} \/ { [x3, y2], [x3, y3]})) by ENUMSET1: 59

      .= ( { [x1, y1], [x1, y2], [x1, y3], [x2, y1]} \/ { [x2, y2], [x2, y3], [x3, y1], [x3, y2], [x3, y3]}) by ENUMSET1: 9

      .= { [x1, y1], [x1, y2], [x1, y3], [x2, y1], [x2, y2], [x2, y3], [x3, y1], [x3, y2], [x3, y3]} by ENUMSET1: 80;

    end;

    ::$Canceled

    theorem :: NECKLACE:4

    

     Th3: for x be non zero Nat holds 0 in x

    proof

      let x be non zero Nat;

      reconsider n = x as Element of NAT by ORDINAL1:def 12;

      n = { i where i be Nat : i < n } & 0 < n by AXIOMS: 4;

      hence thesis;

    end;

    registration

      let X be set;

      cluster ( delta X) -> one-to-one;

      coherence

      proof

        set f = ( delta X);

        let x1,x2 be object;

        assume that

         A1: x1 in ( dom f) & x2 in ( dom f) and

         A2: (f . x1) = (f . x2);

        (f . x1) = [x1, x1] & (f . x2) = [x2, x2] by A1, FUNCT_3:def 6;

        hence thesis by A2, XTUPLE_0: 1;

      end;

    end

    theorem :: NECKLACE:5

    

     Th4: for X be set holds ( card ( id X)) = ( card X)

    proof

      let X be set;

      ( id X) in ( Funcs (X,X)) by FUNCT_2: 9;

      hence thesis by CARD_2: 3;

    end;

    registration

      cluster trivial -> one-to-one for Function;

      coherence

      proof

        let f be Function such that

         A1: f is trivial;

        let x1,x2 be object;

        assume that

         A2: x1 in ( dom f) and

         A3: x2 in ( dom f) and (f . x1) = (f . x2);

        reconsider f as trivial Function by A1;

        consider x be object such that

         A4: ( dom f) = {x} by A2, ZFMISC_1: 131;

        x1 = x by A2, A4, TARSKI:def 1;

        hence thesis by A3, A4, TARSKI:def 1;

      end;

    end

    theorem :: NECKLACE:6

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

    theorem :: NECKLACE:7

    

     Th6: for f,g be one-to-one Function st ( dom f) misses ( dom g) & ( rng f) misses ( rng g) holds ((f +* g) " ) = ((f " ) +* (g " ))

    proof

      let f,g be one-to-one Function such that

       A1: ( dom f) misses ( dom g) and

       A2: ( rng f) misses ( rng g);

      

       A3: (f +* g) is one-to-one by A2, FUNCT_4: 92;

      

       A4: for y,x be object holds y in ( rng (f +* g)) & x = (((f " ) +* (g " )) . y) iff x in ( dom (f +* g)) & y = ((f +* g) . x)

      proof

        let y,x be object;

        thus y in ( rng (f +* g)) & x = (((f " ) +* (g " )) . y) implies x in ( dom (f +* g)) & y = ((f +* g) . x)

        proof

          

           A5: ( rng (f +* g)) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

          assume that

           A6: y in ( rng (f +* g)) and

           A7: x = (((f " ) +* (g " )) . y);

          per cases by A6, A5, XBOOLE_0:def 3;

            suppose

             A8: y in ( rng f);

            then

            consider z be object such that

             A9: z in ( dom f) and

             A10: y = (f . z) by FUNCT_1:def 3;

            ( dom (f +* g)) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

            then

             A11: z in ( dom (f +* g)) by A9, XBOOLE_0:def 3;

            

             A12: ( dom (f " )) = ( rng f) & ( dom (g " )) = ( rng g) by FUNCT_1: 33;

            y = ((f +* g) . z) & z = ((f " ) . y) by A1, A9, A10, FUNCT_1: 32, FUNCT_4: 16;

            hence thesis by A2, A7, A8, A11, A12, FUNCT_4: 16;

          end;

            suppose

             A13: y in ( rng g);

            

             A14: ( dom (f " )) = ( rng f) & ( dom (g " )) = ( rng g) by FUNCT_1: 33;

            consider z be object such that

             A15: z in ( dom g) and

             A16: y = (g . z) by A13, FUNCT_1:def 3;

            z = ((g " ) . y) by A15, A16, FUNCT_1: 32;

            then z = (((g " ) +* (f " )) . y) by A2, A13, A14, FUNCT_4: 16;

            then

             A17: z = x by A2, A7, A14, FUNCT_4: 35;

            ( dom (f +* g)) = (( dom f) \/ ( dom g)) & y = ((g +* f) . z) by A1, A15, A16, FUNCT_4: 16, FUNCT_4:def 1;

            hence thesis by A1, A15, A17, FUNCT_4: 35, XBOOLE_0:def 3;

          end;

        end;

        thus x in ( dom (f +* g)) & y = ((f +* g) . x) implies y in ( rng (f +* g)) & x = (((f " ) +* (g " )) . y)

        proof

          

           A18: ( dom (f +* g)) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

          assume that

           A19: x in ( dom (f +* g)) and

           A20: y = ((f +* g) . x);

          per cases by A19, A18, XBOOLE_0:def 3;

            suppose

             A21: x in ( dom f);

            then not x in ( dom g) by A1, XBOOLE_0: 3;

            then

             A22: y = (f . x) by A20, FUNCT_4: 11;

            then

             A23: x = ((f " ) . y) by A21, FUNCT_1: 32;

            

             A24: ( dom (f " )) = ( rng f) & ( dom (g " )) = ( rng g) by FUNCT_1: 33;

            

             A25: y in ( rng f) by A21, A22, FUNCT_1:def 3;

            then y in (( rng f) \/ ( rng g)) by XBOOLE_0:def 3;

            hence thesis by A1, A2, A25, A23, A24, FRECHET: 35, FUNCT_4: 16, PARTFUN1: 56;

          end;

            suppose

             A26: x in ( dom g);

            then

             A27: y = (g . x) by A20, FUNCT_4: 13;

            then

             A28: y in ( rng g) by A26, FUNCT_1:def 3;

            then

             A29: y in (( rng f) \/ ( rng g)) by XBOOLE_0:def 3;

            

             A30: ( dom (f " )) = ( rng f) & ( dom (g " )) = ( rng g) by FUNCT_1: 33;

            x = ((g " ) . y) by A26, A27, FUNCT_1: 32;

            then x = (((g " ) +* (f " )) . y) by A2, A28, A30, FUNCT_4: 16;

            hence thesis by A1, A2, A29, A30, FRECHET: 35, FUNCT_4: 35, PARTFUN1: 56;

          end;

        end;

      end;

      ( dom ((f " ) +* (g " ))) = (( dom (f " )) \/ ( dom (g " ))) by FUNCT_4:def 1

      .= (( rng f) \/ ( dom (g " ))) by FUNCT_1: 33

      .= (( rng f) \/ ( rng g)) by FUNCT_1: 33

      .= ( rng (f +* g)) by A1, FRECHET: 35, PARTFUN1: 56;

      hence thesis by A3, A4, FUNCT_1: 32;

    end;

    theorem :: NECKLACE:8

    for A,a,b be set holds ((A --> a) +* (A --> b)) = (A --> b)

    proof

      let A,a,b be set;

      set g = (A --> b);

      ( dom (A --> a)) c= ( dom g);

      hence thesis by FUNCT_4: 19;

    end;

    theorem :: NECKLACE:9

    

     Th8: for a,b be set holds ((a .--> b) " ) = (b .--> a)

    proof

      let a,b be set;

      set f = (a .--> b), g = (b .--> a);

      

       A1: for y,x be object holds y in ( rng f) & x = (g . y) iff x in ( dom f) & y = (f . x)

      proof

        let y,x be object;

        thus y in ( rng f) & x = (g . y) implies x in ( dom f) & y = (f . x)

        proof

          assume that

           A2: y in ( rng f) and

           A3: x = (g . y);

          

           A4: y in {b} by A2, FUNCOP_1: 8;

          

          then

           A5: x = (g . b) by A3, TARSKI:def 1

          .= a by FUNCOP_1: 72;

          then

           A6: x in {a} by TARSKI:def 1;

          (f . x) = b by A5, FUNCOP_1: 72

          .= y by A4, TARSKI:def 1;

          hence thesis by A6;

        end;

        assume that

         A7: x in ( dom f) and

         A8: y = (f . x);

        

         A9: x in {a} by A7;

        

        then

         A10: y = (f . a) by A8, TARSKI:def 1

        .= b by FUNCOP_1: 72;

        then

         A11: y in {b} by TARSKI:def 1;

        (g . y) = a by A10, FUNCOP_1: 72

        .= x by A9, TARSKI:def 1;

        hence thesis by A11, FUNCOP_1: 8;

      end;

      ( dom g) = {b}

      .= ( rng f) by FUNCOP_1: 8;

      hence thesis by A1, FUNCT_1: 32;

    end;

    theorem :: NECKLACE:10

    

     Th9: for a,b,c,d be set st a = b iff c = d holds (((a,b) --> (c,d)) " ) = ((c,d) --> (a,b))

    proof

      let a,b,c,d be set such that

       A1: a = b iff c = d;

      per cases by A1;

        suppose

         A2: a = b & c = d;

        (((a,a) --> (d,d)) " ) = ((a .--> d) " ) by FUNCT_4: 81

        .= (d .--> a) by Th8

        .= ((d,d) --> (a,a)) by FUNCT_4: 81;

        hence thesis by A2;

      end;

        suppose

         A3: a <> b & c <> d;

        set f = ((a,b) --> (c,d)), g = ((c,d) --> (a,b));

        

         A4: for y,x be object holds y in ( rng f) & x = (g . y) iff x in ( dom f) & y = (f . x)

        proof

          let y,x be object;

          

           A5: x in ( dom f) & y = (f . x) implies y in ( rng f) & x = (g . y)

          proof

            assume that

             A6: x in ( dom f) and

             A7: y = (f . x);

            

             A8: x in {a, b} by A6, FUNCT_4: 62;

            per cases by A8, TARSKI:def 2;

              suppose

               A9: x = a;

              then

               A10: y = c by A3, A7, FUNCT_4: 63;

              then y in {c, d} by TARSKI:def 2;

              hence thesis by A3, A9, A10, FUNCT_4: 63, FUNCT_4: 64;

            end;

              suppose

               A11: x = b;

              then

               A12: y = d by A7, FUNCT_4: 63;

              then y in {c, d} by TARSKI:def 2;

              hence thesis by A3, A11, A12, FUNCT_4: 63, FUNCT_4: 64;

            end;

          end;

          y in ( rng f) & x = (g . y) implies x in ( dom f) & y = (f . x)

          proof

            assume that

             A13: y in ( rng f) and

             A14: x = (g . y);

            

             A15: y in {c, d} by A3, A13, FUNCT_4: 64;

            per cases by A15, TARSKI:def 2;

              suppose

               A16: y = c;

              then

               A17: x = a by A3, A14, FUNCT_4: 63;

              then x in {a, b} by TARSKI:def 2;

              hence thesis by A3, A16, A17, FUNCT_4: 62, FUNCT_4: 63;

            end;

              suppose

               A18: y = d;

              then

               A19: x = b by A14, FUNCT_4: 63;

              then x in {a, b} by TARSKI:def 2;

              hence thesis by A18, A19, FUNCT_4: 62, FUNCT_4: 63;

            end;

          end;

          hence thesis by A5;

        end;

        

         A20: f is one-to-one

        proof

          

           A21: ( dom f) = {a, b} by FUNCT_4: 62;

          let x1,x2 be object such that

           A22: x1 in ( dom f) & x2 in ( dom f) and

           A23: (f . x1) = (f . x2);

          per cases by A22, A21, TARSKI:def 2;

            suppose x1 = a & x2 = a or x1 = b & x2 = b;

            hence thesis;

          end;

            suppose

             A24: x1 = a & x2 = b;

            then (f . x1) = c by A3, FUNCT_4: 63;

            hence thesis by A3, A23, A24, FUNCT_4: 63;

          end;

            suppose

             A25: x1 = b & x2 = a;

            then (f . x1) = d by FUNCT_4: 63;

            hence thesis by A3, A23, A25, FUNCT_4: 63;

          end;

        end;

        ( dom g) = {c, d} by FUNCT_4: 62

        .= ( rng f) by A3, FUNCT_4: 64;

        hence thesis by A20, A4, FUNCT_1: 32;

      end;

    end;

    scheme :: NECKLACE:sch1

    Convers { X() -> non empty set , R() -> Relation , F,G( set) -> set , P[ set] } :

(R() ~ ) = { [F(x), G(x)] where x be Element of X() : P[x] }

      provided

       A1: R() = { [G(x), F(x)] where x be Element of X() : P[x] };

      set S = { [F(x), G(x)] where x be Element of X() : P[x] };

      S is Relation-like

      proof

        let x be object;

        assume x in S;

        then ex y be Element of X() st x = [F(y), G(y)] & P[y];

        hence thesis;

      end;

      then

      reconsider S9 = S as Relation;

      

       A2: for x,y be object holds [y, x] in R() implies [x, y] in S9

      proof

        let x,y be object;

        assume [y, x] in R();

        then

        consider z be Element of X() such that

         A3: [y, x] = [G(z), F(z)] and

         A4: P[z] by A1;

        y = G(z) & x = F(z) by A3, XTUPLE_0: 1;

        hence thesis by A4;

      end;

      for x,y be object holds [x, y] in S9 implies [y, x] in R()

      proof

        let x,y be object;

        assume [x, y] in S9;

        then

        consider z be Element of X() such that

         A5: [x, y] = [F(z), G(z)] and

         A6: P[z];

        x = F(z) & y = G(z) by A5, XTUPLE_0: 1;

        hence thesis by A1, A6;

      end;

      hence thesis by A2, RELAT_1:def 7;

    end;

    theorem :: NECKLACE:11

    for i,j,n be Nat holds i < j & j in ( Segm n) implies i in ( Segm n)

    proof

      let i,j,n be Nat;

      assume that

       A1: i < j and

       A2: j in ( Segm n);

      j < n by A2, NAT_1: 44;

      then i < n by A1, XXREAL_0: 2;

      hence thesis by NAT_1: 44;

    end;

    begin

    definition

      let R,S be RelStr;

      :: NECKLACE:def1

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

    end

    definition

      let R,S be non empty RelStr;

      :: original: embeds

      redefine

      pred S embeds R;

      reflexivity

      proof

        let R be non empty RelStr;

        set f = ( id the carrier of R);

        reconsider f as Function of R, R;

        take f;

        thus f is one-to-one;

        let x,y be Element of R;

        thus thesis;

      end;

    end

    theorem :: NECKLACE:12

    

     Th11: for R,S,T be non empty RelStr holds R embeds S & S embeds T implies R embeds T

    proof

      let R,S,T be non empty RelStr;

      assume R embeds S;

      then

      consider f be Function of S, R such that

       A1: f is one-to-one and

       A2: for x,y be Element of S holds [x, y] in the InternalRel of S iff [(f . x), (f . y)] in the InternalRel of R;

      assume S embeds T;

      then

      consider g be Function of T, S such that

       A3: g is one-to-one and

       A4: for x,y be Element of T holds [x, y] in the InternalRel of T iff [(g . x), (g . y)] in the InternalRel of S;

      reconsider h = (f * g) as Function of T, R;

      take h;

      thus h is one-to-one by A1, A3;

      thus for x,y be Element of T holds [x, y] in the InternalRel of T iff [(h . x), (h . y)] in the InternalRel of R

      proof

        let x,y be Element of T;

        thus [x, y] in the InternalRel of T implies [(h . x), (h . y)] in the InternalRel of R

        proof

          assume [x, y] in the InternalRel of T;

          then

           A5: [(g . x), (g . y)] in the InternalRel of S by A4;

          (h . x) = (f . (g . x)) & (h . y) = (f . (g . y)) by FUNCT_2: 15;

          hence thesis by A2, A5;

        end;

        thus [(h . x), (h . y)] in the InternalRel of R implies [x, y] in the InternalRel of T

        proof

          

           A6: (h . x) = (f . (g . x)) & (h . y) = (f . (g . y)) by FUNCT_2: 15;

          assume [(h . x), (h . y)] in the InternalRel of R;

          then [(g . x), (g . y)] in the InternalRel of S by A2, A6;

          hence thesis by A4;

        end;

      end;

    end;

    definition

      let R,S be non empty RelStr;

      :: NECKLACE:def2

      pred R is_equimorphic_to S means R embeds S & S embeds R;

      reflexivity ;

      symmetry ;

    end

    theorem :: NECKLACE:13

    for R,S,T be non empty RelStr holds R is_equimorphic_to S & S is_equimorphic_to T implies R is_equimorphic_to T by Th11;

    notation

      let R be non empty RelStr;

      antonym R is parallel for R is connected;

    end

    definition

      let R be RelStr;

      :: NECKLACE:def3

      attr R is symmetric means

      : Def3: the InternalRel of R is_symmetric_in the carrier of R;

    end

    definition

      let R be RelStr;

      :: NECKLACE:def4

      attr R is asymmetric means the InternalRel of R is asymmetric;

    end

    theorem :: NECKLACE:14

    for R be RelStr st R is asymmetric holds the InternalRel of R misses (the InternalRel of R ~ )

    proof

      let R be RelStr;

      assume R is asymmetric;

      then the InternalRel of R is asymmetric;

      then

       A1: the InternalRel of R is_asymmetric_in ( field the InternalRel of R);

      assume the InternalRel of R meets (the InternalRel of R ~ );

      then

      consider x be object such that

       A2: x in the InternalRel of R and

       A3: x in (the InternalRel of R ~ ) by XBOOLE_0: 3;

      consider y,z be object such that

       A4: x = [y, z] by A3, RELAT_1:def 1;

      

       A5: z in ( field the InternalRel of R) by A2, A4, RELAT_1: 15;

       [z, y] in the InternalRel of R & y in ( field the InternalRel of R) by A2, A3, A4, RELAT_1: 15, RELAT_1:def 7;

      hence contradiction by A2, A4, A1, A5;

    end;

    definition

      let R be RelStr;

      :: NECKLACE:def5

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

    end

    definition

      let n be Nat;

      :: NECKLACE:def6

      func n -SuccRelStr -> strict RelStr means

      : Def6: the carrier of it = n & the InternalRel of it = { [i, (i + 1)] where i be Element of NAT : (i + 1) < n };

      existence

      proof

        set r = { [i, (i + 1)] where i be Element of NAT : (i + 1) < n };

        r c= [:n, n:]

        proof

          let x be object;

          assume x in r;

          then

          consider i be Element of NAT such that

           A1: x = [i, (i + 1)] and

           A2: (i + 1) < n;

          i <= (i + 1) by NAT_1: 11;

          then i < n by A2, XXREAL_0: 2;

          then

           A3: i in ( Segm n) by NAT_1: 44;

          (i + 1) in ( Segm n) by A2, NAT_1: 44;

          hence thesis by A1, A3, ZFMISC_1: 87;

        end;

        then

        reconsider r as Relation of n;

        take RelStr (# n, r #);

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: NECKLACE:15

    for n be Nat holds (n -SuccRelStr ) is asymmetric

    proof

      let n be Nat;

      set S = (n -SuccRelStr );

      the InternalRel of S is_asymmetric_in ( field the InternalRel of S)

      proof

        let x,y be object;

        assume that x in ( field the InternalRel of S) and y in ( field the InternalRel of S) and

         A1: [x, y] in the InternalRel of S;

        

         A2: [x, y] in { [i, (i + 1)] where i be Element of NAT : (i + 1) < n } by A1, Def6;

        assume [y, x] in the InternalRel of S;

        then [y, x] in { [i9, (i9 + 1)] where i9 be Element of NAT : (i9 + 1) < n } by Def6;

        then

        consider j be Element of NAT such that

         A3: [y, x] = [j, (j + 1)] and (j + 1) < n;

        

         A4: y = j & x = (j + 1) by A3, XTUPLE_0: 1;

        consider i be Element of NAT such that

         A5: [x, y] = [i, (i + 1)] and (i + 1) < n by A2;

        x = i & y = (i + 1) by A5, XTUPLE_0: 1;

        hence contradiction by A4;

      end;

      hence the InternalRel of S is asymmetric;

    end;

    theorem :: NECKLACE:16

    

     Th15: n > 0 implies ( card the InternalRel of (n -SuccRelStr )) = (n - 1)

    proof

      deffunc F( Element of NAT ) = [$1, ($1 + 1)];

      defpred P[ Element of NAT ] means ($1 + 1) < n;

      defpred Q[ set] means $1 in ( Segm (n -' 1));

      

       A1: (n -' 1) c= NAT ;

      assume

       A2: n > 0 ;

      then

       A3: n >= ( 0 + 1) by NAT_1: 13;

      

       A4: i in ( Segm (n -' 1)) implies (i + 1) < n

      proof

        assume i in ( Segm (n -' 1));

        then

         A5: i < (n -' 1) by NAT_1: 44;

        n >= ( 0 + 1) by A2, NAT_1: 13;

        then i < (n - 1) by A5, XREAL_1: 233;

        hence thesis by XREAL_1: 20;

      end;

      

       A6: for i be Element of NAT holds P[i] iff Q[i]

      proof

        let i be Element of NAT ;

        thus (i + 1) < n implies i in ( Segm (n -' 1))

        proof

          assume (i + 1) < n;

          then i < (n - 1) by XREAL_1: 20;

          then i < (n -' 1) by A3, XREAL_1: 233;

          hence thesis by NAT_1: 44;

        end;

        thus thesis by A4;

      end;

      

       A7: { F(i) where i be Element of NAT : P[i] } = { F(i) where i be Element of NAT : Q[i] } from FRAENKEL:sch 3( A6);

      deffunc F( Element of NAT ) = [$1, ($1 + 1)];

      

       A8: for d1,d2 be Element of NAT st F(d1) = F(d2) holds d1 = d2 by XTUPLE_0: 1;

      

       A9: ((n -' 1),{ F(i) where i be Element of NAT : i in (n -' 1) }) are_equipotent from FUNCT_7:sch 4( A1, A8);

      

      thus ( card the InternalRel of (n -SuccRelStr )) = ( card { [i, (i + 1)] where i be Element of NAT : (i + 1) < n }) by Def6

      .= ( card (n -' 1)) by A7, A9, CARD_1: 5

      .= (n -' 1)

      .= (n - 1) by A3, XREAL_1: 233;

    end;

    definition

      let R be RelStr;

      :: NECKLACE:def7

      func SymRelStr R -> strict RelStr means

      : Def7: the carrier of it = the carrier of R & the InternalRel of it = (the InternalRel of R \/ (the InternalRel of R ~ ));

      existence

      proof

        take RelStr (# the carrier of R, (the InternalRel of R \/ (the InternalRel of R ~ )) #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let R be RelStr;

      cluster ( SymRelStr R) -> symmetric;

      coherence

      proof

        let x,y be object;

        assume that x in the carrier of ( SymRelStr R) and y in the carrier of ( SymRelStr R) and

         A1: [x, y] in the InternalRel of ( SymRelStr R);

        

         A2: [x, y] in (the InternalRel of R \/ (the InternalRel of R ~ )) by A1, Def7;

        per cases by A2, XBOOLE_0:def 3;

          suppose [x, y] in the InternalRel of R;

          then [y, x] in (the InternalRel of R ~ ) by RELAT_1:def 7;

          then [y, x] in (the InternalRel of R \/ (the InternalRel of R ~ )) by XBOOLE_0:def 3;

          hence thesis by Def7;

        end;

          suppose [x, y] in (the InternalRel of R ~ );

          then [y, x] in the InternalRel of R by RELAT_1:def 7;

          then [y, x] in (the InternalRel of R \/ (the InternalRel of R ~ )) by XBOOLE_0:def 3;

          hence thesis by Def7;

        end;

      end;

    end

    registration

      cluster non empty symmetric for RelStr;

      existence

      proof

        set R = { [ 0 , 0 ]};

        R c= [: { 0 }, { 0 }:] by ZFMISC_1: 29;

        then

        reconsider R = { [ 0 , 0 ]} as Relation of { 0 };

        take S = RelStr (# { 0 }, R #);

        thus S is non empty;

        thus the InternalRel of S is_symmetric_in the carrier of S

        proof

          let x,y be object;

          assume that x in the carrier of S and y in the carrier of S and

           A1: [x, y] in the InternalRel of S;

          x = 0 & y = 0 by A1, ZFMISC_1: 28;

          then [y, x] in [: { 0 }, { 0 }:] by ZFMISC_1: 28;

          hence thesis by ZFMISC_1: 29;

        end;

      end;

    end

    registration

      let R be symmetric RelStr;

      cluster the InternalRel of R -> symmetric;

      coherence

      proof

        let x,y be object;

        assume

         A1: x in ( field the InternalRel of R) & y in ( field the InternalRel of R) & [x, y] in the InternalRel of R;

        the InternalRel of R is_symmetric_in the carrier of R & ( field the InternalRel of R) c= (the carrier of R \/ the carrier of R) by Def3, RELSET_1: 8;

        hence thesis by A1;

      end;

    end

    

     Lm1: for S,R be non empty RelStr holds (S,R) are_isomorphic implies ( card the InternalRel of S) = ( card the InternalRel of R)

    proof

      let S,R be non empty RelStr;

      set A = the carrier of S, B = the carrier of R, C = the InternalRel of S, D = the InternalRel of R;

      reconsider C as set;

      assume (S,R) are_isomorphic ;

      then

      consider f be Function of S, R such that

       A1: f is isomorphic;

      reconsider f9 = f as one-to-one Function by A1, WAYBEL_0:def 38;

      

       A2: [:f9, f9:] is one-to-one;

      

       A3: ( dom f) = A by FUNCT_2:def 1;

      

       A4: ( rng f) = B by A1, WAYBEL_0: 66;

      

       A5: f is monotone by A1, WAYBEL_0:def 38;

      (the InternalRel of S,the InternalRel of R) are_equipotent

      proof

        set P = [:f, f:];

        set F = ( [:f, f:] | C);

        set L = ( dom F);

        

         A6: ( dom F) = (( dom [:f, f:]) /\ C) by RELAT_1: 61

        .= ( [:( dom f), ( dom f):] /\ C) by FUNCT_3:def 8

        .= C by A3, XBOOLE_1: 28;

        

         A7: ( rng F) c= D

        proof

          let a be object;

          assume a in ( rng F);

          then

          consider x be object such that

           A8: x in ( dom F) and

           A9: a = (F . x) by FUNCT_1:def 3;

          consider x1,x2 be object such that

           A10: x = [x1, x2] by A8, RELAT_1:def 1;

          

           A11: x in ( dom [:f, f:]) by A8, RELAT_1: 57;

          then

          reconsider X1 = x1, X2 = x2 as Element of S by A10, ZFMISC_1: 87;

          X1 <= X2 by A8, A10, ORDERS_2:def 5;

          then

           A12: (f . X1) <= (f . X2) by A5;

          

           A13: a = (P . (x1,x2)) by A8, A9, A10, FUNCT_1: 47;

          x1 in ( dom f) & x2 in ( dom f) by A3, A10, A11, ZFMISC_1: 87;

          then a = [(f . x1), (f . x2)] by A13, FUNCT_3:def 8;

          hence thesis by A12, ORDERS_2:def 5;

        end;

        then

        reconsider F as Function of L, [:B, B:] by FUNCT_2: 2, XBOOLE_1: 1;

        reconsider F as Function of L, D by A7, FUNCT_2: 6;

        

         A14: ( rng F) = D

        proof

          thus ( rng F) c= D by A7;

          let x be object;

          assume

           A15: x in D;

          then

          consider x1,x2 be object such that

           A16: x = [x1, x2] by RELAT_1:def 1;

          reconsider x19 = x1, x29 = x2 as Element of B by A15, A16, ZFMISC_1: 87;

          x1 in B by A15, A16, ZFMISC_1: 87;

          then

          consider X1 be object such that

           A17: X1 in ( dom f) and

           A18: x1 = (f . X1) by A4, FUNCT_1:def 3;

          x2 in B by A15, A16, ZFMISC_1: 87;

          then

          consider X2 be object such that

           A19: X2 in ( dom f) and

           A20: x2 = (f . X2) by A4, FUNCT_1:def 3;

          reconsider X19 = X1, X29 = X2 as Element of S by A17, A19;

          x19 <= x29 by A15, A16, ORDERS_2:def 5;

          then X19 <= X29 by A1, A18, A20, WAYBEL_0: 66;

          then

           A21: [X1, X2] in C by ORDERS_2:def 5;

          set Pi = [X1, X2];

          Pi in [:( dom f), ( dom f):] by A17, A19, ZFMISC_1: 87;

          

          then x = ( [:f, f:] . (X1,X2)) by A16, A18, A20, FUNCT_3: 65

          .= (F . [X1, X2]) by A6, A21, FUNCT_1: 47;

          hence thesis by A6, A21, FUNCT_1:def 3;

        end;

        F is one-to-one by A2, FUNCT_1: 52;

        hence thesis by A6, A14, WELLORD2:def 4;

      end;

      hence thesis by CARD_1: 5;

    end;

    definition

      let R be RelStr;

      :: NECKLACE:def8

      func ComplRelStr R -> strict RelStr means

      : Def8: the carrier of it = the carrier of R & the InternalRel of it = ((the InternalRel of R ` ) \ ( id the carrier of R));

      existence

      proof

        reconsider r = ((the InternalRel of R ` ) \ ( id the carrier of R)) as Relation of the carrier of R;

        take RelStr (# the carrier of R, r #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let R be non empty RelStr;

      cluster ( ComplRelStr R) -> non empty;

      coherence

      proof

        the carrier of ( ComplRelStr R) = the carrier of R by Def8;

        hence the carrier of ( ComplRelStr R) is non empty;

      end;

    end

    theorem :: NECKLACE:17

    

     Th16: for S,R be RelStr holds (S,R) are_isomorphic implies ( card the InternalRel of S) = ( card the InternalRel of R)

    proof

      let S,R be RelStr;

      assume

       A1: (S,R) are_isomorphic ;

      then

       A2: ex f be Function of S, R st f is isomorphic;

      per cases by A2, WAYBEL_0:def 38;

        suppose S is non empty & R is non empty;

        hence thesis by A1, Lm1;

      end;

        suppose S is empty & R is empty;

        then

        reconsider S, R as empty RelStr;

        the InternalRel of S = {} & the InternalRel of R = {} ;

        hence thesis;

      end;

    end;

    begin

    definition

      let n be Nat;

      :: NECKLACE:def9

      func Necklace n -> strict RelStr equals ( SymRelStr (n -SuccRelStr ));

      coherence ;

    end

    registration

      let n be Nat;

      cluster ( Necklace n) -> symmetric;

      coherence ;

    end

    theorem :: NECKLACE:18

    

     Th17: the InternalRel of ( Necklace n) = ({ [i, (i + 1)] where i be Element of NAT : (i + 1) < n } \/ { [(i + 1), i] where i be Element of NAT : (i + 1) < n })

    proof

      set I = { [i, (i + 1)] where i be Element of NAT : (i + 1) < n };

      I is Relation-like

      proof

        let x be object;

        assume x in I;

        then ex i be Element of NAT st x = [i, (i + 1)] & (i + 1) < n;

        hence thesis;

      end;

      then

      reconsider I as Relation;

      set B = (n -SuccRelStr );

      deffunc F( Element of NAT ) = $1;

      deffunc G( Element of NAT ) = ($1 + 1);

      defpred P[ Element of NAT ] means ($1 + 1) < n;

      set R = { [ G(i), F(i)] where i be Element of NAT : P[i] };

      

       A1: I = { [ F(i), G(i)] where i be Element of NAT : P[i] };

      

       A2: (I ~ ) = R from Convers( A1);

      the InternalRel of B = I by Def6;

      hence thesis by A2, Def7;

    end;

    theorem :: NECKLACE:19

    

     Th18: for x be set holds x in the InternalRel of ( Necklace n) iff ex i be Element of NAT st (i + 1) < n & (x = [i, (i + 1)] or x = [(i + 1), i])

    proof

      let x be set;

      thus x in the InternalRel of ( Necklace n) implies ex i be Element of NAT st (i + 1) < n & (x = [i, (i + 1)] or x = [(i + 1), i])

      proof

        assume x in the InternalRel of ( Necklace n);

        then x in ({ [i, (i + 1)] where i be Element of NAT : (i + 1) < n } \/ { [(i + 1), i] where i be Element of NAT : (i + 1) < n }) by Th17;

        then x in { [i, (i + 1)] where i be Element of NAT : (i + 1) < n } or x in { [(i + 1), i] where i be Element of NAT : (i + 1) < n } by XBOOLE_0:def 3;

        then (ex i be Element of NAT st x = [i, (i + 1)] & (i + 1) < n) or ex i be Element of NAT st x = [(i + 1), i] & (i + 1) < n;

        hence thesis;

      end;

      thus (ex i be Element of NAT st (i + 1) < n & (x = [i, (i + 1)] or x = [(i + 1), i])) implies x in the InternalRel of ( Necklace n)

      proof

        given i be Element of NAT such that

         A1: (i + 1) < n & (x = [i, (i + 1)] or x = [(i + 1), i]);

        per cases by A1;

          suppose (i + 1) < n & x = [i, (i + 1)];

          then x in { [j, (j + 1)] where j be Element of NAT : (j + 1) < n };

          then x in ({ [j, (j + 1)] where j be Element of NAT : (j + 1) < n } \/ { [(j + 1), j] where j be Element of NAT : (j + 1) < n }) by XBOOLE_0:def 3;

          hence thesis by Th17;

        end;

          suppose (i + 1) < n & x = [(i + 1), i];

          then x in { [(j + 1), j] where j be Element of NAT : (j + 1) < n };

          then x in ({ [(j + 1), j] where j be Element of NAT : (j + 1) < n } \/ { [j, (j + 1)] where j be Element of NAT : (j + 1) < n }) by XBOOLE_0:def 3;

          hence thesis by Th17;

        end;

      end;

    end;

    registration

      let n be Nat;

      cluster ( Necklace n) -> irreflexive;

      coherence

      proof

        let x be set;

        set A = ( Necklace n);

        assume x in the carrier of A;

        

         A1: the InternalRel of ( Necklace n) = ({ [i, (i + 1)] where i be Element of NAT : (i + 1) < n } \/ { [(i + 1), i] where i be Element of NAT : (i + 1) < n }) by Th17;

        assume

         A2: [x, x] in the InternalRel of A;

        per cases by A2, A1, XBOOLE_0:def 3;

          suppose [x, x] in { [i, (i + 1)] where i be Element of NAT : (i + 1) < n };

          then

          consider i be Element of NAT such that

           A3: [x, x] = [i, (i + 1)] and (i + 1) < n;

          x = i & x = (i + 1) by A3, XTUPLE_0: 1;

          hence contradiction;

        end;

          suppose [x, x] in { [(i + 1), i] where i be Element of NAT : (i + 1) < n };

          then

          consider i be Element of NAT such that

           A4: [x, x] = [(i + 1), i] and (i + 1) < n;

          x = (i + 1) & x = i by A4, XTUPLE_0: 1;

          hence contradiction;

        end;

      end;

    end

    theorem :: NECKLACE:20

    

     Th19: for n be Nat holds the carrier of ( Necklace n) = n

    proof

      let n be Nat;

      the carrier of ( Necklace n) = the carrier of (n -SuccRelStr ) by Def7

      .= n by Def6;

      hence thesis;

    end;

    registration

      let n be non zero Nat;

      cluster ( Necklace n) -> non empty;

      coherence by Th19;

    end

    registration

      let n be Nat;

      cluster the carrier of ( Necklace n) -> finite;

      coherence by Th19;

    end

    theorem :: NECKLACE:21

    

     Th20: for n,i be Nat st (i + 1) < n holds [i, (i + 1)] in the InternalRel of ( Necklace n)

    proof

      let n,j be Nat such that

       A1: (j + 1) < n;

      reconsider j as Element of NAT by ORDINAL1:def 12;

      

       A2: [j, (j + 1)] in { [i, (i + 1)] where i be Element of NAT : (i + 1) < n } by A1;

      the InternalRel of ( Necklace n) = ({ [i, (i + 1)] where i be Element of NAT : (i + 1) < n } \/ { [(i + 1), i] where i be Element of NAT : (i + 1) < n }) by Th17;

      hence thesis by A2, XBOOLE_0:def 3;

    end;

    theorem :: NECKLACE:22

    

     Th21: for n be Nat, i be Nat st i in the carrier of ( Necklace n) holds i < n

    proof

      let n be Nat, i be Nat;

      assume i in the carrier of ( Necklace n);

      then i in ( Segm n) by Th19;

      hence thesis by NAT_1: 44;

    end;

    theorem :: NECKLACE:23

    for n be non zero Nat holds ( Necklace n) is connected

    proof

      let n be non zero Nat;

      given X,Y be Subset of ( Necklace n) such that

       A1: X <> {} and

       A2: Y <> {} and

       A3: ( [#] ( Necklace n)) = (X \/ Y) and

       A4: X misses Y and

       A5: the InternalRel of ( Necklace n) = ((the InternalRel of ( Necklace n) |_2 X) \/ (the InternalRel of ( Necklace n) |_2 Y));

      

       A6: the carrier of ( Necklace n) = n & 0 in n by Th3, Th19;

      per cases by A3, A6, XBOOLE_0:def 3;

        suppose

         A7: 0 in X;

        defpred P[ Nat] means $1 in Y;

        consider x be Element of ( Necklace n) such that

         A8: x in Y by A2, SUBSET_1: 4;

        x in the carrier of ( Necklace n);

        then x in ( Segm n) by Th19;

        then x is natural;

        then

         A9: ex x be Nat st P[x] by A8;

        consider k be Nat such that

         A10: P[k] and

         A11: for i be Nat st P[i] holds k <= i from NAT_1:sch 5( A9);

        k <> 0 by A4, A7, A10, XBOOLE_0: 3;

        then

        consider i be Nat such that

         A12: k = (i + 1) by NAT_1: 6;

        reconsider i as Element of NAT by ORDINAL1:def 12;

        

         A13: not i in Y by A11, A12, XREAL_1: 29;

        

         A14: not (i + 1) in X by A4, A10, A12, XBOOLE_0: 3;

        

         A15: [i, (i + 1)] in the InternalRel of ( Necklace n) by A10, A12, Th20, Th21;

        now

          per cases by A5, A15, XBOOLE_0:def 3;

            suppose [i, (i + 1)] in (the InternalRel of ( Necklace n) |_2 X);

            then [i, (i + 1)] in [:X, X:] by XBOOLE_0:def 4;

            hence contradiction by A14, ZFMISC_1: 87;

          end;

            suppose [i, (i + 1)] in (the InternalRel of ( Necklace n) |_2 Y);

            then [i, (i + 1)] in [:Y, Y:] by XBOOLE_0:def 4;

            hence contradiction by A13, ZFMISC_1: 87;

          end;

        end;

        hence contradiction;

      end;

        suppose

         A16: 0 in Y;

        defpred P[ Nat] means $1 in X;

        consider y be Element of ( Necklace n) such that

         A17: y in X by A1, SUBSET_1: 4;

        y in the carrier of ( Necklace n);

        then y in ( Segm n) by Th19;

        then y is natural;

        then

         A18: ex y be Nat st P[y] by A17;

        consider k be Nat such that

         A19: P[k] and

         A20: for i be Nat st P[i] holds k <= i from NAT_1:sch 5( A18);

        k <> 0 by A4, A16, A19, XBOOLE_0: 3;

        then

        consider i be Nat such that

         A21: k = (i + 1) by NAT_1: 6;

        reconsider i as Element of NAT by ORDINAL1:def 12;

        

         A22: not i in X by A20, A21, XREAL_1: 29;

        

         A23: not (i + 1) in Y by A4, A19, A21, XBOOLE_0: 3;

        

         A24: [i, (i + 1)] in the InternalRel of ( Necklace n) by A19, A21, Th20, Th21;

        now

          per cases by A5, A24, XBOOLE_0:def 3;

            suppose [i, (i + 1)] in (the InternalRel of ( Necklace n) |_2 Y);

            then [i, (i + 1)] in [:Y, Y:] by XBOOLE_0:def 4;

            hence contradiction by A23, ZFMISC_1: 87;

          end;

            suppose [i, (i + 1)] in (the InternalRel of ( Necklace n) |_2 X);

            then [i, (i + 1)] in [:X, X:] by XBOOLE_0:def 4;

            hence contradiction by A22, ZFMISC_1: 87;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: NECKLACE:24

    

     Th23: for i,j be Nat st [i, j] in the InternalRel of ( Necklace n) holds i = (j + 1) or j = (i + 1)

    proof

      let i,j be Nat;

      assume [i, j] in the InternalRel of ( Necklace n);

      then [i, j] in ({ [k, (k + 1)] where k be Element of NAT : (k + 1) < n } \/ { [(l + 1), l] where l be Element of NAT : (l + 1) < n }) by Th17;

      then

       A1: [i, j] in { [k, (k + 1)] where k be Element of NAT : (k + 1) < n } or [i, j] in { [(k + 1), k] where k be Element of NAT : (k + 1) < n } by XBOOLE_0:def 3;

      (i + 1) = j or (j + 1) = i

      proof

        per cases by A1;

          suppose ex k be Element of NAT st [i, j] = [k, (k + 1)] & (k + 1) < n;

          then

          consider k such that

           A2: [i, j] = [k, (k + 1)] and (k + 1) < n;

          i = k by A2, XTUPLE_0: 1;

          hence thesis by A2, XTUPLE_0: 1;

        end;

          suppose ex k be Element of NAT st [i, j] = [(k + 1), k] & (k + 1) < n;

          then

          consider k such that

           A3: [i, j] = [(k + 1), k] and (k + 1) < n;

          i = (k + 1) by A3, XTUPLE_0: 1;

          hence thesis by A3, XTUPLE_0: 1;

        end;

      end;

      hence thesis;

    end;

    theorem :: NECKLACE:25

    

     Th24: for i,j be Nat st (i = (j + 1) or j = (i + 1)) & i in the carrier of ( Necklace n) & j in the carrier of ( Necklace n) holds [i, j] in the InternalRel of ( Necklace n)

    proof

      let i,j be Nat such that

       A1: i = (j + 1) or j = (i + 1) and

       A2: i in the carrier of ( Necklace n) and

       A3: j in the carrier of ( Necklace n);

      per cases by A1;

        suppose

         A4: i = (j + 1);

        then [j, (j + 1)] in the InternalRel of ( Necklace n) by A2, Th20, Th21;

        then [(j + 1), j] in (the InternalRel of ( Necklace n) ~ ) by RELAT_1:def 7;

        hence thesis by A4, RELAT_2: 13;

      end;

        suppose j = (i + 1);

        hence thesis by A3, Th20, Th21;

      end;

    end;

    theorem :: NECKLACE:26

    

     Th25: n > 0 implies ( card { [(i + 1), i] where i be Element of NAT : (i + 1) < n }) = (n - 1)

    proof

      deffunc F( Element of NAT ) = [($1 + 1), $1];

      defpred P[ Element of NAT ] means ($1 + 1) < n;

      defpred Q[ Element of NAT ] means $1 in ( Segm (n -' 1));

      

       A1: for d1,d2 be Element of NAT st F(d1) = F(d2) holds d1 = d2 by XTUPLE_0: 1;

      assume

       A2: n > 0 ;

      then

       A3: n >= ( 0 + 1) by NAT_1: 13;

      

       A4: i in ( Segm (n -' 1)) implies (i + 1) < n

      proof

        assume i in ( Segm (n -' 1));

        then

         A5: i < (n -' 1) by NAT_1: 44;

        n >= ( 0 + 1) by A2, NAT_1: 13;

        then i < (n - 1) by A5, XREAL_1: 233;

        hence thesis by XREAL_1: 20;

      end;

      

       A6: for i be Element of NAT holds P[i] iff Q[i]

      proof

        let i be Element of NAT ;

        thus (i + 1) < n implies i in ( Segm (n -' 1))

        proof

          assume (i + 1) < n;

          then i < (n - 1) by XREAL_1: 20;

          then i < (n -' 1) by A3, XREAL_1: 233;

          hence thesis by NAT_1: 44;

        end;

        thus thesis by A4;

      end;

      

       A7: { F(i) where i be Element of NAT : P[i] } = { F(i) where i be Element of NAT : Q[i] } from FRAENKEL:sch 3( A6);

      

       A8: (n -' 1) c= NAT ;

      ((n -' 1),{ F(i) where i be Element of NAT : i in (n -' 1) }) are_equipotent from FUNCT_7:sch 4( A8, A1);

      

      hence ( card { [(i + 1), i] where i be Element of NAT : (i + 1) < n }) = ( card (n -' 1)) by A7, CARD_1: 5

      .= (n -' 1)

      .= (n - 1) by A3, XREAL_1: 233;

    end;

    theorem :: NECKLACE:27

    

     Th26: n > 0 implies ( card the InternalRel of ( Necklace n)) = (2 * (n - 1))

    proof

      deffunc G( Element of NAT ) = ($1 + 1);

      deffunc F( Element of NAT ) = $1;

      defpred P[ Element of NAT ] means ($1 + 1) < n;

      set A = { [i, (i + 1)] where i be Element of NAT : (i + 1) < n }, B = { [ G(i), F(i)] where i be Element of NAT : P[i] };

      

       A1: A is Relation-like

      proof

        let x be object;

        assume x in A;

        then ex i be Element of NAT st x = [i, (i + 1)] & (i + 1) < n;

        hence thesis;

      end;

      

       A2: the InternalRel of ( Necklace n) = (A \/ B) by Th17;

      assume

       A3: n > 0 ;

      then n >= ( 0 + 1) by NAT_1: 13;

      then

       A4: (n -' 1) = (n - 1) by XREAL_1: 233;

      A = the InternalRel of (n -SuccRelStr ) by Def6;

      then

       A5: ( card A) = (n - 1) by A3, Th15;

      reconsider A as Relation by A1;

      

       A6: A = { [ F(i), G(i)] where i be Element of NAT : P[i] };

      

       A7: (A ~ ) = B from Convers( A6);

      

       A8: A misses B

      proof

        assume A meets B;

        then

        consider x be object such that

         A9: x in A and

         A10: x in B by XBOOLE_0: 3;

        consider y,z be object such that

         A11: x = [y, z] by A9, RELAT_1:def 1;

         [z, y] in A by A7, A10, A11, RELAT_1:def 7;

        then

        consider j be Element of NAT such that

         A12: [z, y] = [j, (j + 1)] and (j + 1) < n;

        

         A13: z = j & y = (j + 1) by A12, XTUPLE_0: 1;

        consider i be Element of NAT such that

         A14: [y, z] = [i, (i + 1)] and (i + 1) < n by A9, A11;

        y = i & z = (i + 1) by A14, XTUPLE_0: 1;

        hence contradiction by A13;

      end;

      ( card B) = (n - 1) by A3, Th25;

      

      then ( card the InternalRel of ( Necklace n)) = (( card (n - 1)) +` ( card (n - 1))) by A2, A5, A8, CARD_2: 35

      .= ( card ((n -' 1) + (n -' 1))) by A4, CARD_2: 38

      .= (2 * (n - 1)) by A4;

      hence thesis;

    end;

    theorem :: NECKLACE:28

    (( Necklace 1),( ComplRelStr ( Necklace 1))) are_isomorphic

    proof

      set f = ( 0 .--> 0 );

      set S = ( Necklace 1), T = ( ComplRelStr S);

      

       A1: the carrier of S = the carrier of T by Def8;

      

       A2: the carrier of S = { 0 } by Th19, CARD_1: 49;

      then ( dom f) = the carrier of S & ( rng f) c= the carrier of T by A1, FUNCOP_1: 13;

      then f is Relation of the carrier of S, the carrier of T by RELSET_1: 4;

      then

      reconsider g = f as Function of S, T by A2;

      

       A3: ( rng g) = { 0 } by FUNCOP_1: 8;

      for y,x be object holds y in ( rng g) & x = (g . y) iff x in ( dom g) & y = (g . x)

      proof

        let x,y be object;

        

         A5: x in ( dom g) & y = (g . x) implies y in ( rng g) & x = (g . y)

        proof

          assume that

           A6: x in ( dom g) and

           A7: y = (g . x);

          

           A8: x = 0 by A6, TARSKI:def 1;

          y = 0 by A7;

          hence thesis by A3, A8, TARSKI:def 1;

        end;

        y in ( rng g) & x = (g . y) implies x in ( dom g) & y = (g . x)

        proof

          assume that

           A9: y in ( rng g) and

           A10: x = (g . y);

          

           A11: y = 0 by A3, A9, TARSKI:def 1;

          x = 0 by A10;

          hence thesis by A11, TARSKI:def 1;

        end;

        hence thesis by A3, A5;

      end;

      then

      reconsider h = (g " ) as Function of T, S by A1, A3, FUNCT_1: 32;

      

       A12: h is monotone

      proof

        let x,y be Element of T;

        assume x <= y;

        then [x, y] in the InternalRel of T by ORDERS_2:def 5;

        then [x, y] in ((the InternalRel of S ` ) \ ( id the carrier of S)) by Def8;

        then not [x, y] in ( id the carrier of S) by XBOOLE_0:def 5;

        then

         A13: not x in the carrier of S or x <> y by RELAT_1:def 10;

        let a,b be Element of S such that a = (h . x) and b = (h . y);

        

         A14: x in the carrier of T;

        

         A15: the carrier of T = ( Segm 1) by A1, Th19;

        then x in ( Segm 1) & y in ( Segm 1);

        then

        reconsider i = x, j = y as Nat;

        

         A16: j = 0 by A15, CARD_1: 49, TARSKI:def 1;

        

         A17: i = 0 by A15, CARD_1: 49, TARSKI:def 1;

        

         A18: (i + 1) <> j & (j + 1) <> i & i <> j

        proof

          hereby

            assume

             A19: (i + 1) = j or (j + 1) = i;

            per cases by A19;

              suppose (i + 1) = j;

              hence contradiction by A15, A17, NAT_1: 44;

            end;

              suppose (j + 1) = i;

              hence contradiction by A15, A16, NAT_1: 44;

            end;

          end;

          thus thesis by A13, A14, Def8;

        end;

        

         A20: y = 0 by A15, CARD_1: 49, TARSKI:def 1;

        the carrier of T = { 0 } by A1, Th19, CARD_1: 49;

        hence thesis by A18, A20, TARSKI:def 1;

      end;

      g is monotone

      proof

        let x,y be Element of S;

        assume x <= y;

        then

         A21: [x, y] in the InternalRel of S by ORDERS_2:def 5;

        the carrier of S = ( Segm 1) by Th19;

        then x in ( Segm 1) & y in ( Segm 1);

        then

        reconsider i = x, j = y as Nat;

        let a,b be Element of T such that a = (g . x) and b = (g . y);

        the carrier of S = { 0 } by Th19, CARD_1: 49;

        then

         A22: x = 0 & y = 0 by TARSKI:def 1;

        i = (j + 1) or j = (i + 1) by A21, Th23;

        hence thesis by A22;

      end;

      then g is isomorphic by A12, WAYBEL_0:def 38;

      hence thesis;

    end;

    theorem :: NECKLACE:29

    (( Necklace 4),( ComplRelStr ( Necklace 4))) are_isomorphic

    proof

      set g = (( 0 ,1) --> (1,3)), h = ((2,3) --> ( 0 ,2)), f = (g +* h);

      set S = ( Necklace 4), T = ( ComplRelStr ( Necklace 4));

      

       A1: ( rng h) = { 0 , 2} by FUNCT_4: 64;

      

       A2: ( rng g) = {1, 3} by FUNCT_4: 64;

      

       A3: ( rng f) c= the carrier of T

      proof

        let x be object;

        assume

         A4: x in ( rng f);

        

         A5: ( rng f) c= (( rng g) \/ ( rng h)) by FUNCT_4: 17;

        (( rng g) \/ ( rng h)) = {1, 3, 0 , 2} by A2, A1, ENUMSET1: 5

        .= { 0 , 1, 2, 3} by ENUMSET1: 69;

        then x in 4 by A4, A5, CARD_1: 52;

        then x in the carrier of S by Th19;

        hence thesis by Def8;

      end;

      

       A6: ( dom f) = (( dom (( 0 ,1) --> (1,3))) \/ ( dom ((2,3) --> ( 0 ,2)))) by FUNCT_4:def 1

      .= ( { 0 , 1} \/ ( dom ((2,3) --> ( 0 ,2)))) by FUNCT_4: 62

      .= ( { 0 , 1} \/ {2, 3}) by FUNCT_4: 62

      .= { 0 , 1, 2, 3} by ENUMSET1: 5;

      then

       A7: ( dom f) = the carrier of S by Th19, CARD_1: 52;

      then

      reconsider f as Function of S, T by A3, FUNCT_2:def 1, RELSET_1: 4;

      take f;

      per cases ;

        case that S is non empty and T is non empty;

        set A = the InternalRel of T;

        

         A8: ( rng ( 0 .--> 1)) misses ( rng (1 .--> 3))

        proof

          assume ( rng ( 0 .--> 1)) meets ( rng (1 .--> 3));

          then

          consider x be object such that

           A9: x in ( rng ( 0 .--> 1)) and

           A10: x in ( rng (1 .--> 3)) by XBOOLE_0: 3;

          ( rng ( 0 .--> 1)) = {1} by FUNCOP_1: 8;

          then ( rng (1 .--> 3)) = {3} & x = 1 by A9, FUNCOP_1: 8, TARSKI:def 1;

          hence contradiction by A10, TARSKI:def 1;

        end;

        

         A11: ( rng g) misses ( rng h)

        proof

          assume ( rng g) meets ( rng h);

          then

          consider x be object such that

           A12: x in ( rng g) and

           A13: x in ( rng h) by XBOOLE_0: 3;

          x = 1 or x = 3 by A2, A12, TARSKI:def 2;

          hence contradiction by A1, A13, TARSKI:def 2;

        end;

        set B = { [1, 3], [3, 1], [ 0 , 2], [2, 0 ], [ 0 , 3], [3, 0 ]};

        

         A14: ( rng (2 .--> 0 )) misses ( rng (3 .--> 2))

        proof

          assume ( rng (2 .--> 0 )) meets ( rng (3 .--> 2));

          then

          consider x be object such that

           A15: x in ( rng (2 .--> 0 )) and

           A16: x in ( rng (3 .--> 2)) by XBOOLE_0: 3;

          ( rng (2 .--> 0 )) = { 0 } by FUNCOP_1: 8;

          then ( rng (3 .--> 2)) = {2} & x = 0 by A15, FUNCOP_1: 8, TARSKI:def 1;

          hence contradiction by A16, TARSKI:def 1;

        end;

        h = ((2 .--> 0 ) +* (3 .--> 2)) by FUNCT_4:def 4;

        then

         A17: h is one-to-one by A14, FUNCT_4: 92;

        

         A18: ( dom g) misses ( dom h)

        proof

          assume ( dom g) meets ( dom h);

          then

          consider x be object such that

           A19: x in ( dom g) and

           A20: x in ( dom h) by XBOOLE_0: 3;

          x = 0 or x = 1 by A19, TARSKI:def 2;

          hence contradiction by A20, TARSKI:def 2;

        end;

        

        then

         A21: ( rng f) = (( rng g) \/ ( rng h)) by FRECHET: 35, PARTFUN1: 56

        .= {1, 3, 0 , 2} by A2, A1, ENUMSET1: 5

        .= { 0 , 1, 2, 3} by ENUMSET1: 69

        .= the carrier of S by Th19, CARD_1: 52

        .= the carrier of T by Def8;

        g = (( 0 .--> 1) +* (1 .--> 3)) by FUNCT_4:def 4;

        then

         A22: g is one-to-one by A8, FUNCT_4: 92;

        hence f is one-to-one by A17, A11, FUNCT_4: 92;

        then

        reconsider F = (f " ) as Function of T, S by A21, FUNCT_2: 25;

        

         A23: B c= A

        proof

          set C = the carrier of S;

          let x be object;

          assume x in B;

          then

           A24: x = [1, 3] or x = [3, 1] or x = [ 0 , 2] or x = [2, 0 ] or x = [ 0 , 3] or x = [3, 0 ] by ENUMSET1:def 4;

          

           A25: 2 in C & 3 in C by A6, A7, ENUMSET1:def 2;

           0 in C & 1 in C by A6, A7, ENUMSET1:def 2;

          then

          reconsider x9 = x as Element of [:C, C:] by A24, A25, ZFMISC_1: 87;

           not x9 in the InternalRel of S

          proof

            assume x9 in the InternalRel of S;

            then

            consider i be Element of NAT such that (i + 1) < 4 and

             A26: x9 = [i, (i + 1)] or x9 = [(i + 1), i] by Th18;

            i = 1 & (i + 1) = 3 or i = 3 & (i + 1) = 1 or i = 0 & (i + 1) = 2 or i = 2 & (i + 1) = 0 or i = 0 & (i + 1) = 3 or i = 3 & (i + 1) = 0 by A24, A26, XTUPLE_0: 1;

            hence contradiction;

          end;

          then

           A27: x9 in (the InternalRel of S ` ) by SUBSET_1: 29;

           not x in ( id the carrier of S) by A24, RELAT_1:def 10;

          then x in ((the InternalRel of S ` ) \ ( id the carrier of S)) by A27, XBOOLE_0:def 5;

          hence thesis by Def8;

        end;

        thus f is monotone

        proof

          

           A28: ( dom h) = {2, 3} by FUNCT_4: 62;

          then 2 in ( dom h) by TARSKI:def 2;

          

          then

           A29: (f . 2) = (h . 2) by FUNCT_4: 13

          .= 0 by FUNCT_4: 63;

          3 in ( dom h) by A28, TARSKI:def 2;

          

          then

           A30: (f . 3) = (h . 3) by FUNCT_4: 13

          .= 2 by FUNCT_4: 63;

          

           A31: ( dom g) = { 0 , 1} by FUNCT_4: 62;

          then 0 in ( dom g) by TARSKI:def 2;

          

          then

           A32: (f . 0 ) = (g . 0 ) by A18, FUNCT_4: 16

          .= 1 by FUNCT_4: 63;

          1 in ( dom g) by A31, TARSKI:def 2;

          

          then

           A33: (f . 1) = (g . 1) by A18, FUNCT_4: 16

          .= 3 by FUNCT_4: 63;

          let x,y be Element of S;

          assume x <= y;

          then

           A34: [x, y] in the InternalRel of S by ORDERS_2:def 5;

          the carrier of S = 4 by Th19;

          then x in ( Segm 4) & y in ( Segm 4);

          then

          reconsider i = x, j = y as Nat;

          

           A35: i = (j + 1) or j = (i + 1) by A34, Th23;

          let a,b be Element of T such that

           A36: a = (f . x) & b = (f . y);

          per cases by A6, A7, ENUMSET1:def 2;

            suppose x = 0 & y = 0 ;

            hence thesis by A35;

          end;

            suppose x = 0 & y = 1;

            then [a, b] in B by A36, A32, A33, ENUMSET1:def 4;

            hence thesis by A23, ORDERS_2:def 5;

          end;

            suppose x = 0 & y = 2;

            hence thesis by A35;

          end;

            suppose x = 0 & y = 3;

            hence thesis by A35;

          end;

            suppose x = 1 & y = 0 ;

            then [a, b] in B by A36, A32, A33, ENUMSET1:def 4;

            hence thesis by A23, ORDERS_2:def 5;

          end;

            suppose x = 1 & y = 1;

            hence thesis by A35;

          end;

            suppose x = 1 & y = 2;

            then [a, b] in B by A36, A33, A29, ENUMSET1:def 4;

            hence thesis by A23, ORDERS_2:def 5;

          end;

            suppose x = 1 & y = 3;

            hence thesis by A35;

          end;

            suppose x = 2 & y = 0 ;

            hence thesis by A35;

          end;

            suppose x = 2 & y = 1;

            then [a, b] in B by A36, A33, A29, ENUMSET1:def 4;

            hence thesis by A23, ORDERS_2:def 5;

          end;

            suppose x = 2 & y = 2;

            hence thesis by A35;

          end;

            suppose x = 2 & y = 3;

            then [a, b] in B by A36, A29, A30, ENUMSET1:def 4;

            hence thesis by A23, ORDERS_2:def 5;

          end;

            suppose x = 3 & y = 0 ;

            hence thesis by A35;

          end;

            suppose x = 3 & y = 1;

            hence thesis by A35;

          end;

            suppose x = 3 & y = 2;

            then [a, b] in B by A36, A29, A30, ENUMSET1:def 4;

            hence thesis by A23, ORDERS_2:def 5;

          end;

            suppose x = 3 & y = 3;

            hence thesis by A35;

          end;

        end;

        take F;

        thus F = (f " );

        thus F is monotone

        proof

          let x,y be Element of T;

          assume x <= y;

          then [x, y] in the InternalRel of T by ORDERS_2:def 5;

          then

           A37: [x, y] in ((the InternalRel of S ` ) \ ( id the carrier of S)) by Def8;

          then not [x, y] in ( id the carrier of S) by XBOOLE_0:def 5;

          then

           A38: not x in the carrier of S or x <> y by RELAT_1:def 10;

           [x, y] in (the InternalRel of S ` ) implies not [x, y] in the InternalRel of S by XBOOLE_0:def 5;

          then

           A39: not [x, y] in ({ [k, (k + 1)] where k be Element of NAT : (k + 1) < 4 } \/ { [(l + 1), l] where l be Element of NAT : (l + 1) < 4 }) by A37, Th17, XBOOLE_0:def 5;

          then

           A40: not [x, y] in { [(k + 1), k] where k be Element of NAT : (k + 1) < 4 } by XBOOLE_0:def 3;

          

           A41: the carrier of T = the carrier of S by Def8

          .= ( Segm 4) by Th19;

          then x in ( Segm 4) & y in ( Segm 4);

          then x is natural & y is natural;

          then

          reconsider i = x, j = y as Element of NAT by ORDINAL1:def 12;

          

           A42: x in the carrier of T;

          

           A43: not [x, y] in { [k, (k + 1)] where k be Element of NAT : (k + 1) < 4 } by A39, XBOOLE_0:def 3;

          

           A44: (i + 1) <> j & (j + 1) <> i & i <> j

          proof

            hereby

              assume

               A45: (i + 1) = j or (j + 1) = i;

              per cases by A45;

                suppose

                 A46: (i + 1) = j;

                then (i + 1) < 4 by A41, NAT_1: 44;

                hence contradiction by A43, A46;

              end;

                suppose

                 A47: (j + 1) = i;

                then (j + 1) < 4 by A41, NAT_1: 44;

                hence contradiction by A40, A47;

              end;

            end;

            thus thesis by A38, A42, Def8;

          end;

          

           A48: (h " ) = (( 0 ,2) --> (2,3)) by Th9;

          then

           A49: ( dom (h " )) = { 0 , 2} by FUNCT_4: 62;

          then

           A50: 0 in ( dom (h " )) by TARSKI:def 2;

          

           A51: (F . 0 ) = (((g " ) +* (h " )) . 0 ) by A22, A17, A18, A11, Th6

          .= ((h " ) . 0 ) by A50, FUNCT_4: 13

          .= 2 by A48, FUNCT_4: 63;

          

           A52: (g " ) = ((1,3) --> ( 0 ,1)) by Th9;

          then

           A53: ( dom (g " )) = {1, 3} by FUNCT_4: 62;

          then

           A54: 1 in ( dom (g " )) by TARSKI:def 2;

          

           A55: ( dom (g " )) misses ( dom (h " ))

          proof

            assume ( dom (g " )) meets ( dom (h " ));

            then

            consider x be object such that

             A56: x in ( dom (g " )) and

             A57: x in ( dom (h " )) by XBOOLE_0: 3;

            x = 1 or x = 3 by A53, A56, TARSKI:def 2;

            hence contradiction by A49, A57, TARSKI:def 2;

          end;

          

           A58: (F . 1) = (((g " ) +* (h " )) . 1) by A22, A17, A18, A11, Th6

          .= ((g " ) . 1) by A55, A54, FUNCT_4: 16

          .= 0 by A52, FUNCT_4: 63;

          

           A59: 2 in ( dom (h " )) by A49, TARSKI:def 2;

          

           A60: (F . 2) = (((g " ) +* (h " )) . 2) by A22, A17, A18, A11, Th6

          .= ((h " ) . 2) by A59, FUNCT_4: 13

          .= 3 by A48, FUNCT_4: 63;

          

           A61: 3 in ( dom (g " )) by A53, TARSKI:def 2;

          

           A62: (F . 3) = (((g " ) +* (h " )) . 3) by A22, A17, A18, A11, Th6

          .= ((g " ) . 3) by A55, A61, FUNCT_4: 16

          .= 1 by A52, FUNCT_4: 63;

          let a,b be Element of S such that

           A63: a = (F . x) and

           A64: b = (F . y);

          per cases by A41, CARD_1: 52, ENUMSET1:def 2;

            suppose x = 0 & y = 0 ;

            hence thesis by A44;

          end;

            suppose x = 0 & y = 1;

            hence thesis by A44;

          end;

            suppose

             A65: x = 0 & y = 2;

            then b = (2 + 1) by A64, A60;

            then [a, b] in the InternalRel of S by A63, A51, A65, Th24;

            hence thesis by ORDERS_2:def 5;

          end;

            suppose

             A66: x = 0 & y = 3;

            then a = (1 + 1) by A63, A51;

            then [a, b] in the InternalRel of S by A64, A62, A66, Th24;

            hence thesis by ORDERS_2:def 5;

          end;

            suppose x = 1 & y = 0 ;

            hence thesis by A44;

          end;

            suppose x = 1 & y = 1;

            hence thesis by A44;

          end;

            suppose x = 1 & y = 2;

            hence thesis by A44;

          end;

            suppose

             A67: x = 1 & y = 3;

            then b = ( 0 + 1) by A64, A62;

            then [a, b] in the InternalRel of S by A63, A58, A67, Th24;

            hence thesis by ORDERS_2:def 5;

          end;

            suppose

             A68: x = 2 & y = 0 ;

            then a = (2 + 1) by A63, A60;

            then [a, b] in the InternalRel of S by A64, A51, A68, Th24;

            hence thesis by ORDERS_2:def 5;

          end;

            suppose x = 2 & y = 1;

            hence thesis by A44;

          end;

            suppose x = 2 & y = 2;

            hence thesis by A44;

          end;

            suppose x = 2 & y = 3;

            hence thesis by A44;

          end;

            suppose

             A69: x = 3 & y = 0 ;

            then b = (1 + 1) by A64, A51;

            then [a, b] in the InternalRel of S by A63, A62, A69, Th24;

            hence thesis by ORDERS_2:def 5;

          end;

            suppose

             A70: x = 3 & y = 1;

            then a = ( 0 + 1) by A63, A62;

            then [a, b] in the InternalRel of S by A64, A58, A70, Th24;

            hence thesis by ORDERS_2:def 5;

          end;

            suppose x = 3 & y = 2;

            hence thesis by A44;

          end;

            suppose x = 3 & y = 3;

            hence thesis by A44;

          end;

        end;

      end;

        case S is empty or T is empty;

        hence thesis;

      end;

    end;

    theorem :: NECKLACE:30

    (( Necklace n),( ComplRelStr ( Necklace n))) are_isomorphic implies n = 0 or n = 1 or n = 4

    proof

      assume

       A1: (( Necklace n),( ComplRelStr ( Necklace n))) are_isomorphic ;

      set S = ( Necklace n), T = ( ComplRelStr S);

      ( card n) = n;

      then

       A2: ( card [:n, n:]) = (n * n) by CARD_2: 46;

      assume

       A3: not thesis;

      n <= 4 implies n = 0 or ... or n = 4;

      then n = 2 or n = 3 or n > 4 by A3;

      then

       A4: ( card the InternalRel of S) = (2 * (n - 1)) by Th26;

      

       A5: (((n * n) - (2 * (n - 1))) - n) <> (2 * (n - 1))

      proof

        

         A6: ( delta (1,( - 5),4)) = ((( - 5) ^2 ) - ((4 * 1) * 4)) by QUIN_1:def 1

        .= 9;

        assume not thesis;

        then (((1 * (n ^2 )) + (( - 5) * n)) + 4) = 0 ;

        then n = ((( - ( - 5)) - ( sqrt ( delta (1,( - 5),4)))) / (2 * 1)) or n = ((( - ( - 5)) + ( sqrt ( delta (1,( - 5),4)))) / (2 * 1)) by A6, QUIN_1: 15;

        then n = ((5 - ( sqrt (3 ^2 ))) / 2) or n = ((5 + ( sqrt (3 ^2 ))) / 2) by A6;

        then

         A7: n = ((5 - 3) / 2) or n = ((5 + 3) / 2) by SQUARE_1: 22;

        per cases by A7;

          suppose n = 1;

          hence contradiction by A3;

        end;

          suppose n = 4;

          hence contradiction by A3;

        end;

      end;

      

       A8: ( id the carrier of S) misses the InternalRel of S

      proof

        assume not thesis;

        then

        consider x be object such that

         A9: x in ( id the carrier of S) and

         A10: x in the InternalRel of S by XBOOLE_0: 3;

        consider i be Element of NAT such that (i + 1) < n and

         A11: x = [i, (i + 1)] or x = [(i + 1), i] by A10, Th18;

        consider x1,x2 be object such that

         A12: x = [x1, x2] by A9, RELAT_1:def 1;

        

         A13: x1 = x2 by A9, A12, RELAT_1:def 10;

        per cases by A12, A11;

          suppose [x1, x2] = [i, (i + 1)];

          then x1 = i & x2 = (i + 1) by XTUPLE_0: 1;

          hence thesis by A13;

        end;

          suppose [x1, x2] = [(i + 1), i];

          then x1 = (i + 1) & x2 = i by XTUPLE_0: 1;

          hence thesis by A13;

        end;

      end;

      the carrier of S = n by Th19;

      then

       A14: ( card (the InternalRel of S ` )) = ((n * n) - (2 * (n - 1))) by A4, A2, CARD_2: 44;

      the carrier of S = n & n = ( card n) by Th19;

      then

       A15: ( card ( id the carrier of S)) = n by Th4;

      ( card the InternalRel of T) = ( card ((the InternalRel of S ` ) \ ( id the carrier of S))) by Def8

      .= (((n * n) - (2 * (n - 1))) - n) by A14, A15, A8, CARD_2: 44, XBOOLE_1: 86;

      hence thesis by A1, A4, A5, Th16;

    end;