neckla_2.miz



    begin

    reserve U for Universe;

    theorem :: NECKLA_2:1

    

     Th1: for X,Y be set st X in U & Y in U holds for R be Relation of X, Y holds R in U

    proof

      let X,Y be set;

      assume that

       A1: X in U and

       A2: Y in U;

       [:X, Y:] in U by A1, A2, CLASSES2: 61;

      hence thesis by CLASSES1:def 1;

    end;

    theorem :: NECKLA_2:2

    

     Th2: the InternalRel of ( Necklace 4) = { [ 0 , 1], [1, 0 ], [1, 2], [2, 1], [2, 3], [3, 2]}

    proof

      set A = { [ 0 , 1], [1, 0 ], [1, 2], [2, 1], [2, 3], [3, 2]}, B = the InternalRel of ( Necklace 4);

      

       A1: [( 0 + 1), 0 ] in { [(i + 1), i] where i be Element of NAT : (i + 1) < 4 };

      

       A2: B = ({ [i, (i + 1)] where i be Element of NAT : (i + 1) < 4 } \/ { [(i + 1), i] where i be Element of NAT : (i + 1) < 4 }) by NECKLACE: 18;

      

       A3: B c= A

      proof

        let x be object;

        assume

         A4: x in B;

        then

        consider y,z be object such that

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

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

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

          then

          consider i be Element of NAT such that

           A6: [y, z] = [i, (i + 1)] and

           A7: (i + 1) < 4 by A5;

          

           A8: y = i by A6, XTUPLE_0: 1;

          (i + 1) < (1 + 3) by A7;

          then i < (2 + 1) by XREAL_1: 7;

          then i <= 2 by NAT_1: 13;

          then y = 0 or ... or y = 2 by A8;

          hence thesis by A5, A6, A8, ENUMSET1:def 4;

        end;

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

          then

          consider i be Element of NAT such that

           A9: [y, z] = [(i + 1), i] and

           A10: (i + 1) < 4 by A5;

          

           A11: z = i by A9, XTUPLE_0: 1;

          (i + 1) < (1 + 3) by A10;

          then i < (2 + 1) by XREAL_1: 7;

          then i <= 2 by NAT_1: 13;

          then z = 0 or ... or z = 2 by A11;

          hence thesis by A5, A9, A11, ENUMSET1:def 4;

        end;

      end;

      

       A12: [(2 + 1), (1 + 1)] in { [(i + 1), i] where i be Element of NAT : (i + 1) < 4 };

      

       A13: [(1 + 1), (2 + 1)] in { [i, (i + 1)] where i be Element of NAT : (i + 1) < 4 };

      

       A14: [(1 + 1), ( 0 + 1)] in { [(i + 1), i] where i be Element of NAT : (i + 1) < 4 };

      

       A15: [( 0 + 1), (1 + 1)] in { [i, (i + 1)] where i be Element of NAT : (i + 1) < 4 };

      

       A16: [ 0 , ( 0 + 1)] in { [i, (i + 1)] where i be Element of NAT : (i + 1) < 4 };

      A c= B

      proof

        let x be object;

        assume

         A17: x in A;

        per cases by A17, ENUMSET1:def 4;

          suppose x = [ 0 , 1];

          hence thesis by A2, A16, XBOOLE_0:def 3;

        end;

          suppose x = [1, 0 ];

          hence thesis by A2, A1, XBOOLE_0:def 3;

        end;

          suppose x = [1, 2];

          hence thesis by A2, A15, XBOOLE_0:def 3;

        end;

          suppose x = [2, 1];

          hence thesis by A2, A14, XBOOLE_0:def 3;

        end;

          suppose x = [2, 3];

          hence thesis by A2, A13, XBOOLE_0:def 3;

        end;

          suppose x = [3, 2];

          hence thesis by A2, A12, XBOOLE_0:def 3;

        end;

      end;

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    registration

      let n be Nat;

      cluster -> finite for Element of ( Rank n);

      coherence

      proof

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

        let x be Element of ( Rank n);

        per cases ;

          suppose ( Rank n) = {} ;

          hence thesis;

        end;

          suppose

           A1: ( Rank n) <> {} ;

          

           A2: ( Rank m) is finite by CARD_2: 67;

          x c= ( Rank n) by A1, ORDINAL1:def 2;

          hence thesis by A2;

        end;

      end;

    end

    theorem :: NECKLA_2:3

    

     Th3: for x be set st x in FinSETS holds x is finite

    proof

      

       A1: omega is limit_ordinal by ORDINAL1:def 11;

      let x be set;

      assume x in FinSETS ;

      then

      consider n be Ordinal such that

       A2: n in omega and

       A3: x in ( Rank n) by A1, CLASSES1: 31, CLASSES2: 64;

      reconsider n as Nat by A2;

      x is Element of ( Rank n) by A3;

      hence thesis;

    end;

    registration

      cluster -> finite for Element of FinSETS ;

      coherence by Th3;

    end

    definition

      let G be non empty RelStr;

      :: NECKLA_2:def1

      attr G is N-free means not G embeds ( Necklace 4);

    end

    registration

      cluster strict finite N-free for non empty RelStr;

      existence

      proof

        set X = { 0 , 1}, Y = ( Necklace 4);

        reconsider r = ( id X) as Relation of X by RELSET_1: 14;

        take R = RelStr (# X, r #);

        now

          let f be Function of Y, R;

          

           A1: ( dom f) = the carrier of Y by FUNCT_2:def 1

          .= { 0 , 1, 2, 3} by NECKLACE: 1, NECKLACE: 20;

          then

           A2: 3 in ( dom f) by ENUMSET1:def 2;

          then

           A3: (f . 3) in X by PARTFUN1: 4;

          

           A4: 2 in ( dom f) by A1, ENUMSET1:def 2;

          then (f . 2) in X by PARTFUN1: 4;

          then

           A5: (f . 2) = 0 or (f . 2) = 1 by TARSKI:def 2;

          

           A6: 1 in ( dom f) by A1, ENUMSET1:def 2;

          then (f . 1) in X by PARTFUN1: 4;

          then

           A7: (f . 1) = 0 or (f . 1) = 1 by TARSKI:def 2;

          assume

           A8: f is one-to-one;

          then

           A9: (f . 2) <> (f . 3) by A4, A2, FUNCT_1:def 4;

          (f . 1) <> (f . 3) by A8, A6, A2, FUNCT_1:def 4;

          hence ex x,y be Element of Y st not ( [x, y] in the InternalRel of Y iff [(f . x), (f . y)] in the InternalRel of R) by A8, A6, A4, A9, A3, A7, A5, FUNCT_1:def 4, TARSKI:def 2;

        end;

        then not R embeds Y by NECKLACE:def 1;

        hence thesis;

      end;

    end

    definition

      let R,S be RelStr;

      :: NECKLA_2:def2

      func union_of (R,S) -> strict RelStr means

      : Def2: the carrier of it = (the carrier of R \/ the carrier of S) & the InternalRel of it = (the InternalRel of R \/ the InternalRel of S);

      existence

      proof

        set X = (the carrier of R \/ the carrier of S);

        

         A1: the carrier of S c= X by XBOOLE_1: 7;

        the carrier of R c= X by XBOOLE_1: 7;

        then

        reconsider IR = the InternalRel of R, IS = the InternalRel of S as Relation of X by A1, RELSET_1: 7;

        set D = (IR \/ IS);

        reconsider D as Relation of X;

        take RelStr (# X, D #);

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      let R,S be RelStr;

      :: NECKLA_2:def3

      func sum_of (R,S) -> strict RelStr means

      : Def3: the carrier of it = (the carrier of R \/ the carrier of S) & the InternalRel of it = (((the InternalRel of R \/ the InternalRel of S) \/ [:the carrier of R, the carrier of S:]) \/ [:the carrier of S, the carrier of R:]);

      existence

      proof

        set X = (the carrier of R \/ the carrier of S);

        

         A1: the carrier of S c= X by XBOOLE_1: 7;

        

         A2: the carrier of R c= X by XBOOLE_1: 7;

        then

        reconsider IQ = [:the carrier of R, the carrier of S:] as Relation of X by A1, ZFMISC_1: 96;

        reconsider IP = [:the carrier of S, the carrier of R:] as Relation of X by A2, A1, ZFMISC_1: 96;

        

         A3: the carrier of S c= X by XBOOLE_1: 7;

        the carrier of R c= X by XBOOLE_1: 7;

        then

        reconsider IR = the InternalRel of R, IS = the InternalRel of S as Relation of X by A3, RELSET_1: 7;

        set D = (((IR \/ IS) \/ IQ) \/ IP);

        take RelStr (# X, D #);

        thus thesis;

      end;

      uniqueness ;

    end

    definition

      :: NECKLA_2:def4

      func fin_RelStr -> set means

      : Def4: for X be object holds X in it iff ex R be strict RelStr st X = R & the carrier of R in FinSETS ;

      existence

      proof

        defpred P[ object, object] means ex R be strict RelStr st $1 = [the carrier of R, the InternalRel of R] & $2 = R;

        

         A1: for x,y,z be object st P[x, y] & P[x, z] holds y = z

        proof

          let x,y,z be object;

          given R1 be strict RelStr such that

           A2: x = [the carrier of R1, the InternalRel of R1] and

           A3: y = R1;

          given R2 be strict RelStr such that

           A4: x = [the carrier of R2, the InternalRel of R2] and

           A5: z = R2;

          the carrier of R1 = the carrier of R2 by A2, A4, XTUPLE_0: 1;

          hence thesis by A2, A3, A4, A5, XTUPLE_0: 1;

        end;

        consider X be set such that

         A6: for x be object holds x in X iff ex y be object st y in FinSETS & P[y, x] from TARSKI:sch 1( A1);

        take X;

        for x be object holds x in X iff ex R be strict RelStr st x = R & the carrier of R in FinSETS

        proof

          let x be object;

          thus x in X implies ex R be strict RelStr st x = R & the carrier of R in FinSETS

          proof

            assume x in X;

            then

            consider y be object such that

             A7: y in FinSETS and

             A8: ex R be strict RelStr st y = [the carrier of R, the InternalRel of R] & x = R by A6;

            consider R be strict RelStr such that

             A9: y = [the carrier of R, the InternalRel of R] and

             A10: x = R by A8;

            

             A11: {the carrier of R} in { {the carrier of R, the InternalRel of R}, {the carrier of R}} by TARSKI:def 2;

             { {the carrier of R, the InternalRel of R}, {the carrier of R}} c= FinSETS by A7, A9, ORDINAL1:def 2;

            then

             A12: {the carrier of R} c= FinSETS by A11, ORDINAL1:def 2;

            the carrier of R in {the carrier of R} by TARSKI:def 1;

            hence thesis by A10, A12;

          end;

          given R be strict RelStr such that

           A13: x = R and

           A14: the carrier of R in FinSETS ;

          consider R be strict RelStr such that

           A15: x = R and

           A16: the carrier of R in FinSETS by A13, A14;

          the InternalRel of R in FinSETS by A16, Th1;

          then [the carrier of R, the InternalRel of R] in FinSETS by A16, CLASSES2: 58;

          hence thesis by A6, A15;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ object] means ex R be strict RelStr st $1 = R & the carrier of R in FinSETS ;

        thus for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

      end;

    end

    registration

      cluster fin_RelStr -> non empty;

      correctness

      proof

         RelStr (# {} , ( {} ( {} , {} )) #) in fin_RelStr

        proof

          set X = RelStr (# {} , ( {} ( {} , {} )) #);

          the carrier of X in FinSETS by CLASSES1: 2, CLASSES2:def 2;

          hence thesis by Def4;

        end;

        hence thesis;

      end;

    end

    definition

      :: NECKLA_2:def5

      func fin_RelStr_sp -> Subset of fin_RelStr means

      : Def5: (for R be strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds R in it ) & (for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in it & H2 in it holds ( union_of (H1,H2)) in it & ( sum_of (H1,H2)) in it ) & for M be Subset of fin_RelStr st ((for R be strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds R in M) & for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds ( union_of (H1,H2)) in M & ( sum_of (H1,H2)) in M) holds it c= M;

      existence

      proof

        defpred P[ set] means (for R be strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds R in $1) & (for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in $1 & H2 in $1 holds ( union_of (H1,H2)) in $1 & ( sum_of (H1,H2)) in $1);

        consider X be set such that

         A1: for x be set holds x in X iff x in ( bool fin_RelStr ) & P[x] from XFAMILY:sch 1;

        for x be object holds x in X implies x in ( bool fin_RelStr ) by A1;

        then

        reconsider X as Subset-Family of fin_RelStr by TARSKI:def 3;

        take IT = ( Intersect X);

        

         A2: P[ fin_RelStr ]

        proof

          set A = fin_RelStr ;

          for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in A & H2 in A holds ( union_of (H1,H2)) in A & ( sum_of (H1,H2)) in A

          proof

            let H1,H2 be strict RelStr such that the carrier of H1 misses the carrier of H2 and

             A3: H1 in A and

             A4: H2 in A;

            consider S2 be strict RelStr such that

             A5: S2 = H2 and

             A6: the carrier of S2 in FinSETS by A4, Def4;

            reconsider RS9 = ( sum_of (H1,H2)) as strict RelStr;

            consider S1 be strict RelStr such that

             A7: S1 = H1 and

             A8: the carrier of S1 in FinSETS by A3, Def4;

            reconsider RS = ( union_of (S1,S2)) as strict RelStr;

            

             A9: (the carrier of H1 \/ the carrier of H2) in FinSETS by A7, A8, A5, A6, CLASSES2: 60;

            then the carrier of RS in FinSETS by A7, A5, Def2;

            hence ( union_of (H1,H2)) in A by A7, A5, Def4;

            the carrier of RS9 in FinSETS by A9, Def3;

            hence thesis by Def4;

          end;

          hence thesis by Def4;

        end;

         fin_RelStr in ( bool fin_RelStr ) by ZFMISC_1:def 1;

        then

         A10: X <> {} by A1, A2;

        then

         A11: IT = ( meet X) by SETFAM_1:def 9;

         P[IT] & for X be Subset of fin_RelStr st P[X] holds IT c= X

        proof

          

           A12: for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in IT & H2 in IT holds ( union_of (H1,H2)) in IT & ( sum_of (H1,H2)) in IT

          proof

            let H1,H2 be strict RelStr such that

             A13: the carrier of H1 misses the carrier of H2 and

             A14: H1 in IT and

             A15: H2 in IT;

            

             A16: for Y be set holds Y in X implies ( sum_of (H1,H2)) in Y

            proof

              let Y be set;

              assume

               A17: Y in X;

              then

               A18: H2 in Y by A11, A15, SETFAM_1:def 1;

              H1 in Y by A11, A14, A17, SETFAM_1:def 1;

              hence thesis by A1, A13, A17, A18;

            end;

            for Y be set holds Y in X implies ( union_of (H1,H2)) in Y

            proof

              let Y be set;

              assume

               A19: Y in X;

              then

               A20: H2 in Y by A11, A15, SETFAM_1:def 1;

              H1 in Y by A11, A14, A19, SETFAM_1:def 1;

              hence thesis by A1, A13, A19, A20;

            end;

            hence thesis by A10, A11, A16, SETFAM_1:def 1;

          end;

          for R be strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds R in IT

          proof

            let R be strict RelStr such that

             A21: the carrier of R is 1 -element and

             A22: the carrier of R in FinSETS ;

            for Y be set holds Y in X implies R in Y by A1, A21, A22;

            hence thesis by A10, A11, SETFAM_1:def 1;

          end;

          hence P[IT] by A12;

          let Y be Subset of fin_RelStr such that

           A23: P[Y];

          IT c= Y

          proof

            

             A24: Y in X by A1, A23;

            let x be object;

            assume x in IT;

            hence thesis by A11, A24, SETFAM_1:def 1;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of fin_RelStr ;

        assume that

         A25: for R be strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds R in X1 and

         A26: for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X1 & H2 in X1 holds ( union_of (H1,H2)) in X1 & ( sum_of (H1,H2)) in X1 and

         A27: for M be Subset of fin_RelStr st ((for R be strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds R in M) & for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds ( union_of (H1,H2)) in M & ( sum_of (H1,H2)) in M) holds X1 c= M and

         A28: for R be strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds R in X2 and

         A29: for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in X2 & H2 in X2 holds ( union_of (H1,H2)) in X2 & ( sum_of (H1,H2)) in X2 and

         A30: for M be Subset of fin_RelStr st ((for R be strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds R in M) & for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds ( union_of (H1,H2)) in M & ( sum_of (H1,H2)) in M) holds X2 c= M;

        

         A31: X2 c= X1 by A25, A26, A30;

        X1 c= X2 by A27, A28, A29;

        hence thesis by A31, XBOOLE_0:def 10;

      end;

    end

    registration

      cluster fin_RelStr_sp -> non empty;

      correctness

      proof

         [: { 0 }, { 0 }:] c= [: { 0 }, { 0 }:];

        then

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

         RelStr (# { 0 }, R #) in fin_RelStr_sp

        proof

          set X = RelStr (# { 0 }, R #);

          

           A1: the carrier of X in FinSETS by CLASSES2: 56, CLASSES2: 57;

          thus thesis by A1, Def5;

        end;

        hence thesis;

      end;

    end

    theorem :: NECKLA_2:4

    

     Th4: for X be set st X in fin_RelStr_sp holds X is finite strict non empty RelStr

    proof

      let X be set;

      assume

       A1: X in fin_RelStr_sp ;

      then

       A2: ex R be strict RelStr st X = R & the carrier of R in FinSETS by Def4;

      then

      reconsider R = X as strict RelStr;

      now

        set M = ( fin_RelStr_sp \ {R}), F = fin_RelStr_sp ;

        reconsider M as Subset of fin_RelStr ;

        

         A3: R in {R} by TARSKI:def 1;

        assume

         A4: R is empty;

         A5:

        now

          let H1,H2 be strict RelStr;

          assume that

           A6: the carrier of H1 misses the carrier of H2 and

           A7: H1 in M and

           A8: H2 in M;

          

           A9: H2 in F by A8, XBOOLE_0:def 5;

          

           A10: not H1 in {R} by A7, XBOOLE_0:def 5;

          the carrier of H1 <> {}

          proof

            per cases by A10, TARSKI:def 1;

              suppose the carrier of H1 <> the carrier of R;

              hence thesis by A4;

            end;

              suppose

               A11: the InternalRel of H1 <> the InternalRel of R;

              set InterH1 = the InternalRel of H1;

              InterH1 <> {} by A4, A11;

              hence thesis;

            end;

          end;

          then

          reconsider A = the carrier of H1 as non empty set;

          (A \/ the carrier of H2) <> {} ;

          then ( union_of (H1,H2)) <> R by A4, Def2;

          then

           A12: not ( union_of (H1,H2)) in {R} by TARSKI:def 1;

          the carrier of ( sum_of (H1,H2)) = (A \/ the carrier of H2) by Def3;

          then

           A13: not ( sum_of (H1,H2)) in {R} by A4, TARSKI:def 1;

          

           A14: H1 in F by A7, XBOOLE_0:def 5;

          then ( union_of (H1,H2)) in F by A6, A9, Def5;

          hence ( union_of (H1,H2)) in M by A12, XBOOLE_0:def 5;

          ( sum_of (H1,H2)) in F by A6, A14, A9, Def5;

          hence ( sum_of (H1,H2)) in M by A13, XBOOLE_0:def 5;

        end;

        now

          let S be strict RelStr;

          assume that

           A15: the carrier of S is 1 -element and

           A16: the carrier of S in FinSETS ;

          

           A17: not S in {R} by A4, A15, TARSKI:def 1;

          S in F by A15, A16, Def5;

          hence S in M by A17, XBOOLE_0:def 5;

        end;

        then F c= M by A5, Def5;

        hence contradiction by A1, A3, XBOOLE_0:def 5;

      end;

      hence thesis by A2;

    end;

    theorem :: NECKLA_2:5

    for R be RelStr st R in fin_RelStr_sp holds the carrier of R in FinSETS

    proof

      let R be RelStr;

      assume R in fin_RelStr_sp ;

      then ex S be strict RelStr st R = S & the carrier of S in FinSETS by Def4;

      hence thesis;

    end;

    theorem :: NECKLA_2:6

    

     Th6: for X be set st X in fin_RelStr_sp holds X is strict1 -element RelStr or ex H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & (X = ( union_of (H1,H2)) or X = ( sum_of (H1,H2)))

    proof

      deffunc F( set, set) = ($2 \/ { x where x be Element of fin_RelStr_sp : ex R1,R2 be strict RelStr st the carrier of R1 misses the carrier of R2 & R1 in $2 & R2 in $2 & (x = ( union_of (R1,R2)) or x = ( sum_of (R1,R2))) });

      set Y = fin_RelStr_sp ;

      let X be set such that

       A1: X in fin_RelStr_sp ;

      consider f be Function such that

       A2: ( dom f) = NAT and

       A3: (f . 0 ) = { x where x be Element of fin_RelStr_sp : x is trivial RelStr } and

       A4: for n be Nat holds (f . (n + 1)) = F(n,.) from NAT_1:sch 11;

      

       A5: ( Union f) c= fin_RelStr_sp

      proof

        defpred P[ Nat] means (f . $1) c= fin_RelStr_sp ;

        let y be object;

        assume y in ( Union f);

        then

        consider x be object such that

         A6: x in ( dom f) and

         A7: y in (f . x) by CARD_5: 2;

        reconsider x as Element of NAT by A2, A6;

        

         A8: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A9: P[k];

          

           A10: { a where a be Element of fin_RelStr_sp : ex R1,R2 be strict RelStr st the carrier of R1 misses the carrier of R2 & R1 in (f . k) & R2 in (f . k) & (a = ( union_of (R1,R2)) or a = ( sum_of (R1,R2))) } c= fin_RelStr_sp

          proof

            let x be object;

            set S = { a where a be Element of fin_RelStr_sp : ex R1,R2 be strict RelStr st the carrier of R1 misses the carrier of R2 & R1 in (f . k) & R2 in (f . k) & (a = ( union_of (R1,R2)) or a = ( sum_of (R1,R2))) };

            assume x in S;

            then ex a be Element of fin_RelStr_sp st x = a & ex R1,R2 be strict RelStr st the carrier of R1 misses the carrier of R2 & R1 in (f . k) & R2 in (f . k) & (a = ( union_of (R1,R2)) or a = ( sum_of (R1,R2)));

            hence thesis;

          end;

          (f . (k + 1)) = ((f . k) \/ { a where a be Element of fin_RelStr_sp : ex R1,R2 be strict RelStr st the carrier of R1 misses the carrier of R2 & R1 in (f . k) & R2 in (f . k) & (a = ( union_of (R1,R2)) or a = ( sum_of (R1,R2))) }) by A4;

          hence thesis by A9, A10, XBOOLE_1: 8;

        end;

        

         A11: P[ 0 ]

        proof

          let y be object;

          assume y in (f . 0 );

          then ex a be Element of fin_RelStr_sp st y = a & a is trivial RelStr by A3;

          hence thesis;

        end;

        for k be Nat holds P[k] from NAT_1:sch 2( A11, A8);

        then (f . x) c= fin_RelStr_sp ;

        hence thesis by A7;

      end;

      then

      reconsider M = ( Union f) as Subset of fin_RelStr by XBOOLE_1: 1;

      

       A12: for i be Nat holds (f . i) c= (f . (i + 1))

      proof

        let i be Nat;

        

         A13: (f . (i + 1)) = ((f . i) \/ { b where b be Element of fin_RelStr_sp : ex R1,R2 be strict RelStr st the carrier of R1 misses the carrier of R2 & R1 in (f . i) & R2 in (f . i) & (b = ( union_of (R1,R2)) or b = ( sum_of (R1,R2))) }) by A4;

        let x be object;

        assume x in (f . i);

        hence thesis by A13, XBOOLE_0:def 3;

      end;

      

       A14: for i,j be Element of NAT st i <= j holds (f . i) c= (f . j)

      proof

        let i,j be Element of NAT ;

        defpred P[ Nat] means (f . i) c= (f . (i + $1));

        assume i <= j;

        then

         A15: ex k be Nat st j = (i + k) by NAT_1: 10;

        

         A16: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A17: P[k];

          (f . (i + k)) c= (f . ((i + k) + 1)) by A12;

          hence thesis by A17, XBOOLE_1: 1;

        end;

        

         A18: P[ 0 ];

        for k be Nat holds P[k] from NAT_1:sch 2( A18, A16);

        hence thesis by A15;

      end;

      

       A19: for H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds ( union_of (H1,H2)) in M & ( sum_of (H1,H2)) in M

      proof

        let H1,H2 be strict RelStr such that

         A20: the carrier of H1 misses the carrier of H2 and

         A21: H1 in M and

         A22: H2 in M;

        consider x2 be object such that

         A23: x2 in ( dom f) and

         A24: H2 in (f . x2) by A22, CARD_5: 2;

        consider x1 be object such that

         A25: x1 in ( dom f) and

         A26: H1 in (f . x1) by A21, CARD_5: 2;

        reconsider x1, x2 as Element of NAT by A2, A25, A23;

        set W = { a where a be Element of fin_RelStr_sp : ex R1,R2 be strict RelStr st the carrier of R1 misses the carrier of R2 & R1 in (f . ( max (x1,x2))) & R2 in (f . ( max (x1,x2))) & (a = ( union_of (R1,R2)) or a = ( sum_of (R1,R2))) };

        

         A27: (f . (( max (x1,x2)) + 1)) = ((f . ( max (x1,x2))) \/ W) by A4;

        

         A28: (f . x1) c= (f . ( max (x1,x2))) by A14, XXREAL_0: 25;

        

         A29: (f . x2) c= (f . ( max (x1,x2))) by A14, XXREAL_0: 25;

        ( sum_of (H1,H2)) in fin_RelStr_sp by A5, A20, A21, A22, Def5;

        then ( sum_of (H1,H2)) in W by A20, A26, A24, A28, A29;

        then

         A30: ( sum_of (H1,H2)) in (f . (( max (x1,x2)) + 1)) by A27, XBOOLE_0:def 3;

        ( union_of (H1,H2)) in fin_RelStr_sp by A5, A20, A21, A22, Def5;

        then ( union_of (H1,H2)) in W by A20, A26, A24, A28, A29;

        then ( union_of (H1,H2)) in (f . (( max (x1,x2)) + 1)) by A27, XBOOLE_0:def 3;

        hence thesis by A2, A30, CARD_5: 2;

      end;

      for R be strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds R in M

      proof

        

         A31: (f . 0 ) c= M by A2, CARD_5: 2;

        let R be strict RelStr such that

         A32: the carrier of R is 1 -element and

         A33: the carrier of R in FinSETS ;

        

         A34: R is trivial RelStr by A32;

        R is Element of fin_RelStr_sp by A32, A33, Def5;

        then R in (f . 0 ) by A3, A34;

        hence thesis by A31;

      end;

      then

       A35: fin_RelStr_sp c= M by A19, Def5;

      then

       A36: ( Union f) = fin_RelStr_sp by A5, XBOOLE_0:def 10;

      assume

       A37: not X is strict1 -element RelStr;

      ex H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in Y & H2 in Y & (X = ( union_of (H1,H2)) or X = ( sum_of (H1,H2)))

      proof

        defpred P[ Nat] means X in (f . $1) implies ex H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in Y & H2 in Y & (X = ( union_of (H1,H2)) or X = ( sum_of (H1,H2)));

        

         A38: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let n be Nat such that

           A39: P[n];

          set W = { a where a be Element of fin_RelStr_sp : ex R1,R2 be strict RelStr st the carrier of R1 misses the carrier of R2 & R1 in (f . n) & R2 in (f . n) & (a = ( union_of (R1,R2)) or a = ( sum_of (R1,R2))) };

          assume

           A40: X in (f . (n + 1));

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

          

           A41: (f . (n + 1)) = ((f . n) \/ W) by A4;

          per cases by A40, A41, XBOOLE_0:def 3;

            suppose X in (f . n);

            hence thesis by A39;

          end;

            suppose X in W;

            then ex a be Element of fin_RelStr_sp st a = X & ex R1,R2 be strict RelStr st the carrier of R1 misses the carrier of R2 & R1 in (f . n) & R2 in (f . n) & (a = ( union_of (R1,R2)) or a = ( sum_of (R1,R2)));

            then

            consider R1,R2 be strict RelStr such that

             A42: the carrier of R1 misses the carrier of R2 and

             A43: R1 in (f . n) and

             A44: R2 in (f . n) and

             A45: X = ( union_of (R1,R2)) or X = ( sum_of (R1,R2));

            

             A46: R2 in Y by A2, A36, A44, CARD_5: 2;

            R1 in Y by A2, A36, A43, CARD_5: 2;

            hence thesis by A42, A45, A46;

          end;

        end;

        

         A47: P[ 0 ]

        proof

          assume X in (f . 0 );

          then

          consider a be Element of fin_RelStr_sp such that

           A48: X = a & a is trivial RelStr by A3;

          a is strict non empty RelStr by Th4;

          then a is non empty trivial strict RelStr by A48;

          then

          reconsider a as non empty trivial strict RelStr;

          a is 1 -element strict RelStr;

          hence thesis by A37, A48;

        end;

        

         A49: for n be Nat holds P[n] from NAT_1:sch 2( A47, A38);

        ex y be object st y in ( dom f) & X in (f . y) by A1, A35, CARD_5: 2;

        hence thesis by A2, A49;

      end;

      hence thesis;

    end;

    

     Lm1: the carrier of ( Necklace 4) = { 0 , 1, 2, 3} by NECKLACE: 1, NECKLACE: 20;

    theorem :: NECKLA_2:7

    for R be strict non empty RelStr st R in fin_RelStr_sp holds R is N-free

    proof

      let R be strict non empty RelStr;

      set N4 = ( Necklace 4);

      defpred P[ Nat] means ex S be strict non empty RelStr st S in fin_RelStr_sp & ( card the carrier of S) = $1 & S embeds N4;

      assume

       A1: R in fin_RelStr_sp ;

      then ex S be strict RelStr st R = S & the carrier of S in FinSETS by Def4;

      then

      reconsider C = the carrier of R as Element of FinSETS ;

      set k = ( card C);

      

       A2: for m be Nat st m <> 0 & P[m] holds ex n be Nat st n < m & P[n]

      proof

        let m be Nat such that m <> 0 and

         A3: P[m];

        consider S be non empty strict RelStr such that

         A4: S in fin_RelStr_sp and

         A5: ( card the carrier of S) = m and

         A6: S embeds N4 by A3;

        per cases by A4, Th6;

          suppose

           A7: S is strict1 -element RelStr;

          

           A8: ( dom the InternalRel of S) c= the carrier of S by RELAT_1:def 18;

          

           A9: ( rng the InternalRel of S) c= the carrier of S by RELAT_1:def 19;

          consider f be Function of N4, S such that f is one-to-one and

           A10: for x,y be Element of N4 holds [x, y] in the InternalRel of N4 iff [(f . x), (f . y)] in the InternalRel of S by A6, NECKLACE:def 1;

          

           A11: the carrier of N4 = { 0 , 1, 2, 3} by NECKLACE: 1, NECKLACE: 20;

          then

           A12: 0 in the carrier of N4 by ENUMSET1:def 2;

          

           A13: 1 in the carrier of N4 by A11, ENUMSET1:def 2;

           0 = ( 0 + 1) or 1 = ( 0 + 1);

          then [ 0 , 1] in the InternalRel of N4 by A12, A13, NECKLACE: 25;

          then

           A14: [(f . 0 ), (f . 1)] in the InternalRel of S by A10, A12, A13;

          then

           A15: (f . 1) in ( rng the InternalRel of S) by XTUPLE_0:def 13;

          (f . 0 ) in ( dom the InternalRel of S) by A14, XTUPLE_0:def 12;

          then (f . 0 ) = (f . 1) by A7, A15, A8, A9, STRUCT_0:def 10;

          then [ 0 , 0 ] in the InternalRel of N4 by A10, A12, A14;

          then [ 0 , 0 ] = [ 0 , 1] or [ 0 , 0 ] = [1, 0 ] or [ 0 , 0 ] = [1, 2] or [ 0 , 0 ] = [2, 1] or [ 0 , 0 ] = [2, 3] or [ 0 , 0 ] = [3, 2] by Th2, ENUMSET1:def 4;

          hence thesis by XTUPLE_0: 1;

        end;

          suppose ex H1,H2 be strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & (S = ( union_of (H1,H2)) or S = ( sum_of (H1,H2)));

          then

          consider H1,H2 be strict RelStr such that

           A16: the carrier of H1 misses the carrier of H2 and

           A17: H1 in fin_RelStr_sp and

           A18: H2 in fin_RelStr_sp and

           A19: S = ( union_of (H1,H2)) or S = ( sum_of (H1,H2));

           A20:

          now

            

             A21: not [1, 3] in the InternalRel of N4

            proof

              assume

               A22: [1, 3] in the InternalRel of N4;

              per cases by A22, Th2, ENUMSET1:def 4;

                suppose [1, 3] = [ 0 , 1];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [1, 3] = [1, 2];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [1, 3] = [2, 3];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [1, 3] = [3, 2];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [1, 3] = [2, 1];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [1, 3] = [1, 0 ];

                hence contradiction by XTUPLE_0: 1;

              end;

            end;

            

             A23: not [ 0 , 2] in the InternalRel of N4

            proof

              assume

               A24: [ 0 , 2] in the InternalRel of N4;

              per cases by A24, Th2, ENUMSET1:def 4;

                suppose [ 0 , 2] = [ 0 , 1];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 2] = [1, 2];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 2] = [2, 3];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 2] = [3, 2];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 2] = [2, 1];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 2] = [1, 0 ];

                hence contradiction by XTUPLE_0: 1;

              end;

            end;

            

             A25: the carrier of N4 = { 0 , 1, 2, 3} by NECKLACE: 1, NECKLACE: 20;

            then

             A26: 0 in the carrier of N4 by ENUMSET1:def 2;

            

             A27: not [ 0 , 3] in the InternalRel of N4

            proof

              assume

               A28: [ 0 , 3] in the InternalRel of N4;

              per cases by A28, Th2, ENUMSET1:def 4;

                suppose [ 0 , 3] = [ 0 , 1];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 3] = [1, 2];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 3] = [2, 3];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 3] = [3, 2];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 3] = [2, 1];

                hence contradiction by XTUPLE_0: 1;

              end;

                suppose [ 0 , 3] = [1, 0 ];

                hence contradiction by XTUPLE_0: 1;

              end;

            end;

            set A = the InternalRel of H1, B = the InternalRel of H2, C = [:the carrier of H1, the carrier of H2:], D = [:the carrier of H2, the carrier of H1:], cH1 = the carrier of H1, cH2 = the carrier of H2, cS = the carrier of S;

            

             A29: ( dom the InternalRel of S) c= cS by RELAT_1:def 18;

            assume

             A30: S = ( sum_of (H1,H2));

            

             A31: C c= the InternalRel of S

            proof

              let x be object;

              assume x in C;

              then

               A32: x in ((A \/ B) \/ C) by XBOOLE_0:def 3;

              ((A \/ B) \/ C) c= (((A \/ B) \/ C) \/ D) by XBOOLE_1: 7;

              then ((A \/ B) \/ C) c= the InternalRel of S by A30, Def3;

              hence thesis by A32;

            end;

            

             A33: ( rng the InternalRel of S) c= cS by RELAT_1:def 19;

            

             A34: 3 in the carrier of N4 by A25, ENUMSET1:def 2;

            

             A35: D c= the InternalRel of S

            proof

              let x be object;

              ((B \/ C) \/ D) c= (A \/ ((B \/ C) \/ D)) by XBOOLE_1: 7;

              then ((B \/ C) \/ D) c= (A \/ (B \/ (C \/ D))) by XBOOLE_1: 4;

              then ((B \/ C) \/ D) c= ((A \/ B) \/ (C \/ D)) by XBOOLE_1: 4;

              then ((B \/ C) \/ D) c= (((A \/ B) \/ C) \/ D) by XBOOLE_1: 4;

              then

               A36: ((B \/ C) \/ D) c= the InternalRel of S by A30, Def3;

              assume x in D;

              then x in ((B \/ C) \/ D) by XBOOLE_0:def 3;

              hence thesis by A36;

            end;

            

             A37: ( rng A) c= cH1 by RELAT_1:def 19;

            

             A38: 1 in the carrier of N4 by A25, ENUMSET1:def 2;

            consider f be Function of N4, S such that

             A39: f is one-to-one and

             A40: for x,y be Element of N4 holds [x, y] in the InternalRel of N4 iff [(f . x), (f . y)] in the InternalRel of S by A6, NECKLACE:def 1;

             [1, 0 ] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A41: [(f . 1), (f . 0 )] in the InternalRel of S by A40, A26, A38;

            

             A42: 2 in the carrier of N4 by A25, ENUMSET1:def 2;

             [3, 2] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A43: [(f . 3), (f . 2)] in the InternalRel of S by A40, A42, A34;

             [2, 1] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A44: [(f . 2), (f . 1)] in the InternalRel of S by A40, A38, A42;

            

             A45: ( rng B) c= cH2 by RELAT_1:def 19;

             [2, 3] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A46: [(f . 2), (f . 3)] in the InternalRel of S by A40, A42, A34;

            then (f . 3) in ( rng the InternalRel of S) by XTUPLE_0:def 13;

            then (f . 3) in cS by A33;

            then

             A47: (f . 3) in (cH1 \/ cH2) by A30, Def3;

             [ 0 , 1] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A48: [(f . 0 ), (f . 1)] in the InternalRel of S by A40, A26, A38;

            then (f . 0 ) in ( dom the InternalRel of S) by XTUPLE_0:def 12;

            then (f . 0 ) in cS by A29;

            then

             A49: (f . 0 ) in (cH1 \/ cH2) by A30, Def3;

            (f . 1) in ( rng the InternalRel of S) by A48, XTUPLE_0:def 13;

            then (f . 1) in cS by A33;

            then

             A50: (f . 1) in (cH1 \/ cH2) by A30, Def3;

            

             A51: ( dom A) c= cH1 by RELAT_1:def 18;

             [1, 2] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A52: [(f . 1), (f . 2)] in the InternalRel of S by A40, A38, A42;

            then (f . 2) in ( rng the InternalRel of S) by XTUPLE_0:def 13;

            then (f . 2) in cS by A33;

            then

             A53: (f . 2) in (cH1 \/ cH2) by A30, Def3;

            

             A54: ( dom B) c= cH2 by RELAT_1:def 18;

            per cases by A49, XBOOLE_0:def 3;

              suppose

               A55: (f . 0 ) in cH1;

              set x1 = [(f . 0 ), (f . 1)], x2 = [(f . 1), (f . 2)], x3 = [(f . 2), (f . 3)], x4 = [(f . 1), (f . 0 )], x5 = [(f . 2), (f . 1)], x6 = [(f . 3), (f . 2)];

               A56:

              now

                assume x1 in D;

                then (f . 0 ) in cH2 by ZFMISC_1: 87;

                hence contradiction by A16, A55, XBOOLE_0: 3;

              end;

               A57:

              now

                assume (f . 2) in cH2;

                then [(f . 0 ), (f . 2)] in C by A55, ZFMISC_1: 87;

                hence contradiction by A40, A26, A42, A23, A31;

              end;

               A58:

              now

                assume x4 in B;

                then (f . 0 ) in ( rng B) by XTUPLE_0:def 13;

                hence contradiction by A16, A45, A55, XBOOLE_0: 3;

              end;

               A59:

              now

                assume x4 in C;

                then (f . 0 ) in cH2 by ZFMISC_1: 87;

                hence contradiction by A16, A55, XBOOLE_0: 3;

              end;

               A60:

              now

                assume x1 in B;

                then (f . 0 ) in ( dom B) by XTUPLE_0:def 12;

                hence contradiction by A16, A54, A55, XBOOLE_0: 3;

              end;

               A61:

              now

                assume (f . 3) in cH2;

                then [(f . 0 ), (f . 3)] in C by A55, ZFMISC_1: 87;

                hence contradiction by A40, A26, A34, A27, A31;

              end;

              then

               A62: (f . 3) in cH1 by A47, XBOOLE_0:def 3;

               A63:

              now

                assume (f . 1) in cH2;

                then [(f . 1), (f . 3)] in D by A62, ZFMISC_1: 87;

                hence contradiction by A40, A38, A34, A21, A35;

              end;

              

               A64: ( dom f) = the carrier of N4 by FUNCT_2:def 1;

              ( rng f) c= the carrier of H1

              proof

                let y be object;

                assume y in ( rng f);

                then

                consider x be object such that

                 A65: x in ( dom f) and

                 A66: y = (f . x) by FUNCT_1:def 3;

                per cases by A64, A65, Lm1, ENUMSET1:def 2;

                  suppose x = 0 ;

                  hence thesis by A55, A66;

                end;

                  suppose x = 1;

                  hence thesis by A50, A63, A66, XBOOLE_0:def 3;

                end;

                  suppose x = 2;

                  hence thesis by A53, A57, A66, XBOOLE_0:def 3;

                end;

                  suppose x = 3;

                  hence thesis by A47, A61, A66, XBOOLE_0:def 3;

                end;

              end;

              then

               A67: f is Function of the carrier of N4, cH1 by FUNCT_2: 6;

              H1 is finite by A17, Th4;

              then

              reconsider cH1 as finite set;

              

               A68: H1 is strict non empty RelStr by A17, Th4;

               A69:

              now

                assume x6 in B;

                then (f . 2) in ( rng B) by XTUPLE_0:def 13;

                hence contradiction by A45, A57;

              end;

               A70:

              now

                assume x3 in B;

                then (f . 2) in ( dom B) by XTUPLE_0:def 12;

                hence contradiction by A54, A57;

              end;

              x4 in (((A \/ B) \/ C) \/ D) by A30, A41, Def3;

              then x4 in ((A \/ B) \/ C) or x4 in D by XBOOLE_0:def 3;

              then x4 in (A \/ B) or x4 in C or x4 in D by XBOOLE_0:def 3;

              then

               A71: [(f . 1), (f . 0 )] in A by A58, A59, A63, XBOOLE_0:def 3, ZFMISC_1: 87;

               A72:

              now

                assume x2 in B;

                then (f . 1) in ( dom B) by XTUPLE_0:def 12;

                hence contradiction by A54, A63;

              end;

              x2 in (((A \/ B) \/ C) \/ D) by A30, A52, Def3;

              then x2 in ((A \/ B) \/ C) or x2 in D by XBOOLE_0:def 3;

              then x2 in (A \/ B) or x2 in C or x2 in D by XBOOLE_0:def 3;

              then

               A73: [(f . 1), (f . 2)] in A by A72, A57, A63, XBOOLE_0:def 3, ZFMISC_1: 87;

              x6 in (((A \/ B) \/ C) \/ D) by A30, A43, Def3;

              then x6 in ((A \/ B) \/ C) or x6 in D by XBOOLE_0:def 3;

              then x6 in (A \/ B) or x6 in C or x6 in D by XBOOLE_0:def 3;

              then

               A74: [(f . 3), (f . 2)] in A by A69, A57, A61, XBOOLE_0:def 3, ZFMISC_1: 87;

              x3 in (((A \/ B) \/ C) \/ D) by A30, A46, Def3;

              then x3 in ((A \/ B) \/ C) or x3 in D by XBOOLE_0:def 3;

              then x3 in (A \/ B) or x3 in C or x3 in D by XBOOLE_0:def 3;

              then

               A75: [(f . 2), (f . 3)] in A by A70, A61, A57, XBOOLE_0:def 3, ZFMISC_1: 87;

               A76:

              now

                assume x5 in B;

                then (f . 1) in ( rng B) by XTUPLE_0:def 13;

                hence contradiction by A45, A63;

              end;

              H2 is finite by A18, Th4;

              then

              reconsider cH2 as finite set;

              cS = (cH1 \/ cH2) by A30, Def3;

              then

              reconsider cS as finite set;

              

               A77: H2 is non empty by A18, Th4;

              

               A78: cH1 <> cS

              proof

                

                 A79: cS = (cH1 \/ cH2) by A30, Def3;

                assume

                 A80: cH1 = cS;

                consider x be object such that

                 A81: x in cH2 by A77, XBOOLE_0:def 1;

                (cH1 /\ cH2) = {} by A16, XBOOLE_0:def 7;

                then not x in cH1 by A81, XBOOLE_0:def 4;

                hence contradiction by A80, A79, A81, XBOOLE_0:def 3;

              end;

              cS = (cH1 \/ cH2) by A30, Def3;

              then cH1 c= cS by XBOOLE_1: 7;

              then cH1 c< cS by A78, XBOOLE_0:def 8;

              then

               A82: ( card cH1) < ( card cS) by CARD_2: 48;

              x5 in (((A \/ B) \/ C) \/ D) by A30, A44, Def3;

              then x5 in ((A \/ B) \/ C) or x5 in D by XBOOLE_0:def 3;

              then x5 in (A \/ B) or x5 in C or x5 in D by XBOOLE_0:def 3;

              then

               A83: [(f . 2), (f . 1)] in A by A76, A63, A57, XBOOLE_0:def 3, ZFMISC_1: 87;

              x1 in (((A \/ B) \/ C) \/ D) by A30, A48, Def3;

              then x1 in ((A \/ B) \/ C) or x1 in D by XBOOLE_0:def 3;

              then x1 in (A \/ B) or x1 in C or x1 in D by XBOOLE_0:def 3;

              then

               A84: [(f . 0 ), (f . 1)] in A by A60, A63, A56, XBOOLE_0:def 3, ZFMISC_1: 87;

              for x,y be Element of N4 holds [x, y] in the InternalRel of N4 iff [(f . x), (f . y)] in the InternalRel of H1

              proof

                let x,y be Element of N4;

                thus [x, y] in the InternalRel of N4 implies [(f . x), (f . y)] in the InternalRel of H1

                proof

                  assume

                   A85: [x, y] in the InternalRel of N4;

                  per cases by A85, Th2, ENUMSET1:def 4;

                    suppose

                     A86: [x, y] = [ 0 , 1];

                    then x = 0 by XTUPLE_0: 1;

                    hence thesis by A84, A86, XTUPLE_0: 1;

                  end;

                    suppose

                     A87: [x, y] = [1, 0 ];

                    then x = 1 by XTUPLE_0: 1;

                    hence thesis by A71, A87, XTUPLE_0: 1;

                  end;

                    suppose

                     A88: [x, y] = [1, 2];

                    then x = 1 by XTUPLE_0: 1;

                    hence thesis by A73, A88, XTUPLE_0: 1;

                  end;

                    suppose

                     A89: [x, y] = [2, 1];

                    then x = 2 by XTUPLE_0: 1;

                    hence thesis by A83, A89, XTUPLE_0: 1;

                  end;

                    suppose

                     A90: [x, y] = [2, 3];

                    then x = 2 by XTUPLE_0: 1;

                    hence thesis by A75, A90, XTUPLE_0: 1;

                  end;

                    suppose

                     A91: [x, y] = [3, 2];

                    then x = 3 by XTUPLE_0: 1;

                    hence thesis by A74, A91, XTUPLE_0: 1;

                  end;

                end;

                thus [(f . x), (f . y)] in the InternalRel of H1 implies [x, y] in the InternalRel of N4

                proof

                   [(f . x), (f . y)] in the InternalRel of S implies [x, y] in the InternalRel of N4 by A40;

                  then [(f . x), (f . y)] in (((A \/ B) \/ C) \/ D) implies [x, y] in the InternalRel of N4 by A30, Def3;

                  then [(f . x), (f . y)] in ((A \/ B) \/ (C \/ D)) implies [x, y] in the InternalRel of N4 by XBOOLE_1: 4;

                  then

                   A92: [(f . x), (f . y)] in (A \/ (B \/ (C \/ D))) implies [x, y] in the InternalRel of N4 by XBOOLE_1: 4;

                  assume [(f . x), (f . y)] in the InternalRel of H1;

                  hence thesis by A92, XBOOLE_0:def 3;

                end;

              end;

              then H1 embeds N4 by A39, A67, NECKLACE:def 1;

              hence thesis by A5, A17, A68, A82;

            end;

              suppose

               A93: (f . 0 ) in the carrier of H2;

              set x1 = [(f . 0 ), (f . 1)], x2 = [(f . 1), (f . 2)], x3 = [(f . 2), (f . 3)], x4 = [(f . 1), (f . 0 )], x5 = [(f . 2), (f . 1)], x6 = [(f . 3), (f . 2)];

               A94:

              now

                assume x1 in C;

                then (f . 0 ) in cH1 by ZFMISC_1: 87;

                hence contradiction by A16, A93, XBOOLE_0: 3;

              end;

               A95:

              now

                assume x4 in D;

                then (f . 0 ) in cH1 by ZFMISC_1: 87;

                hence contradiction by A16, A93, XBOOLE_0: 3;

              end;

               A96:

              now

                assume (f . 3) in cH1;

                then [(f . 0 ), (f . 3)] in D by A93, ZFMISC_1: 87;

                hence contradiction by A40, A26, A34, A27, A35;

              end;

              then

               A97: (f . 3) in cH2 by A47, XBOOLE_0:def 3;

               A98:

              now

                assume (f . 1) in cH1;

                then [(f . 1), (f . 3)] in C by A97, ZFMISC_1: 87;

                hence contradiction by A40, A38, A34, A21, A31;

              end;

               A99:

              now

                assume x4 in A;

                then (f . 1) in ( dom A) by XTUPLE_0:def 12;

                hence contradiction by A51, A98;

              end;

              x4 in (((A \/ B) \/ C) \/ D) by A30, A41, Def3;

              then x4 in ((A \/ B) \/ C) or x4 in D by XBOOLE_0:def 3;

              then x4 in (A \/ B) or x4 in C or x4 in D by XBOOLE_0:def 3;

              then

               A100: [(f . 1), (f . 0 )] in B by A99, A98, A95, XBOOLE_0:def 3, ZFMISC_1: 87;

               A101:

              now

                assume x5 in A;

                then (f . 1) in ( rng A) by XTUPLE_0:def 13;

                hence contradiction by A37, A98;

              end;

               A102:

              now

                assume (f . 2) in cH1;

                then [(f . 0 ), (f . 2)] in D by A93, ZFMISC_1: 87;

                hence contradiction by A40, A26, A42, A23, A35;

              end;

              

               A103: ( dom f) = the carrier of N4 by FUNCT_2:def 1;

              ( rng f) c= the carrier of H2

              proof

                let y be object;

                assume y in ( rng f);

                then

                consider x be object such that

                 A104: x in ( dom f) and

                 A105: y = (f . x) by FUNCT_1:def 3;

                per cases by A103, A104, Lm1, ENUMSET1:def 2;

                  suppose x = 0 ;

                  hence thesis by A93, A105;

                end;

                  suppose x = 1;

                  hence thesis by A50, A98, A105, XBOOLE_0:def 3;

                end;

                  suppose x = 2;

                  hence thesis by A53, A102, A105, XBOOLE_0:def 3;

                end;

                  suppose x = 3;

                  hence thesis by A47, A96, A105, XBOOLE_0:def 3;

                end;

              end;

              then

               A106: f is Function of the carrier of N4, cH2 by FUNCT_2: 6;

              H1 is finite by A17, Th4;

              then

              reconsider cH1 as finite set;

              

               A107: H2 is strict non empty RelStr by A18, Th4;

               A108:

              now

                assume x1 in A;

                then (f . 0 ) in ( dom A) by XTUPLE_0:def 12;

                hence contradiction by A16, A51, A93, XBOOLE_0: 3;

              end;

               A109:

              now

                assume x6 in A;

                then (f . 2) in ( rng A) by XTUPLE_0:def 13;

                hence contradiction by A37, A102;

              end;

               A110:

              now

                assume x3 in A;

                then (f . 2) in ( dom A) by XTUPLE_0:def 12;

                hence contradiction by A51, A102;

              end;

              x6 in (((A \/ B) \/ C) \/ D) by A30, A43, Def3;

              then x6 in ((A \/ B) \/ C) or x6 in D by XBOOLE_0:def 3;

              then x6 in (A \/ B) or x6 in C or x6 in D by XBOOLE_0:def 3;

              then

               A111: [(f . 3), (f . 2)] in B by A109, A96, A102, XBOOLE_0:def 3, ZFMISC_1: 87;

               A112:

              now

                assume x2 in A;

                then (f . 2) in ( rng A) by XTUPLE_0:def 13;

                hence contradiction by A37, A102;

              end;

              x2 in (((A \/ B) \/ C) \/ D) by A30, A52, Def3;

              then x2 in ((A \/ B) \/ C) or x2 in D by XBOOLE_0:def 3;

              then x2 in (A \/ B) or x2 in C or x2 in D by XBOOLE_0:def 3;

              then

               A113: [(f . 1), (f . 2)] in B by A112, A98, A102, XBOOLE_0:def 3, ZFMISC_1: 87;

              x3 in (((A \/ B) \/ C) \/ D) by A30, A46, Def3;

              then x3 in ((A \/ B) \/ C) or x3 in D by XBOOLE_0:def 3;

              then x3 in (A \/ B) or x3 in C or x3 in D by XBOOLE_0:def 3;

              then

               A114: [(f . 2), (f . 3)] in B by A110, A102, A96, XBOOLE_0:def 3, ZFMISC_1: 87;

              x5 in (((A \/ B) \/ C) \/ D) by A30, A44, Def3;

              then x5 in ((A \/ B) \/ C) or x5 in D by XBOOLE_0:def 3;

              then x5 in (A \/ B) or x5 in C or x5 in D by XBOOLE_0:def 3;

              then

               A115: [(f . 2), (f . 1)] in B by A101, A102, A98, XBOOLE_0:def 3, ZFMISC_1: 87;

              H2 is finite by A18, Th4;

              then

              reconsider cH2 as finite set;

              cS = (cH1 \/ cH2) by A30, Def3;

              then

              reconsider cS as finite set;

              

               A116: H1 is non empty by A17, Th4;

              

               A117: cH2 <> cS

              proof

                

                 A118: cS = (cH1 \/ cH2) by A30, Def3;

                assume

                 A119: cH2 = cS;

                consider x be object such that

                 A120: x in cH1 by A116, XBOOLE_0:def 1;

                (cH1 /\ cH2) = {} by A16, XBOOLE_0:def 7;

                then not x in cH2 by A120, XBOOLE_0:def 4;

                hence contradiction by A119, A118, A120, XBOOLE_0:def 3;

              end;

              cS = (cH1 \/ cH2) by A30, Def3;

              then cH2 c= cS by XBOOLE_1: 7;

              then cH2 c< cS by A117, XBOOLE_0:def 8;

              then

               A121: ( card cH2) < ( card cS) by CARD_2: 48;

              x1 in (((A \/ B) \/ C) \/ D) by A30, A48, Def3;

              then x1 in ((A \/ B) \/ C) or x1 in D by XBOOLE_0:def 3;

              then x1 in (A \/ B) or x1 in C or x1 in D by XBOOLE_0:def 3;

              then

               A122: [(f . 0 ), (f . 1)] in B by A108, A94, A98, XBOOLE_0:def 3, ZFMISC_1: 87;

              for x,y be Element of N4 holds [x, y] in the InternalRel of N4 iff [(f . x), (f . y)] in the InternalRel of H2

              proof

                let x,y be Element of N4;

                thus [x, y] in the InternalRel of N4 implies [(f . x), (f . y)] in the InternalRel of H2

                proof

                  assume

                   A123: [x, y] in the InternalRel of N4;

                  per cases by A123, Th2, ENUMSET1:def 4;

                    suppose

                     A124: [x, y] = [ 0 , 1];

                    then x = 0 by XTUPLE_0: 1;

                    hence thesis by A122, A124, XTUPLE_0: 1;

                  end;

                    suppose

                     A125: [x, y] = [1, 0 ];

                    then x = 1 by XTUPLE_0: 1;

                    hence thesis by A100, A125, XTUPLE_0: 1;

                  end;

                    suppose

                     A126: [x, y] = [1, 2];

                    then x = 1 by XTUPLE_0: 1;

                    hence thesis by A113, A126, XTUPLE_0: 1;

                  end;

                    suppose

                     A127: [x, y] = [2, 1];

                    then x = 2 by XTUPLE_0: 1;

                    hence thesis by A115, A127, XTUPLE_0: 1;

                  end;

                    suppose

                     A128: [x, y] = [2, 3];

                    then x = 2 by XTUPLE_0: 1;

                    hence thesis by A114, A128, XTUPLE_0: 1;

                  end;

                    suppose

                     A129: [x, y] = [3, 2];

                    then x = 3 by XTUPLE_0: 1;

                    hence thesis by A111, A129, XTUPLE_0: 1;

                  end;

                end;

                thus [(f . x), (f . y)] in the InternalRel of H2 implies [x, y] in the InternalRel of N4

                proof

                   [(f . x), (f . y)] in the InternalRel of S implies [x, y] in the InternalRel of N4 by A40;

                  then [(f . x), (f . y)] in (((A \/ B) \/ C) \/ D) implies [x, y] in the InternalRel of N4 by A30, Def3;

                  then [(f . x), (f . y)] in ((A \/ B) \/ (C \/ D)) implies [x, y] in the InternalRel of N4 by XBOOLE_1: 4;

                  then

                   A130: [(f . x), (f . y)] in (B \/ (A \/ (C \/ D))) implies [x, y] in the InternalRel of N4 by XBOOLE_1: 4;

                  assume [(f . x), (f . y)] in the InternalRel of H2;

                  hence thesis by A130, XBOOLE_0:def 3;

                end;

              end;

              then H2 embeds N4 by A39, A106, NECKLACE:def 1;

              hence thesis by A5, A18, A107, A121;

            end;

          end;

          now

            

             A131: the carrier of N4 = { 0 , 1, 2, 3} by NECKLACE: 1, NECKLACE: 20;

            then

             A132: 0 in the carrier of N4 by ENUMSET1:def 2;

            

             A133: 3 in the carrier of N4 by A131, ENUMSET1:def 2;

            

             A134: 1 in the carrier of N4 by A131, ENUMSET1:def 2;

            

             A135: ( dom the InternalRel of S) c= the carrier of S by RELAT_1:def 18;

            consider f be Function of N4, S such that

             A136: f is one-to-one and

             A137: for x,y be Element of N4 holds [x, y] in the InternalRel of N4 iff [(f . x), (f . y)] in the InternalRel of S by A6, NECKLACE:def 1;

            assume

             A138: S = ( union_of (H1,H2));

             [ 0 , 1] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A139: [(f . 0 ), (f . 1)] in the InternalRel of S by A137, A132, A134;

            then (f . 0 ) in ( dom the InternalRel of S) by XTUPLE_0:def 12;

            then (f . 0 ) in the carrier of S by A135;

            then

             A140: (f . 0 ) in (the carrier of H1 \/ the carrier of H2) by A138, Def2;

            

             A141: 2 in the carrier of N4 by A131, ENUMSET1:def 2;

             [3, 2] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A142: [(f . 3), (f . 2)] in the InternalRel of S by A137, A141, A133;

             [2, 3] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A143: [(f . 2), (f . 3)] in the InternalRel of S by A137, A141, A133;

             [2, 1] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A144: [(f . 2), (f . 1)] in the InternalRel of S by A137, A134, A141;

             [1, 2] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A145: [(f . 1), (f . 2)] in the InternalRel of S by A137, A134, A141;

             [1, 0 ] in the InternalRel of N4 by Th2, ENUMSET1:def 4;

            then

             A146: [(f . 1), (f . 0 )] in the InternalRel of S by A137, A132, A134;

            per cases by A140, XBOOLE_0:def 3;

              suppose

               A147: (f . 0 ) in the carrier of H1;

              set cS = the carrier of S, cH1 = the carrier of H1, cH2 = the carrier of H2;

              

               A148: ( dom f) = the carrier of N4 by FUNCT_2:def 1;

              H2 is finite by A18, Th4;

              then

              reconsider cH2 as finite set;

              H1 is finite by A17, Th4;

              then

              reconsider cH1 as finite set;

              

               A149: cS = (cH1 \/ cH2) by A138, Def2;

              

               A150: ( dom the InternalRel of H2) c= the carrier of H2 by RELAT_1:def 18;

               A151:

              now

                assume [(f . 0 ), (f . 1)] in the InternalRel of H2;

                then (f . 0 ) in ( dom the InternalRel of H2) by XTUPLE_0:def 12;

                hence contradiction by A16, A147, A150, XBOOLE_0: 3;

              end;

              

               A152: ( rng the InternalRel of H2) c= the carrier of H2 by RELAT_1:def 19;

               A153:

              now

                assume [(f . 1), (f . 0 )] in the InternalRel of H2;

                then (f . 0 ) in ( rng the InternalRel of H2) by XTUPLE_0:def 13;

                hence contradiction by A16, A147, A152, XBOOLE_0: 3;

              end;

               [(f . 1), (f . 0 )] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A146, Def2;

              then

               A154: [(f . 1), (f . 0 )] in the InternalRel of H1 by A153, XBOOLE_0:def 3;

              

               A155: H1 is strict non empty RelStr by A17, Th4;

              reconsider cS as finite set by A149;

              

               A156: ( rng the InternalRel of H1) c= the carrier of H1 by RELAT_1:def 19;

               [(f . 0 ), (f . 1)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A139, Def2;

              then

               A157: [(f . 0 ), (f . 1)] in the InternalRel of H1 by A151, XBOOLE_0:def 3;

              then

               A158: (f . 1) in ( rng the InternalRel of H1) by XTUPLE_0:def 13;

               A159:

              now

                assume [(f . 2), (f . 1)] in the InternalRel of H2;

                then (f . 1) in ( rng the InternalRel of H2) by XTUPLE_0:def 13;

                hence contradiction by A16, A156, A152, A158, XBOOLE_0: 3;

              end;

              

               A160: H2 is non empty by A18, Th4;

              

               A161: cH1 <> cS

              proof

                

                 A162: cS = (cH1 \/ cH2) by A138, Def2;

                assume

                 A163: cH1 = cS;

                consider x be object such that

                 A164: x in cH2 by A160, XBOOLE_0:def 1;

                (cH1 /\ cH2) = {} by A16, XBOOLE_0:def 7;

                then not x in cH1 by A164, XBOOLE_0:def 4;

                hence contradiction by A163, A162, A164, XBOOLE_0:def 3;

              end;

              cS = (cH1 \/ cH2) by A138, Def2;

              then cH1 c= cS by XBOOLE_1: 7;

              then cH1 c< cS by A161, XBOOLE_0:def 8;

              then

               A165: ( card cH1) < ( card cS) by CARD_2: 48;

              

               A166: [(f . 2), (f . 3)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A143, Def2;

              

               A167: [(f . 1), (f . 2)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A145, Def2;

              now

                assume [(f . 1), (f . 2)] in the InternalRel of H2;

                then (f . 1) in ( dom the InternalRel of H2) by XTUPLE_0:def 12;

                hence contradiction by A16, A156, A150, A158, XBOOLE_0: 3;

              end;

              then

               A168: [(f . 1), (f . 2)] in the InternalRel of H1 by A167, XBOOLE_0:def 3;

              then

               A169: (f . 2) in ( rng the InternalRel of H1) by XTUPLE_0:def 13;

              now

                assume [(f . 2), (f . 3)] in the InternalRel of H2;

                then (f . 2) in ( dom the InternalRel of H2) by XTUPLE_0:def 12;

                hence contradiction by A16, A156, A150, A169, XBOOLE_0: 3;

              end;

              then

               A170: [(f . 2), (f . 3)] in the InternalRel of H1 by A166, XBOOLE_0:def 3;

               [(f . 2), (f . 1)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A144, Def2;

              then

               A171: [(f . 2), (f . 1)] in the InternalRel of H1 by A159, XBOOLE_0:def 3;

               A172:

              now

                assume [(f . 3), (f . 2)] in the InternalRel of H2;

                then (f . 2) in ( rng the InternalRel of H2) by XTUPLE_0:def 13;

                hence contradiction by A16, A156, A152, A169, XBOOLE_0: 3;

              end;

               [(f . 3), (f . 2)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A142, Def2;

              then

               A173: [(f . 3), (f . 2)] in the InternalRel of H1 by A172, XBOOLE_0:def 3;

              

               A174: for x,y be Element of N4 holds [x, y] in the InternalRel of N4 iff [(f . x), (f . y)] in the InternalRel of H1

              proof

                let x,y be Element of N4;

                thus [x, y] in the InternalRel of N4 implies [(f . x), (f . y)] in the InternalRel of H1

                proof

                  assume

                   A175: [x, y] in the InternalRel of N4;

                  per cases by A175, Th2, ENUMSET1:def 4;

                    suppose

                     A176: [x, y] = [ 0 , 1];

                    then x = 0 by XTUPLE_0: 1;

                    hence thesis by A157, A176, XTUPLE_0: 1;

                  end;

                    suppose

                     A177: [x, y] = [1, 0 ];

                    then x = 1 by XTUPLE_0: 1;

                    hence thesis by A154, A177, XTUPLE_0: 1;

                  end;

                    suppose

                     A178: [x, y] = [1, 2];

                    then x = 1 by XTUPLE_0: 1;

                    hence thesis by A168, A178, XTUPLE_0: 1;

                  end;

                    suppose

                     A179: [x, y] = [2, 1];

                    then x = 2 by XTUPLE_0: 1;

                    hence thesis by A171, A179, XTUPLE_0: 1;

                  end;

                    suppose

                     A180: [x, y] = [2, 3];

                    then x = 2 by XTUPLE_0: 1;

                    hence thesis by A170, A180, XTUPLE_0: 1;

                  end;

                    suppose

                     A181: [x, y] = [3, 2];

                    then x = 3 by XTUPLE_0: 1;

                    hence thesis by A173, A181, XTUPLE_0: 1;

                  end;

                end;

                thus [(f . x), (f . y)] in the InternalRel of H1 implies [x, y] in the InternalRel of N4

                proof

                   [(f . x), (f . y)] in the InternalRel of S implies [x, y] in the InternalRel of N4 by A137;

                  then

                   A182: [(f . x), (f . y)] in (the InternalRel of H1 \/ the InternalRel of H2) implies [x, y] in the InternalRel of N4 by A138, Def2;

                  assume [(f . x), (f . y)] in the InternalRel of H1;

                  hence thesis by A182, XBOOLE_0:def 3;

                end;

              end;

              

               A183: (f . 3) in ( rng the InternalRel of H1) by A170, XTUPLE_0:def 13;

              ( rng f) c= the carrier of H1

              proof

                let y be object;

                assume y in ( rng f);

                then

                consider x be object such that

                 A184: x in ( dom f) and

                 A185: y = (f . x) by FUNCT_1:def 3;

                per cases by A148, A184, Lm1, ENUMSET1:def 2;

                  suppose x = 0 ;

                  hence thesis by A147, A185;

                end;

                  suppose x = 1;

                  hence thesis by A156, A158, A185;

                end;

                  suppose x = 2;

                  hence thesis by A156, A169, A185;

                end;

                  suppose x = 3;

                  hence thesis by A156, A183, A185;

                end;

              end;

              then f is Function of the carrier of N4, the carrier of H1 by FUNCT_2: 6;

              then H1 embeds N4 by A136, A174, NECKLACE:def 1;

              hence thesis by A5, A17, A155, A165;

            end;

              suppose

               A186: (f . 0 ) in the carrier of H2;

              set cS = the carrier of S, cH1 = the carrier of H1, cH2 = the carrier of H2;

              

               A187: ( dom f) = the carrier of N4 by FUNCT_2:def 1;

              H2 is finite by A18, Th4;

              then

              reconsider cH2 as finite set;

              H1 is finite by A17, Th4;

              then

              reconsider cH1 as finite set;

              

               A188: cS = (cH1 \/ cH2) by A138, Def2;

              

               A189: ( dom the InternalRel of H1) c= the carrier of H1 by RELAT_1:def 18;

               A190:

              now

                assume [(f . 0 ), (f . 1)] in the InternalRel of H1;

                then (f . 0 ) in ( dom the InternalRel of H1) by XTUPLE_0:def 12;

                hence contradiction by A16, A186, A189, XBOOLE_0: 3;

              end;

              

               A191: ( rng the InternalRel of H1) c= the carrier of H1 by RELAT_1:def 19;

               A192:

              now

                assume [(f . 1), (f . 0 )] in the InternalRel of H1;

                then (f . 0 ) in ( rng the InternalRel of H1) by XTUPLE_0:def 13;

                hence contradiction by A16, A186, A191, XBOOLE_0: 3;

              end;

               [(f . 1), (f . 0 )] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A146, Def2;

              then

               A193: [(f . 1), (f . 0 )] in the InternalRel of H2 by A192, XBOOLE_0:def 3;

              

               A194: H2 is strict non empty RelStr by A18, Th4;

              reconsider cS as finite set by A188;

              

               A195: ( rng the InternalRel of H2) c= the carrier of H2 by RELAT_1:def 19;

               [(f . 0 ), (f . 1)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A139, Def2;

              then

               A196: [(f . 0 ), (f . 1)] in the InternalRel of H2 by A190, XBOOLE_0:def 3;

              then

               A197: (f . 1) in ( rng the InternalRel of H2) by XTUPLE_0:def 13;

               A198:

              now

                assume [(f . 2), (f . 1)] in the InternalRel of H1;

                then (f . 1) in ( rng the InternalRel of H1) by XTUPLE_0:def 13;

                hence contradiction by A16, A195, A191, A197, XBOOLE_0: 3;

              end;

              

               A199: H1 is non empty by A17, Th4;

              

               A200: cH2 <> cS

              proof

                

                 A201: cS = (cH1 \/ cH2) by A138, Def2;

                assume

                 A202: cH2 = cS;

                consider x be object such that

                 A203: x in cH1 by A199, XBOOLE_0:def 1;

                (cH1 /\ cH2) = {} by A16, XBOOLE_0:def 7;

                then not x in cH2 by A203, XBOOLE_0:def 4;

                hence contradiction by A202, A201, A203, XBOOLE_0:def 3;

              end;

              cS = (cH1 \/ cH2) by A138, Def2;

              then cH2 c= cS by XBOOLE_1: 7;

              then cH2 c< cS by A200, XBOOLE_0:def 8;

              then

               A204: ( card cH2) < ( card cS) by CARD_2: 48;

              

               A205: [(f . 2), (f . 3)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A143, Def2;

              

               A206: [(f . 1), (f . 2)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A145, Def2;

              now

                assume [(f . 1), (f . 2)] in the InternalRel of H1;

                then (f . 1) in ( dom the InternalRel of H1) by XTUPLE_0:def 12;

                hence contradiction by A16, A195, A189, A197, XBOOLE_0: 3;

              end;

              then

               A207: [(f . 1), (f . 2)] in the InternalRel of H2 by A206, XBOOLE_0:def 3;

              then

               A208: (f . 2) in ( rng the InternalRel of H2) by XTUPLE_0:def 13;

              now

                assume [(f . 2), (f . 3)] in the InternalRel of H1;

                then (f . 2) in ( dom the InternalRel of H1) by XTUPLE_0:def 12;

                hence contradiction by A16, A195, A189, A208, XBOOLE_0: 3;

              end;

              then

               A209: [(f . 2), (f . 3)] in the InternalRel of H2 by A205, XBOOLE_0:def 3;

               [(f . 2), (f . 1)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A144, Def2;

              then

               A210: [(f . 2), (f . 1)] in the InternalRel of H2 by A198, XBOOLE_0:def 3;

               A211:

              now

                assume [(f . 3), (f . 2)] in the InternalRel of H1;

                then (f . 2) in ( rng the InternalRel of H1) by XTUPLE_0:def 13;

                hence contradiction by A16, A195, A191, A208, XBOOLE_0: 3;

              end;

               [(f . 3), (f . 2)] in (the InternalRel of H1 \/ the InternalRel of H2) by A138, A142, Def2;

              then

               A212: [(f . 3), (f . 2)] in the InternalRel of H2 by A211, XBOOLE_0:def 3;

              

               A213: for x,y be Element of N4 holds [x, y] in the InternalRel of N4 iff [(f . x), (f . y)] in the InternalRel of H2

              proof

                let x,y be Element of N4;

                thus [x, y] in the InternalRel of N4 implies [(f . x), (f . y)] in the InternalRel of H2

                proof

                  assume

                   A214: [x, y] in the InternalRel of N4;

                  per cases by A214, Th2, ENUMSET1:def 4;

                    suppose

                     A215: [x, y] = [ 0 , 1];

                    then x = 0 by XTUPLE_0: 1;

                    hence thesis by A196, A215, XTUPLE_0: 1;

                  end;

                    suppose

                     A216: [x, y] = [1, 0 ];

                    then x = 1 by XTUPLE_0: 1;

                    hence thesis by A193, A216, XTUPLE_0: 1;

                  end;

                    suppose

                     A217: [x, y] = [1, 2];

                    then x = 1 by XTUPLE_0: 1;

                    hence thesis by A207, A217, XTUPLE_0: 1;

                  end;

                    suppose

                     A218: [x, y] = [2, 1];

                    then x = 2 by XTUPLE_0: 1;

                    hence thesis by A210, A218, XTUPLE_0: 1;

                  end;

                    suppose

                     A219: [x, y] = [2, 3];

                    then x = 2 by XTUPLE_0: 1;

                    hence thesis by A209, A219, XTUPLE_0: 1;

                  end;

                    suppose

                     A220: [x, y] = [3, 2];

                    then x = 3 by XTUPLE_0: 1;

                    hence thesis by A212, A220, XTUPLE_0: 1;

                  end;

                end;

                thus [(f . x), (f . y)] in the InternalRel of H2 implies [x, y] in the InternalRel of N4

                proof

                   [(f . x), (f . y)] in the InternalRel of S implies [x, y] in the InternalRel of N4 by A137;

                  then

                   A221: [(f . x), (f . y)] in (the InternalRel of H1 \/ the InternalRel of H2) implies [x, y] in the InternalRel of N4 by A138, Def2;

                  assume [(f . x), (f . y)] in the InternalRel of H2;

                  hence thesis by A221, XBOOLE_0:def 3;

                end;

              end;

              

               A222: (f . 3) in ( rng the InternalRel of H2) by A209, XTUPLE_0:def 13;

              ( rng f) c= the carrier of H2

              proof

                let y be object;

                assume y in ( rng f);

                then

                consider x be object such that

                 A223: x in ( dom f) and

                 A224: y = (f . x) by FUNCT_1:def 3;

                per cases by A187, A223, Lm1, ENUMSET1:def 2;

                  suppose x = 0 ;

                  hence thesis by A186, A224;

                end;

                  suppose x = 1;

                  hence thesis by A195, A197, A224;

                end;

                  suppose x = 2;

                  hence thesis by A195, A208, A224;

                end;

                  suppose x = 3;

                  hence thesis by A195, A222, A224;

                end;

              end;

              then f is Function of the carrier of N4, the carrier of H2 by FUNCT_2: 6;

              then H2 embeds N4 by A136, A213, NECKLACE:def 1;

              hence thesis by A5, A18, A194, A204;

            end;

          end;

          hence thesis by A19, A20;

        end;

      end;

      assume R embeds N4;

      then P[k] by A1;

      then

       A225: ex i be Nat st P[i];

       P[ 0 ] from NAT_1:sch 7( A225, A2);

      hence thesis;

    end;