lfuzzy_1.miz



    begin

    reserve X,Y for non empty set;

    registration

      let X;

      cluster -> real-valued for Membership_Func of X;

      coherence ;

    end

    definition

      let X, Y;

      let f,g be RMembership_Func of X, Y;

      :: original: is_less_than

      redefine

      :: LFUZZY_1:def1

      pred f is_less_than g means for x be Element of X, y be Element of Y holds (f . (x,y)) <= (g . (x,y));

      compatibility

      proof

        thus f is_less_than g iff for x be Element of X, y be Element of Y holds (f . (x,y)) <= (g . (x,y))

        proof

          hereby

            assume

             A1: f is_less_than g;

            thus for x be Element of X, y be Element of Y holds (f . (x,y)) <= (g . (x,y))

            proof

              let x be Element of X, y be Element of Y;

              ( dom f) = [:X, Y:] & [x, y] in [:X, Y:] by FUNCT_2:def 1;

              hence thesis by A1;

            end;

          end;

          assume

           A2: for x be Element of X, y be Element of Y holds (f . (x,y)) <= (g . (x,y));

          

           A3: for c be set st c in ( dom f) holds (f . c) <= (g . c)

          proof

            let c be set;

            assume

             A4: c in ( dom f);

            then

            consider x,y be object such that

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

            reconsider y as Element of Y by A4, A5, ZFMISC_1: 87;

            reconsider x as Element of X by A4, A5, ZFMISC_1: 87;

            (f . (x,y)) <= (g . (x,y)) by A2;

            hence thesis by A5;

          end;

          ( dom g) = [:X, Y:] by FUNCT_2:def 1;

          hence thesis by A3;

        end;

      end;

    end

    theorem :: LFUZZY_1:1

    

     Th1: for R,S be Membership_Func of X st for x be Element of X holds (R . x) = (S . x) holds R = S

    proof

      let R,S be Membership_Func of X;

      assume for x be Element of X holds (R . x) = (S . x);

      then

       A1: for x be Element of X st x in ( dom R) holds (R . x) = (S . x);

      ( dom R) = X & ( dom S) = X by FUNCT_2:def 1;

      hence thesis by A1, PARTFUN1: 5;

    end;

    theorem :: LFUZZY_1:2

    

     Th2: for R,S be RMembership_Func of X, Y st for x be Element of X, y be Element of Y holds (R . (x,y)) = (S . (x,y)) holds R = S

    proof

      let R,S be RMembership_Func of X, Y;

      assume

       A1: for x be Element of X, y be Element of Y holds (R . (x,y)) = (S . (x,y));

      

       A2: for x,y be object st [x, y] in ( dom R) holds (R . (x,y)) = (S . (x,y))

      proof

        let x,y be object;

        assume

         A3: [x, y] in ( dom R);

        then

        reconsider x as Element of X by ZFMISC_1: 87;

        reconsider y as Element of Y by A3, ZFMISC_1: 87;

        (R . (x,y)) = (S . (x,y)) by A1;

        hence thesis;

      end;

      ( dom R) = [:X, Y:] & ( dom S) = [:X, Y:] by FUNCT_2:def 1;

      hence thesis by A2, BINOP_1: 20;

    end;

    theorem :: LFUZZY_1:3

    

     Th3: for R,S be Membership_Func of X holds R = S iff R c= S & S c= R

    proof

      let R,S be Membership_Func of X;

      thus R = S implies R c= S & S c= R;

      assume

       A1: R c= S & S c= R;

      for x be Element of X holds (R . x) = (S . x)

      proof

        let x be Element of X;

        (R . x) <= (S . x) & (S . x) <= (R . x) by A1;

        hence thesis by XXREAL_0: 1;

      end;

      hence thesis by Th1;

    end;

    theorem :: LFUZZY_1:4

    for R be Membership_Func of X holds R c= R;

    theorem :: LFUZZY_1:5

    

     Th5: for R,S,T be Membership_Func of X holds R c= S & S c= T implies R c= T

    proof

      let R,S,T be Membership_Func of X;

      assume

       A1: R c= S & S c= T;

      for x be Element of X holds (R . x) <= (T . x)

      proof

        let x be Element of X;

        (R . x) <= (S . x) & (S . x) <= (T . x) by A1;

        hence thesis by XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: LFUZZY_1:6

    

     Th6: for X,Y,Z be non empty set, R,S be RMembership_Func of X, Y, T,U be RMembership_Func of Y, Z holds R c= S & T c= U implies (R (#) T) c= (S (#) U)

    proof

      let X,Y,Z be non empty set;

      let R,S be RMembership_Func of X, Y;

      let T,U be RMembership_Func of Y, Z;

      assume

       A1: R c= S & T c= U;

      for c be Element of [:X, Z:] holds ((R (#) T) . c) <= ((S (#) U) . c)

      proof

        let c be Element of [:X, Z:];

        consider x,z be object such that

         A2: [x, z] = c by RELAT_1:def 1;

        

         A3: x in X & z in Z by A2, ZFMISC_1: 87;

        for y be set st y in Y holds (R . [x, y]) <= (S . [x, y]) & (T . [y, z]) <= (U . [y, z])

        proof

          let y be set;

          assume y in Y;

          then [x, y] in [:X, Y:] & [y, z] in [:Y, Z:] by A3, ZFMISC_1: 87;

          hence thesis by A1;

        end;

        hence thesis by A2, A3, FUZZY_4: 18;

      end;

      hence thesis;

    end;

    definition

      let X be non empty set;

      let f,g be Membership_Func of X;

      :: original: min

      redefine

      func min (f,g);

      commutativity ;

      :: original: max

      redefine

      func max (f,g);

      commutativity ;

    end

    theorem :: LFUZZY_1:7

    for f,g be Membership_Func of X holds ( min (f,g)) c= f

    proof

      let f,g be Membership_Func of X;

      let x be Element of X;

      (( min (f,g)) . x) = ( min ((f . x),(g . x))) by FUZZY_1:def 3;

      hence (( min (f,g)) . x) <= (f . x) by XXREAL_0: 17;

    end;

    theorem :: LFUZZY_1:8

    for f,g be Membership_Func of X holds f c= ( max (f,g))

    proof

      let f,g be Membership_Func of X;

      let x be Element of X;

      (( max (f,g)) . x) = ( max ((f . x),(g . x))) by FUZZY_1:def 4;

      hence thesis by XXREAL_0: 25;

    end;

    begin

    definition

      let X be non empty set;

      let R be RMembership_Func of X, X;

      :: LFUZZY_1:def2

      attr R is reflexive means ( Imf (X,X)) c= R;

    end

    definition

      let X be non empty set;

      let R be RMembership_Func of X, X;

      :: original: reflexive

      redefine

      :: LFUZZY_1:def3

      attr R is reflexive means for x be Element of X holds (R . (x,x)) = 1;

      compatibility

      proof

        hereby

          assume R is reflexive;

          then

           A1: ( Imf (X,X)) c= R;

          thus for x be Element of X holds (R . (x,x)) = 1

          proof

            let x be Element of X;

            (( Imf (X,X)) . (x,x)) <= (R . (x,x)) by A1;

            then (R . (x,x)) <= 1 & (R . (x,x)) >= 1 by FUZZY_4: 4, FUZZY_4: 25;

            hence thesis by XXREAL_0: 1;

          end;

        end;

        assume

         A2: for x be Element of X holds (R . (x,x)) = 1;

        let x,y be Element of X;

        per cases ;

          suppose

           A3: x = y;

          then (( Imf (X,X)) . (x,y)) = 1 by FUZZY_4: 25;

          hence thesis by A2, A3;

        end;

          suppose x <> y;

          then (( Imf (X,X)) . (x,y)) = 0 by FUZZY_4: 25;

          hence thesis by FUZZY_4: 4;

        end;

      end;

    end

    definition

      let X be non empty set;

      let R be RMembership_Func of X, X;

      :: LFUZZY_1:def4

      attr R is symmetric means ( converse R) = R;

    end

    definition

      let X be non empty set;

      let R be RMembership_Func of X, X;

      :: original: symmetric

      redefine

      :: LFUZZY_1:def5

      attr R is symmetric means for x,y be Element of X holds (R . (x,y)) = (R . (y,x));

      compatibility

      proof

        thus R is symmetric iff for x,y be Element of X holds (R . (x,y)) = (R . (y,x))

        proof

          thus R is symmetric implies for x,y be Element of X holds (R . (x,y)) = (R . (y,x)) by FUZZY_4: 26;

          assume

           A1: for x,y be Element of X holds (R . (x,y)) = (R . (y,x));

          

           A2: for x,y be object st [x, y] in ( dom R) holds (( converse R) . (x,y)) = (R . (x,y))

          proof

            let x,y be object;

            assume [x, y] in ( dom R);

            then

            reconsider x, y as Element of X by ZFMISC_1: 87;

            (R . (x,y)) = (R . (y,x)) by A1;

            hence thesis by FUZZY_4: 26;

          end;

          ( dom ( converse R)) = [:X, X:] & ( dom R) = [:X, X:] by FUNCT_2:def 1;

          then ( converse R) = R by A2, BINOP_1: 20;

          hence thesis;

        end;

      end;

    end

    definition

      let X be non empty set;

      let R be RMembership_Func of X, X;

      :: LFUZZY_1:def6

      attr R is transitive means (R (#) R) c= R;

    end

    

     Lm1: for X,Y,Z be non empty set holds for R be RMembership_Func of X, Y holds for S be RMembership_Func of Y, Z holds for x be Element of X, z be Element of Z holds ( rng ( min (R,S,x,z))) = the set of all ((R . [x, y]) "/\" (S . [y, z])) where y be Element of Y & ( rng ( min (R,S,x,z))) <> {}

    proof

      let X,Y,Z be non empty set;

      let R be RMembership_Func of X, Y;

      let S be RMembership_Func of Y, Z;

      let x be Element of X, z be Element of Z;

      set L = the set of all ((R . [x, y]) "/\" (S . [y, z])) where y be Element of Y;

      

       A1: Y = ( dom ( min (R,S,x,z))) & ( min (R,S,x,z)) is PartFunc of ( dom ( min (R,S,x,z))), ( rng ( min (R,S,x,z))) by FUNCT_2:def 1, RELSET_1: 4;

      for c be object holds c in L iff c in ( rng ( min (R,S,x,z)))

      proof

        let c be object;

        hereby

          assume c in L;

          then

          consider y be Element of Y such that

           A2: c = ((R . [x, y]) "/\" (S . [y, z]));

          c = (( min (R,S,x,z)) . y) by A2, FUZZY_4:def 2;

          hence c in ( rng ( min (R,S,x,z))) by A1, PARTFUN1: 4;

        end;

        assume c in ( rng ( min (R,S,x,z)));

        then

        consider y be Element of Y such that y in ( dom ( min (R,S,x,z))) and

         A3: c = (( min (R,S,x,z)) . y) by PARTFUN1: 3;

        c = ((R . [x, y]) "/\" (S . [y, z])) by A3, FUZZY_4:def 2;

        hence thesis;

      end;

      hence ( rng ( min (R,S,x,z))) = L by TARSKI: 2;

      thus ( rng ( min (R,S,x,z))) <> {} ;

    end;

    definition

      let X be non empty set;

      let R be RMembership_Func of X, X;

      :: original: transitive

      redefine

      :: LFUZZY_1:def7

      attr R is transitive means for x,y,z be Element of X holds ((R . [x, y]) "/\" (R . [y, z])) <<= (R . [x, z]);

      compatibility

      proof

        thus R is transitive iff for x,y,z be Element of X holds ((R . [x, y]) "/\" (R . [y, z])) <<= (R . [x, z])

        proof

          hereby

            assume R is transitive;

            then

             A1: (R (#) R) c= R;

            thus for x,y,z be Element of X holds ((R . [x, y]) "/\" (R . [y, z])) <<= (R . [x, z])

            proof

              let x,y,z be Element of X;

              ((R . (x,y)) "/\" (R . (y,z))) in the set of all ((R . (x,y9)) "/\" (R . (y9,z))) where y9 be Element of X;

              then ((R . (x,y)) "/\" (R . (y,z))) <<= ( "\/" ( the set of all ((R . (x,y9)) "/\" (R . (y9,z))) where y9 be Element of X,( RealPoset [. 0 , 1.]))) by YELLOW_2: 22;

              then ((R . (x,y)) "/\" (R . (y,z))) <<= ((R (#) R) . (x,z)) by LFUZZY_0: 22;

              then

               A2: ((R . (x,y)) "/\" (R . (y,z))) <= ((R (#) R) . (x,z)) by LFUZZY_0: 3;

              ((R (#) R) . (x,z)) <= (R . (x,z)) by A1;

              then ((R . [x, y]) "/\" (R . [y, z])) <= (R . [x, z]) by A2, XXREAL_0: 2;

              hence thesis by LFUZZY_0: 3;

            end;

          end;

          assume

           A3: for x,y,z be Element of X holds ((R . [x, y]) "/\" (R . [y, z])) <<= (R . [x, z]);

          thus (R (#) R) c= R

          proof

            let x,z be Element of X;

            set W = ( rng ( min (R,R,x,z)));

            for r be Real st r in W holds r <= (R . [x, z])

            proof

              let r be Real;

              assume r in W;

              then r in the set of all ((R . [x, y9]) "/\" (R . [y9, z])) where y9 be Element of X by Lm1;

              then

              consider y be Element of X such that

               A4: r = ((R . [x, y]) "/\" (R . [y, z]));

              ((R . [x, y]) "/\" (R . [y, z])) <<= (R . [x, z]) by A3;

              hence thesis by A4, LFUZZY_0: 3;

            end;

            then ( upper_bound W) <= (R . [x, z]) by SEQ_4: 144;

            hence thesis by FUZZY_4:def 3;

          end;

        end;

      end;

    end

    definition

      let X be non empty set;

      let R be RMembership_Func of X, X;

      :: LFUZZY_1:def8

      attr R is antisymmetric means for x,y be Element of X holds (R . (x,y)) <> 0 & (R . (y,x)) <> 0 implies x = y;

    end

    registration

      let X;

      cluster ( Imf (X,X)) -> symmetric transitive reflexive antisymmetric;

      coherence

      proof

        thus ( Imf (X,X)) is symmetric

        proof

          let x,y be Element of X;

          per cases ;

            suppose x = y;

            hence thesis;

          end;

            suppose

             A1: not x = y;

            

            hence (( Imf (X,X)) . (x,y)) = 0 by FUZZY_4: 25

            .= (( Imf (X,X)) . (y,x)) by A1, FUZZY_4: 25;

          end;

        end;

        thus ( Imf (X,X)) is transitive

        proof

          let x,y,z be Element of X;

          per cases ;

            suppose

             A2: x = z;

            thus thesis

            proof

              per cases ;

                suppose

                 A3: x = y;

                ((( Imf (X,X)) . [x, y]) "/\" (( Imf (X,X)) . [y, z])) = ( min ((( Imf (X,X)) . (x,y)),(( Imf (X,X)) . (y,z))))

                .= 1 by A2, A3, FUZZY_4: 25;

                then ((( Imf (X,X)) . (x,y)) "/\" (( Imf (X,X)) . (y,z))) <= (( Imf (X,X)) . (x,z)) by A2, FUZZY_4: 25;

                hence thesis by LFUZZY_0: 3;

              end;

                suppose

                 A4: not x = y;

                ((( Imf (X,X)) . [x, y]) "/\" (( Imf (X,X)) . [y, z])) = ( min ((( Imf (X,X)) . (x,y)),(( Imf (X,X)) . (y,z))))

                .= ( min ((( Imf (X,X)) . (x,y)), 0 )) by A2, A4, FUZZY_4: 25

                .= ( min ( 0 , 0 )) by A4, FUZZY_4: 25

                .= 0 ;

                then ((( Imf (X,X)) . (x,y)) "/\" (( Imf (X,X)) . (y,z))) <= (( Imf (X,X)) . (x,z)) by A2, FUZZY_4: 25;

                hence thesis by LFUZZY_0: 3;

              end;

            end;

          end;

            suppose

             A5: not x = z;

            thus thesis

            proof

              per cases ;

                suppose

                 A6: x = y;

                ((( Imf (X,X)) . [x, y]) "/\" (( Imf (X,X)) . [y, z])) = ( min ((( Imf (X,X)) . (x,y)),(( Imf (X,X)) . (y,z))))

                .= ( min ((( Imf (X,X)) . (x,y)), 0 )) by A5, A6, FUZZY_4: 25

                .= ( min (1, 0 )) by A6, FUZZY_4: 25

                .= 0 by XXREAL_0:def 9;

                then ((( Imf (X,X)) . (x,y)) "/\" (( Imf (X,X)) . (y,z))) <= (( Imf (X,X)) . (x,z)) by A5, FUZZY_4: 25;

                hence thesis by LFUZZY_0: 3;

              end;

                suppose

                 A7: x <> y;

                thus thesis

                proof

                  per cases ;

                    suppose

                     A8: y = z;

                    ((( Imf (X,X)) . [x, y]) "/\" (( Imf (X,X)) . [y, z])) = ( min ((( Imf (X,X)) . (x,y)),(( Imf (X,X)) . (y,z))))

                    .= ( min ((( Imf (X,X)) . (x,y)),1)) by A8, FUZZY_4: 25

                    .= ( min ( 0 ,1)) by A7, FUZZY_4: 25

                    .= 0 by XXREAL_0:def 9;

                    then ((( Imf (X,X)) . (x,y)) "/\" (( Imf (X,X)) . (y,z))) <= (( Imf (X,X)) . (x,z)) by A5, FUZZY_4: 25;

                    hence thesis by LFUZZY_0: 3;

                  end;

                    suppose

                     A9: y <> z;

                    ((( Imf (X,X)) . [x, y]) "/\" (( Imf (X,X)) . [y, z])) = ( min ((( Imf (X,X)) . (x,y)),(( Imf (X,X)) . (y,z))))

                    .= ( min ((( Imf (X,X)) . (x,y)), 0 )) by A9, FUZZY_4: 25

                    .= ( min ( 0 , 0 )) by A7, FUZZY_4: 25

                    .= 0 ;

                    then ((( Imf (X,X)) . (x,y)) "/\" (( Imf (X,X)) . (y,z))) <= (( Imf (X,X)) . (x,z)) by A5, FUZZY_4: 25;

                    hence thesis by LFUZZY_0: 3;

                  end;

                end;

              end;

            end;

          end;

        end;

        thus ( Imf (X,X)) is reflexive;

        thus for x,y be Element of X holds (( Imf (X,X)) . (x,y)) <> 0 & (( Imf (X,X)) . (y,x)) <> 0 implies x = y by FUZZY_4: 25;

      end;

    end

    registration

      let X;

      cluster reflexive transitive symmetric antisymmetric for RMembership_Func of X, X;

      existence

      proof

        take ( Imf (X,X));

        thus thesis;

      end;

    end

    theorem :: LFUZZY_1:9

    

     Th9: for R,S be RMembership_Func of X, X holds R is symmetric & S is symmetric implies ( converse ( min (R,S))) = ( min (R,S)) by FUZZY_4: 8;

    theorem :: LFUZZY_1:10

    

     Th10: for R,S be RMembership_Func of X, X holds R is symmetric & S is symmetric implies ( converse ( max (R,S))) = ( max (R,S)) by FUZZY_4: 7;

    registration

      let X;

      let R,S be symmetric RMembership_Func of X, X;

      cluster ( min (R,S)) -> symmetric;

      coherence by Th9;

      cluster ( max (R,S)) -> symmetric;

      coherence by Th10;

    end

    theorem :: LFUZZY_1:11

    

     Th11: for R,S be RMembership_Func of X, X holds R is transitive & S is transitive implies (( min (R,S)) (#) ( min (R,S))) c= ( min (R,S))

    proof

      let R,S be RMembership_Func of X, X;

      assume that

       A1: R is transitive and

       A2: S is transitive;

      let x be Element of X, y be Element of X;

      (( min ((R (#) S),(S (#) S))) . [x, y]) = ( min (((S (#) S) . [x, y]),((R (#) S) . [x, y]))) by FUZZY_1:def 3;

      then

       A3: (( min ((R (#) S),(S (#) S))) . [x, y]) <= ((S (#) S) . [x, y]) by XXREAL_0: 17;

      (S (#) S) c= S by A2;

      then ((S (#) S) . (x,y)) <= (S . (x,y));

      then

       A4: (( min ((R (#) S),(S (#) S))) . [x, y]) <= (S . [x, y]) by A3, XXREAL_0: 2;

      (( min ((R (#) R),(S (#) R))) . [x, y]) = ( min (((R (#) R) . [x, y]),((S (#) R) . [x, y]))) by FUZZY_1:def 3;

      then

       A5: (( min ((R (#) R),(S (#) R))) . [x, y]) <= ((R (#) R) . [x, y]) by XXREAL_0: 17;

      (R (#) R) c= R by A1;

      then ((R (#) R) . (x,y)) <= (R . (x,y));

      then (( min ((R (#) R),(S (#) R))) . [x, y]) <= (R . [x, y]) by A5, XXREAL_0: 2;

      then

       A6: ( min ((( min ((R (#) R),(S (#) R))) . [x, y]),(( min ((R (#) S),(S (#) S))) . [x, y]))) <= ( min ((R . [x, y]),(S . [x, y]))) by A4, XXREAL_0: 18;

      (( min (R,S)) (#) ( min (R,S))) c= ( min ((( min (R,S)) (#) R),(( min (R,S)) (#) S))) by FUZZY_4: 15;

      then

       A7: ((( min (R,S)) (#) ( min (R,S))) . [x, y]) <= (( min ((( min (R,S)) (#) R),(( min (R,S)) (#) S))) . [x, y]);

      (( min (R,S)) (#) S) c= ( min ((R (#) S),(S (#) S))) by FUZZY_4: 16;

      then

       A8: ((( min (R,S)) (#) S) . [x, y]) <= (( min ((R (#) S),(S (#) S))) . [x, y]);

      (( min (R,S)) (#) R) c= ( min ((R (#) R),(S (#) R))) by FUZZY_4: 16;

      then (( min ((( min (R,S)) (#) R),(( min (R,S)) (#) S))) . [x, y]) = ( min (((( min (R,S)) (#) R) . [x, y]),((( min (R,S)) (#) S) . [x, y]))) & ((( min (R,S)) (#) R) . [x, y]) <= (( min ((R (#) R),(S (#) R))) . [x, y]) by FUZZY_1:def 3;

      then (( min ((( min (R,S)) (#) R),(( min (R,S)) (#) S))) . [x, y]) <= ( min ((( min ((R (#) R),(S (#) R))) . [x, y]),(( min ((R (#) S),(S (#) S))) . [x, y]))) by A8, XXREAL_0: 18;

      then ((( min (R,S)) (#) ( min (R,S))) . [x, y]) <= ( min ((( min ((R (#) R),(S (#) R))) . [x, y]),(( min ((R (#) S),(S (#) S))) . [x, y]))) by A7, XXREAL_0: 2;

      then ((( min (R,S)) (#) ( min (R,S))) . [x, y]) <= ( min ((R . [x, y]),(S . [x, y]))) by A6, XXREAL_0: 2;

      hence thesis by FUZZY_1:def 3;

    end;

    registration

      let X;

      let R,S be transitive RMembership_Func of X, X;

      cluster ( min (R,S)) -> transitive;

      coherence by Th11;

    end

    definition

      let A be set, X be non empty set;

      :: original: chi

      redefine

      func chi (A,X) -> Membership_Func of X ;

      coherence

      proof

        ( dom ( chi (A,X))) = X by FUNCT_3:def 3;

        hence ( chi (A,X)) is Membership_Func of X by FUNCT_2:def 1;

      end;

    end

    theorem :: LFUZZY_1:12

    for r be Relation of X st r is_reflexive_in X holds ( chi (r, [:X, X:])) is reflexive

    proof

      let r be Relation of X;

      assume

       A1: r is_reflexive_in X;

      for x be Element of X holds (( chi (r, [:X, X:])) . (x,x)) = 1

      proof

        let x be Element of X;

         [x, x] in r by A1, RELAT_2:def 1;

        hence thesis by FUNCT_3:def 3;

      end;

      hence thesis;

    end;

    theorem :: LFUZZY_1:13

    for r be Relation of X st r is antisymmetric holds ( chi (r, [:X, X:])) is antisymmetric

    proof

      let r be Relation of X;

      assume r is antisymmetric;

      then

       A1: r is_antisymmetric_in ( field r) by RELAT_2:def 12;

      for x,y be Element of X holds (( chi (r, [:X, X:])) . (x,y)) <> 0 & (( chi (r, [:X, X:])) . (y,x)) <> 0 implies x = y

      proof

        let x,y be Element of X;

        assume that

         A2: (( chi (r, [:X, X:])) . (x,y)) <> 0 and

         A3: (( chi (r, [:X, X:])) . (y,x)) <> 0 ;

        

         A4: x in ( field r) & y in ( field r) & [x, y] in r & [y, x] in r implies x = y by A1, RELAT_2:def 4;

         [x, y] in r by A2, FUNCT_3:def 3;

        hence thesis by A3, A4, FUNCT_3:def 3, RELAT_1: 15;

      end;

      hence thesis;

    end;

    theorem :: LFUZZY_1:14

    for r be Relation of X st r is symmetric holds ( chi (r, [:X, X:])) is symmetric

    proof

      let r be Relation of X;

      assume r is symmetric;

      then

       A1: r is_symmetric_in ( field r) by RELAT_2:def 11;

      let x,y be Element of X;

      

       A2: x in ( field r) & y in ( field r) & [x, y] in r implies [y, x] in r by A1, RELAT_2:def 3;

      

       A3: x in ( field r) & y in ( field r) & [y, x] in r implies [x, y] in r by A1, RELAT_2:def 3;

      per cases ;

        suppose

         A4: [x, y] in r;

        then (( chi (r, [:X, X:])) . [x, y]) = 1 by FUNCT_3:def 3;

        hence thesis by A2, A4, FUNCT_3:def 3, RELAT_1: 15;

      end;

        suppose not [x, y] in r;

        then ( not [y, x] in r) & (( chi (r, [:X, X:])) . [x, y]) = 0 by A3, FUNCT_3:def 3, RELAT_1: 15;

        hence thesis by FUNCT_3:def 3;

      end;

    end;

    theorem :: LFUZZY_1:15

    for r be Relation of X st r is transitive holds ( chi (r, [:X, X:])) is transitive

    proof

      let r be Relation of X;

      assume

       A1: r is transitive;

      let x,y,z be Element of X;

      r is_transitive_in ( field r) by A1, RELAT_2:def 16;

      then

       A2: x in ( field r) & y in ( field r) & z in ( field r) & [x, y] in r & [y, z] in r implies [x, z] in r by RELAT_2:def 8;

      per cases ;

        suppose

         A3: [x, y] in r;

        thus thesis

        proof

          per cases ;

            suppose

             A4: [y, z] in r;

            ((( chi (r, [:X, X:])) . [x, y]) "/\" (( chi (r, [:X, X:])) . [y, z])) = ( min (1,(( chi (r, [:X, X:])) . [y, z]))) by A3, FUNCT_3:def 3

            .= ( min (1,1)) by A4, FUNCT_3:def 3

            .= (( chi (r, [:X, X:])) . [x, z]) by A2, A3, A4, FUNCT_3:def 3, RELAT_1: 15;

            hence thesis by LFUZZY_0: 3;

          end;

            suppose

             A5: not [y, z] in r;

            ((( chi (r, [:X, X:])) . [x, y]) "/\" (( chi (r, [:X, X:])) . [y, z])) = ( min (1,(( chi (r, [:X, X:])) . [y, z]))) by A3, FUNCT_3:def 3

            .= ( min (1, 0 )) by A5, FUNCT_3:def 3

            .= 0 by XXREAL_0:def 9;

            then ((( chi (r, [:X, X:])) . [x, y]) "/\" (( chi (r, [:X, X:])) . [y, z])) <= (( chi (r, [:X, X:])) . [x, z]) by FUZZY_2: 1;

            hence thesis by LFUZZY_0: 3;

          end;

        end;

      end;

        suppose

         A6: not [x, y] in r;

        thus thesis

        proof

          per cases ;

            suppose

             A7: [y, z] in r;

            ((( chi (r, [:X, X:])) . [x, y]) "/\" (( chi (r, [:X, X:])) . [y, z])) = ( min ( 0 ,(( chi (r, [:X, X:])) . [y, z]))) by A6, FUNCT_3:def 3

            .= ( min ( 0 ,1)) by A7, FUNCT_3:def 3

            .= 0 by XXREAL_0:def 9;

            then ((( chi (r, [:X, X:])) . [x, y]) "/\" (( chi (r, [:X, X:])) . [y, z])) <= (( chi (r, [:X, X:])) . [x, z]) by FUZZY_2: 1;

            hence thesis by LFUZZY_0: 3;

          end;

            suppose

             A8: not [y, z] in r;

            ((( chi (r, [:X, X:])) . [x, y]) "/\" (( chi (r, [:X, X:])) . [y, z])) = ( min ( 0 ,(( chi (r, [:X, X:])) . [y, z]))) by A6, FUNCT_3:def 3

            .= ( min ( 0 , 0 )) by A8, FUNCT_3:def 3

            .= 0 ;

            then ((( chi (r, [:X, X:])) . [x, y]) "/\" (( chi (r, [:X, X:])) . [y, z])) <= (( chi (r, [:X, X:])) . [x, z]) by FUZZY_2: 1;

            hence thesis by LFUZZY_0: 3;

          end;

        end;

      end;

    end;

    theorem :: LFUZZY_1:16

    ( Zmf (X,X)) is symmetric antisymmetric transitive

    proof

      thus ( Zmf (X,X)) is symmetric

      proof

        let x,y be Element of X;

        (( Zmf (X,X)) . [x, y]) = 0 & (( Zmf (X,X)) . [y, x]) = 0 by FUZZY_4: 21;

        hence thesis;

      end;

      thus ( Zmf (X,X)) is antisymmetric

      proof

        let x,y be Element of X;

        (( Zmf (X,X)) . [x, y]) = 0 by FUZZY_4: 21;

        hence thesis;

      end;

      thus ( Zmf (X,X)) is transitive

      proof

        let x,y,z be Element of X;

        

         A1: (( Zmf (X,X)) . [x, z]) = 0 by FUZZY_4: 20;

        ((( Zmf (X,X)) . [x, y]) "/\" (( Zmf (X,X)) . [y, z])) = ( min ( 0 ,(( Zmf (X,X)) . [y, z]))) by FUZZY_4: 20

        .= ( min ( 0 , 0 )) by FUZZY_4: 20

        .= 0 ;

        hence thesis by A1, LFUZZY_0: 3;

      end;

    end;

    theorem :: LFUZZY_1:17

    ( Umf (X,X)) is symmetric transitive reflexive

    proof

      thus ( Umf (X,X)) is symmetric

      proof

        let x,y be Element of X;

        

        thus (( Umf (X,X)) . (x,y)) = (( Umf (X,X)) . [x, y])

        .= 1 by FUZZY_4: 21

        .= (( Umf (X,X)) . [y, x]) by FUZZY_4: 21

        .= (( Umf (X,X)) . (y,x));

      end;

      thus ( Umf (X,X)) is transitive

      proof

        let x,y,z be Element of X;

        ((( Umf (X,X)) . [x, y]) "/\" (( Umf (X,X)) . [y, z])) = ( min (1,(( Umf (X,X)) . [y, z]))) by FUZZY_4: 20

        .= ( min (1,1)) by FUZZY_4: 20

        .= 1;

        then ((( Umf (X,X)) . [x, y]) "/\" (( Umf (X,X)) . [y, z])) <= (( Umf (X,X)) . [x, z]) by FUZZY_4: 20;

        hence thesis by LFUZZY_0: 3;

      end;

      thus ( Umf (X,X)) is reflexive

      proof

        let x be Element of X;

        (( Umf (X,X)) . [x, x]) = 1 by FUZZY_4: 21;

        hence thesis;

      end;

    end;

    theorem :: LFUZZY_1:18

    for R be RMembership_Func of X, X holds ( max (R,( converse R))) is symmetric

    proof

      let R be RMembership_Func of X, X;

      set S = ( max (R,( converse R)));

      let x,y be Element of X;

      

      thus (S . (x,y)) = (S . [x, y])

      .= ( max ((R . (x,y)),(( converse R) . (x,y)))) by FUZZY_1:def 4

      .= ( max ((R . (x,y)),(R . (y,x)))) by FUZZY_4: 26

      .= ( max ((( converse R) . (y,x)),(R . (y,x)))) by FUZZY_4: 26

      .= (S . [y, x]) by FUZZY_1:def 4

      .= (S . (y,x));

    end;

    theorem :: LFUZZY_1:19

    for R be RMembership_Func of X, X holds ( min (R,( converse R))) is symmetric

    proof

      let R be RMembership_Func of X, X;

      set S = ( min (R,( converse R)));

      let x,y be Element of X;

      

      thus (S . (x,y)) = (S . [x, y])

      .= ( min ((R . (x,y)),(( converse R) . (x,y)))) by FUZZY_1:def 3

      .= ( min ((R . (x,y)),(R . (y,x)))) by FUZZY_4: 26

      .= ( min ((( converse R) . (y,x)),(R . (y,x)))) by FUZZY_4: 26

      .= (S . [y, x]) by FUZZY_1:def 3

      .= (S . (y,x));

    end;

    theorem :: LFUZZY_1:20

    for R be RMembership_Func of X, X holds for R9 be RMembership_Func of X, X st R9 is symmetric & R c= R9 holds ( max (R,( converse R))) c= R9

    proof

      let R be RMembership_Func of X, X;

      let T be RMembership_Func of X, X;

      assume that

       A1: T is symmetric and

       A2: R c= T;

      let x,y be Element of X;

      (R . [y, x]) <= (T . [y, x]) by A2;

      then (R . (y,x)) <= (T . (y,x));

      then

       A3: (R . (y,x)) <= (T . (x,y)) by A1;

      (R . [x, y]) <= (T . [x, y]) by A2;

      then ( max ((R . (x,y)),(R . (y,x)))) <= (T . (x,y)) by A3, XXREAL_0: 28;

      then ( max ((R . (x,y)),(( converse R) . (x,y)))) <= (T . (x,y)) by FUZZY_4: 26;

      then ( max ((R . [x, y]),(( converse R) . [x, y]))) <= (T . [x, y]);

      hence thesis by FUZZY_1:def 4;

    end;

    theorem :: LFUZZY_1:21

    for R be RMembership_Func of X, X holds for R9 be RMembership_Func of X, X st R9 is symmetric & R9 c= R holds R9 c= ( min (R,( converse R)))

    proof

      let R be RMembership_Func of X, X;

      let T be RMembership_Func of X, X;

      assume that

       A1: T is symmetric and

       A2: T c= R;

      let x,y be Element of X;

      (T . [y, x]) <= (R . [y, x]) by A2;

      then (T . (y,x)) <= (R . (y,x));

      then

       A3: (T . (x,y)) <= (R . (y,x)) by A1;

      (T . [x, y]) <= (R . [x, y]) by A2;

      then (T . (x,y)) <= ( min ((R . (x,y)),(R . (y,x)))) by A3, XXREAL_0: 20;

      then (T . (x,y)) <= ( min ((R . (x,y)),(( converse R) . (x,y)))) by FUZZY_4: 26;

      then (T . [x, y]) <= ( min ((R . [x, y]),(( converse R) . [x, y])));

      hence thesis by FUZZY_1:def 3;

    end;

    begin

    definition

      let X be non empty set;

      let R be RMembership_Func of X, X;

      let n be Nat;

      :: LFUZZY_1:def9

      func n iter R -> RMembership_Func of X, X means

      : Def9: ex F be sequence of ( Funcs ( [:X, X:], [. 0 , 1.])) st it = (F . n) & (F . 0 ) = ( Imf (X,X)) & for k be Nat holds ex Q be RMembership_Func of X, X st (F . k) = Q & (F . (k + 1)) = (Q (#) R);

      existence

      proof

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

        set D = the carrier of ( FuzzyLattice [:X, X:]);

        defpred P[ set, set, set] means ex Q be Element of D st $2 = Q & $3 = (( @ Q) (#) R);

        

         A1: for k be Nat holds for x be Element of D holds ex y be Element of D st P[k, x, y]

        proof

          let k be Nat;

          let Q be Element of D;

          set y = (( @ Q) (#) R);

          reconsider y9 = (( [:X, X:],y) @ ) as Element of D;

          take y9;

          thus thesis by LFUZZY_0:def 6;

        end;

        consider F be sequence of D such that

         A2: (F . 0 ) = (( [:X, X:],( Imf (X,X))) @ ) & for k be Nat holds P[k, (F . k), (F . (k + 1))] from RECDEF_1:sch 2( A1);

        reconsider F as sequence of ( Funcs ( [:X, X:], [. 0 , 1.])) by LFUZZY_0: 14;

        reconsider IT = (F . n9) as Element of ( FuzzyLattice [:X, X:]) by LFUZZY_0: 14;

        reconsider IT9 = ( @ IT) as RMembership_Func of X, X;

        take IT9;

        thus ex F be sequence of ( Funcs ( [:X, X:], [. 0 , 1.])) st IT9 = (F . n) & (F . 0 ) = ( Imf (X,X)) & for k be Nat holds ex Q be RMembership_Func of X, X st (F . k) = Q & (F . (k + 1)) = (Q (#) R)

        proof

          take F;

          thus IT9 = (F . n) by LFUZZY_0:def 5;

          thus (F . 0 ) = ( Imf (X,X)) by A2, LFUZZY_0:def 6;

          thus for k be Nat holds ex Q be RMembership_Func of X, X st (F . k) = Q & (F . (k + 1)) = (Q (#) R)

          proof

            let k be Nat;

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

            reconsider Q9 = (F . n) as Element of D by LFUZZY_0: 14;

            reconsider Q = ( @ Q9) as RMembership_Func of X, X;

            take Q;

            thus (F . k) = Q by LFUZZY_0:def 5;

             P[n, (F . n), (F . (n + 1))] by A2;

            hence thesis;

          end;

        end;

      end;

      uniqueness

      proof

        let S,T be RMembership_Func of X, X;

        given F be sequence of ( Funcs ( [:X, X:], [. 0 , 1.])) such that

         A3: S = (F . n) and

         A4: (F . 0 ) = ( Imf (X,X)) and

         A5: for k be Nat holds ex Q be RMembership_Func of X, X st (F . k) = Q & (F . (k + 1)) = (Q (#) R);

        given G be sequence of ( Funcs ( [:X, X:], [. 0 , 1.])) such that

         A6: T = (G . n) and

         A7: (G . 0 ) = ( Imf (X,X)) and

         A8: for k be Nat holds ex Q be RMembership_Func of X, X st (G . k) = Q & (G . (k + 1)) = (Q (#) R);

        defpred P[ Nat] means (F . $1) = (G . $1);

        

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

        proof

          let k be Nat;

          assume

           A10: (F . k) = (G . k);

          (ex Q be RMembership_Func of X, X st (G . k) = Q & (G . (k + 1)) = (Q (#) R)) & ex Q9 be RMembership_Func of X, X st (F . k) = Q9 & (F . (k + 1)) = (Q9 (#) R) by A5, A8;

          hence thesis by A10;

        end;

        

         A11: P[ 0 ] by A4, A7;

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

        hence S = T by A3, A6;

      end;

    end

    reserve X for non empty set;

    reserve R for RMembership_Func of X, X;

    theorem :: LFUZZY_1:22

    

     Th22: (( Imf (X,X)) (#) R) = R

    proof

      

       A1: for x,y be object st [x, y] in ( dom (( Imf (X,X)) (#) R)) holds ((( Imf (X,X)) (#) R) . (x,y)) = (R . (x,y))

      proof

        let x,y be object;

        assume [x, y] in ( dom (( Imf (X,X)) (#) R));

        then

        reconsider x, y as Element of X by ZFMISC_1: 87;

        set S = the set of all ((( Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z be Element of X;

        for c be Element of ( RealPoset [. 0 , 1.]) st c in S holds c <<= (R . [x, y])

        proof

          let c be Element of ( RealPoset [. 0 , 1.]);

          assume c in S;

          then

          consider z be Element of X such that

           A2: c = ((( Imf (X,X)) . (x,z)) "/\" (R . (z,y)));

          per cases ;

            suppose

             A3: x = z;

            

             A4: (R . (z,y)) <= 1 by FUZZY_4: 4;

            c = ( min ((R . [z, y]),1)) by A2, A3, FUZZY_4: 25

            .= (R . [x, y]) by A3, A4, XXREAL_0:def 9;

            hence thesis by LFUZZY_0: 3;

          end;

            suppose

             A5: x <> z;

            

             A6: 0 <= (R . (z,y)) by FUZZY_4: 4;

            c = ( min ((R . [z, y]), 0 )) by A2, A5, FUZZY_4: 25

            .= 0 by A6, XXREAL_0:def 9;

            then c <= (R . (x,y)) by FUZZY_4: 4;

            hence thesis by LFUZZY_0: 3;

          end;

        end;

        then

         A7: ((( Imf (X,X)) (#) R) . (x,y)) = ( "\/" ( the set of all ((( Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z be Element of X,( RealPoset [. 0 , 1.]))) & (R . (x,y)) is_>=_than S by LATTICE3:def 9, LFUZZY_0: 22;

        for b be Element of ( RealPoset [. 0 , 1.]) st b is_>=_than S holds (R . (x,y)) <<= b

        proof

          let b be Element of ( RealPoset [. 0 , 1.]);

          

           A8: (R . (x,y)) <= 1 by FUZZY_4: 4;

          ((( Imf (X,X)) . (x,x)) "/\" (R . [x, y])) = ( min (1,(R . (x,y)))) by FUZZY_4: 25

          .= (R . [x, y]) by A8, XXREAL_0:def 9;

          then

           A9: (R . (x,y)) in S;

          assume b is_>=_than S;

          hence thesis by A9, LATTICE3:def 9;

        end;

        hence thesis by A7, YELLOW_0: 32;

      end;

      ( dom (( Imf (X,X)) (#) R)) = [:X, X:] by FUNCT_2:def 1

      .= ( dom R) by FUNCT_2:def 1;

      hence thesis by A1, BINOP_1: 20;

    end;

    theorem :: LFUZZY_1:23

    

     Th23: (R (#) ( Imf (X,X))) = R

    proof

      

       A1: for x,y be object st [x, y] in ( dom (R (#) ( Imf (X,X)))) holds ((R (#) ( Imf (X,X))) . (x,y)) = (R . (x,y))

      proof

        let x,y be object;

        assume [x, y] in ( dom (R (#) ( Imf (X,X))));

        then

        reconsider x, y as Element of X by ZFMISC_1: 87;

        set S = the set of all ((R . (x,z)) "/\" (( Imf (X,X)) . (z,y))) where z be Element of X;

        for c be Element of ( RealPoset [. 0 , 1.]) st c in S holds c <<= (R . [x, y])

        proof

          let c be Element of ( RealPoset [. 0 , 1.]);

          assume c in S;

          then

          consider z be Element of X such that

           A2: c = ((R . (x,z)) "/\" (( Imf (X,X)) . (z,y)));

          per cases ;

            suppose

             A3: y = z;

            

             A4: (R . (x,z)) <= 1 by FUZZY_4: 4;

            c = ( min ((R . [x, z]),1)) by A2, A3, FUZZY_4: 25

            .= (R . [x, y]) by A3, A4, XXREAL_0:def 9;

            hence thesis by LFUZZY_0: 3;

          end;

            suppose

             A5: not y = z;

            

             A6: 0 <= (R . (x,z)) by FUZZY_4: 4;

            c = ( min ((R . [x, z]), 0 )) by A2, A5, FUZZY_4: 25

            .= 0 by A6, XXREAL_0:def 9;

            then c <= (R . (x,y)) by FUZZY_4: 4;

            hence thesis by LFUZZY_0: 3;

          end;

        end;

        then

         A7: ((R (#) ( Imf (X,X))) . (x,y)) = ( "\/" ( the set of all ((R . (x,z)) "/\" (( Imf (X,X)) . (z,y))) where z be Element of X,( RealPoset [. 0 , 1.]))) & (R . (x,y)) is_>=_than S by LATTICE3:def 9, LFUZZY_0: 22;

        for b be Element of ( RealPoset [. 0 , 1.]) st b is_>=_than S holds (R . (x,y)) <<= b

        proof

          let b be Element of ( RealPoset [. 0 , 1.]);

          

           A8: (R . (x,y)) <= 1 by FUZZY_4: 4;

          ((R . [x, y]) "/\" (( Imf (X,X)) . (y,y))) = ( min ((R . [x, y]),1)) by FUZZY_4: 25

          .= (R . [x, y]) by A8, XXREAL_0:def 9;

          then

           A9: (R . (x,y)) in S;

          assume b is_>=_than S;

          hence thesis by A9, LATTICE3:def 9;

        end;

        hence thesis by A7, YELLOW_0: 32;

      end;

      ( dom (R (#) ( Imf (X,X)))) = [:X, X:] by FUNCT_2:def 1

      .= ( dom R) by FUNCT_2:def 1;

      hence thesis by A1, BINOP_1: 20;

    end;

    theorem :: LFUZZY_1:24

    

     Th24: ( 0 iter R) = ( Imf (X,X))

    proof

      ex F be sequence of ( Funcs ( [:X, X:], [. 0 , 1.])) st ( 0 iter R) = (F . 0 ) & (F . 0 ) = ( Imf (X,X)) & for k be Nat holds ex Q be RMembership_Func of X, X st (F . k) = Q & (F . (k + 1)) = (Q (#) R) by Def9;

      hence thesis;

    end;

    theorem :: LFUZZY_1:25

    

     Th25: (1 iter R) = R

    proof

      consider F be sequence of ( Funcs ( [:X, X:], [. 0 , 1.])) such that

       A1: (1 iter R) = (F . 1) & (F . 0 ) = ( Imf (X,X)) and

       A2: for k be Nat holds ex Q be RMembership_Func of X, X st (F . k) = Q & (F . (k + 1)) = (Q (#) R) by Def9;

      ex Q be RMembership_Func of X, X st (F . 0 ) = Q & (F . ( 0 + 1)) = (Q (#) R) by A2;

      hence thesis by A1, Th22;

    end;

    theorem :: LFUZZY_1:26

    

     Th26: for n be Nat holds ((n + 1) iter R) = ((n iter R) (#) R)

    proof

      let n be Nat;

      consider f be sequence of ( Funcs ( [:X, X:], [. 0 , 1.])) such that

       A1: ((n + 1) iter R) = (f . (n + 1)) & (f . 0 ) = ( Imf (X,X)) and

       A2: for k be Nat holds ex Q be RMembership_Func of X, X st (f . k) = Q & (f . (k + 1)) = (Q (#) R) by Def9;

      ex Q be RMembership_Func of X, X st (f . n) = Q & (f . (n + 1)) = (Q (#) R) by A2;

      hence thesis by A1, A2, Def9;

    end;

    theorem :: LFUZZY_1:27

    

     Th27: for m,n be Nat holds ((m + n) iter R) = ((m iter R) (#) (n iter R))

    proof

      let m,n be Nat;

      defpred P[ Nat] means ((m + $1) iter R) = ((m iter R) (#) ($1 iter R));

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: ((m + n) iter R) = ((m iter R) (#) (n iter R));

        

        thus ((m iter R) (#) ((n + 1) iter R)) = ((m iter R) (#) ((n iter R) (#) R)) by Th26

        .= (((m + n) iter R) (#) R) by A2, LFUZZY_0: 23

        .= (((m + n) + 1) iter R) by Th26

        .= ((m + (n + 1)) iter R);

      end;

      ((m iter R) (#) ( 0 iter R)) = ((m iter R) (#) ( Imf (X,X))) by Th24

      .= (m iter R) by Th23;

      then

       A3: P[ 0 ];

      for m be Nat holds P[m] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: LFUZZY_1:28

    for m,n be Nat holds ((m * n) iter R) = (m iter (n iter R))

    proof

      let m,n be Nat;

      defpred P[ Nat] means (($1 * n) iter R) = ($1 iter (n iter R));

      

       A1: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume

         A2: ((m * n) iter R) = (m iter (n iter R));

        

         A3: ((m + 1) iter (n iter R)) = ((m iter (n iter R)) (#) (1 iter (n iter R))) by Th27

        .= ((m iter (n iter R)) (#) (n iter R)) by Th25;

        (((m + 1) * n) iter R) = (((m * n) + (1 * n)) iter R)

        .= ((m iter (n iter R)) (#) (n iter R)) by A2, Th27;

        hence thesis by A3;

      end;

      (( 0 * n) iter R) = ( Imf (X,X)) by Th24

      .= ( 0 iter (n iter R)) by Th24;

      then

       A4: P[ 0 ];

      for m be Nat holds P[m] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    definition

      let X be non empty set;

      let R be RMembership_Func of X, X;

      :: LFUZZY_1:def10

      func TrCl R -> RMembership_Func of X, X equals ( "\/" ({ (n iter R) where n be Element of NAT : n > 0 },( FuzzyLattice [:X, X:])));

      coherence

      proof

        set S = ( "\/" ({ (n iter R) where n be Element of NAT : n > 0 },( FuzzyLattice [:X, X:])));

        S = ( @ S) by LFUZZY_0:def 5;

        hence thesis;

      end;

    end

    theorem :: LFUZZY_1:29

    

     Th29: for x,y be Element of X holds (( TrCl R) . [x, y]) = ( "\/" (( pi ({ (n iter R) where n be Element of NAT : n > 0 }, [x, y])),( RealPoset [. 0 , 1.])))

    proof

      set Q = { (n iter R) where n be Element of NAT : n > 0 };

      Q c= the carrier of ( FuzzyLattice [:X, X:])

      proof

        let t be object;

        assume t in Q;

        then ex n be Element of NAT st t = (n iter R) & n > 0 ;

        then

        reconsider t as Membership_Func of [:X, X:];

        (( [:X, X:],t) @ ) is Element of ( FuzzyLattice [:X, X:]);

        then

        reconsider t as Element of ( FuzzyLattice [:X, X:]) by LFUZZY_0:def 6;

        t in the carrier of ( FuzzyLattice [:X, X:]);

        hence thesis;

      end;

      then

      reconsider Q as Subset of ( FuzzyLattice [:X, X:]);

      let x,z be Element of X;

      reconsider i = [x, z] as Element of [:X, X:];

      

       A1: for a be Element of [:X, X:] holds (( [:X, X:] --> ( RealPoset [. 0 , 1.])) . a) is complete LATTICE by FUNCOP_1: 7;

      ( FuzzyLattice [:X, X:]) = (( RealPoset [. 0 , 1.]) |^ [:X, X:]) by LFUZZY_0:def 4

      .= ( product ( [:X, X:] --> ( RealPoset [. 0 , 1.]))) by YELLOW_1:def 5;

      then (( sup Q) . i) = ( "\/" (( pi (Q,i)),(( [:X, X:] --> ( RealPoset [. 0 , 1.])) . i))) by A1, WAYBEL_3: 32;

      hence thesis by FUNCOP_1: 7;

    end;

    theorem :: LFUZZY_1:30

    

     Th30: R c= ( TrCl R)

    proof

      for c be Element of [:X, X:] holds (R . c) <= (( TrCl R) . c)

      proof

        set Q = { (n iter R) where n be Element of NAT : n > 0 };

        let c be Element of [:X, X:];

        consider x,y be object such that

         A1: [x, y] = c by RELAT_1:def 1;

        reconsider x, y as Element of X by A1, ZFMISC_1: 87;

        R = (1 iter R) by Th25;

        then R in Q;

        then

         A2: (R . [x, y]) in ( pi (Q, [x, y])) by CARD_3:def 6;

        (( TrCl R) . [x, y]) = ( "\/" (( pi (Q, [x, y])),( RealPoset [. 0 , 1.]))) by Th29;

        then (R . [x, y]) <<= (( TrCl R) . [x, y]) by A2, YELLOW_2: 22;

        hence thesis by A1, LFUZZY_0: 3;

      end;

      hence thesis;

    end;

    theorem :: LFUZZY_1:31

    

     Th31: for n be Nat st n > 0 holds (n iter R) c= ( TrCl R)

    proof

      let n9 be Nat;

      assume

       A1: n9 > 0 ;

      for c be Element of [:X, X:] holds ((n9 iter R) . c) <= (( TrCl R) . c)

      proof

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

        set Q = { (n iter R) where n be Element of NAT : n > 0 };

        let c be Element of [:X, X:];

        consider x,y be object such that

         A2: [x, y] = c by RELAT_1:def 1;

        reconsider x, y as Element of X by A2, ZFMISC_1: 87;

        (n9 iter R) in Q by A1;

        then

         A3: ((n9 iter R) . [x, y]) in ( pi (Q, [x, y])) by CARD_3:def 6;

        (( TrCl R) . [x, y]) = ( "\/" (( pi (Q, [x, y])),( RealPoset [. 0 , 1.]))) by Th29;

        then ((n9 iter R) . [x, y]) <<= (( TrCl R) . [x, y]) by A3, YELLOW_2: 22;

        hence thesis by A2, LFUZZY_0: 3;

      end;

      hence thesis;

    end;

    theorem :: LFUZZY_1:32

    

     Th32: for Q be Subset of ( FuzzyLattice X), x be Element of X holds (( "\/" (Q,( FuzzyLattice X))) . x) = ( "\/" (( pi (Q,x)),( RealPoset [. 0 , 1.])))

    proof

      let Q be Subset of ( FuzzyLattice X);

      let x be Element of X;

      

       A1: for a be Element of X holds ((X --> ( RealPoset [. 0 , 1.])) . a) is complete LATTICE by FUNCOP_1: 7;

      ( FuzzyLattice X) = (( RealPoset [. 0 , 1.]) |^ X) by LFUZZY_0:def 4

      .= ( product (X --> ( RealPoset [. 0 , 1.]))) by YELLOW_1:def 5;

      then (( sup Q) . x) = ( "\/" (( pi (Q,x)),((X --> ( RealPoset [. 0 , 1.])) . x))) by A1, WAYBEL_3: 32;

      hence thesis by FUNCOP_1: 7;

    end;

    

     Lm2: for R be RMembership_Func of X, X, Q be Subset of ( FuzzyLattice [:X, X:]), x,z be Element of X holds the set of all ((R . (x,y)) "/\" (( @ ( "\/" (Q,( FuzzyLattice [:X, X:])))) . (y,z))) where y be Element of X = the set of all ((R . [x, y]) "/\" ( "\/" (( pi (Q, [y, z])),( RealPoset [. 0 , 1.])))) where y be Element of X

    proof

      let R be RMembership_Func of X, X;

      let Q be Subset of ( FuzzyLattice [:X, X:]);

      let x,z be Element of X;

      defpred P[ Element of X] means not contradiction;

      deffunc F( Element of X) = ((R . (x,$1)) "/\" (( @ ( "\/" (Q,( FuzzyLattice [:X, X:])))) . ($1,z)));

      deffunc G( Element of X) = ((R . [x, $1]) "/\" ( "\/" (( pi (Q, [$1, z])),( RealPoset [. 0 , 1.]))));

      for y be Element of X holds ((R . [x, y]) "/\" (( @ ( "\/" (Q,( FuzzyLattice [:X, X:])))) . [y, z])) = ((R . [x, y]) "/\" ( "\/" (( pi (Q, [y, z])),( RealPoset [. 0 , 1.]))))

      proof

        let y be Element of X;

        (( @ ( "\/" (Q,( FuzzyLattice [:X, X:])))) . [y, z]) = (( "\/" (Q,( FuzzyLattice [:X, X:]))) . [y, z]) by LFUZZY_0:def 5

        .= ( "\/" (( pi (Q, [y, z])),( RealPoset [. 0 , 1.]))) by Th32;

        hence thesis;

      end;

      then

       A1: for y be Element of X holds F(y) = G(y);

      thus { F(y) where y be Element of X : P[y] } = { G(y9) where y9 be Element of X : P[y9] } from FRAENKEL:sch 5( A1);

    end;

    theorem :: LFUZZY_1:33

    

     Th33: for R be complete Heyting LATTICE, X be Subset of R, y be Element of R holds (y "/\" ( "\/" (X,R))) = ( "\/" ({ (y "/\" x) where x be Element of R : x in X },R))

    proof

      let R be complete Heyting LATTICE, X be Subset of R, y be Element of R;

      for z be Element of R holds (z "/\" ) is lower_adjoint by WAYBEL_1:def 19;

      hence thesis by WAYBEL_1: 64;

    end;

    

     Lm3: for R be RMembership_Func of X, X, Q be Subset of ( FuzzyLattice [:X, X:]), x,z be Element of X holds the set of all ((R . [x, y]) "/\" ( "\/" (( pi (Q, [y, z])),( RealPoset [. 0 , 1.])))) where y be Element of X = the set of all ( "\/" ({ ((R . [x, y9]) "/\" b) where b be Element of ( RealPoset [. 0 , 1.]) : b in ( pi (Q, [y9, z])) },( RealPoset [. 0 , 1.]))) where y9 be Element of X

    proof

      let R be RMembership_Func of X, X;

      let Q be Subset of ( FuzzyLattice [:X, X:]);

      let x,z be Element of X;

      defpred P[ Element of X] means not contradiction;

      deffunc F( Element of X) = ((R . [x, $1]) "/\" ( "\/" (( pi (Q, [$1, z])),( RealPoset [. 0 , 1.]))));

      deffunc G( Element of X) = ( "\/" ({ ((R . [x, $1]) "/\" b) where b be Element of ( RealPoset [. 0 , 1.]) : b in ( pi (Q, [$1, z])) },( RealPoset [. 0 , 1.])));

      for y be Element of X holds ((R . [x, y]) "/\" ( "\/" (( pi (Q, [y, z])),( RealPoset [. 0 , 1.])))) = ( "\/" ({ ((R . [x, y]) "/\" b) where b be Element of ( RealPoset [. 0 , 1.]) : b in ( pi (Q, [y, z])) },( RealPoset [. 0 , 1.])))

      proof

        let y be Element of X;

        ( FuzzyLattice [:X, X:]) = (( RealPoset [. 0 , 1.]) |^ [:X, X:]) by LFUZZY_0:def 4

        .= ( product ( [:X, X:] --> ( RealPoset [. 0 , 1.]))) by YELLOW_1:def 5;

        then

        reconsider Q as Subset of ( product ( [:X, X:] --> ( RealPoset [. 0 , 1.])));

        ( pi (Q, [y, z])) is Subset of ( RealPoset [. 0 , 1.]) by FUNCOP_1: 7;

        hence thesis by Th33;

      end;

      then

       A1: for y be Element of X holds F(y) = G(y);

      { F(y) where y be Element of X : P[y] } = { G(y) where y be Element of X : P[y] } from FRAENKEL:sch 5( A1);

      hence thesis;

    end;

    

     Lm4: for R be RMembership_Func of X, X, Q be Subset of ( FuzzyLattice [:X, X:]), x,z be Element of X holds the set of all ( "\/" ({ ((R . [x, y]) "/\" b) where b be Element of ( RealPoset [. 0 , 1.]) : b in ( pi (Q, [y, z])) },( RealPoset [. 0 , 1.]))) where y be Element of X = the set of all ( "\/" ({ ((R . [x, y9]) "/\" (r . [y9, z])) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q },( RealPoset [. 0 , 1.]))) where y9 be Element of X

    proof

      let R be RMembership_Func of X, X;

      let Q be Subset of ( FuzzyLattice [:X, X:]);

      let x,z be Element of X;

      set RP = ( RealPoset [. 0 , 1.]), FL = ( FuzzyLattice [:X, X:]);

      defpred P[ Element of X] means not contradiction;

      deffunc F( Element of X) = ( "\/" ({ ((R . [x, $1]) "/\" b) where b be Element of RP : b in ( pi (Q, [$1, z])) },RP));

      deffunc G( Element of X) = ( "\/" ({ ((R . [x, $1]) "/\" (r . [$1, z])) where r be Element of FL : r in Q },RP));

      for y be Element of X holds ( "\/" ({ ((R . [x, y]) "/\" b) where b be Element of RP : b in ( pi (Q, [y, z])) },RP)) = ( "\/" ({ ((R . [x, y]) "/\" (r . [y, z])) where r be Element of FL : r in Q },RP))

      proof

        let y be Element of X;

        set A = { ((R . [x, y]) "/\" b) where b be Element of RP : b in ( pi (Q, [y, z])) }, B = { ((R . [x, y]) "/\" (r . [y, z])) where r be Element of FL : r in Q };

        

         A1: B c= A

        proof

          let a be object;

          assume a in B;

          then

          consider r be Element of FL such that

           A2: a = ((R . [x, y]) "/\" (r . [y, z])) and

           A3: r in Q;

          (r . [y, z]) in ( pi (Q, [y, z])) by A3, CARD_3:def 6;

          hence thesis by A2;

        end;

        A c= B

        proof

          let a be object;

          assume a in A;

          then

          consider b be Element of RP such that

           A4: a = ((R . [x, y]) "/\" b) and

           A5: b in ( pi (Q, [y, z]));

          ex f be Function st f in Q & b = (f . [y, z]) by A5, CARD_3:def 6;

          hence thesis by A4;

        end;

        hence thesis by A1, XBOOLE_0:def 10;

      end;

      then

       A6: for y be Element of X holds F(y) = G(y);

      thus { F(y) where y be Element of X : P[y] } = { G(y) where y be Element of X : P[y] } from FRAENKEL:sch 5( A6);

    end;

    

     Lm5: for X,Y,Z be non empty set holds for R be RMembership_Func of X, Y holds for S be RMembership_Func of Y, Z holds for x be Element of X, z be Element of Z holds ( rng ( min (R,S,x,z))) = the set of all ((R . [x, y]) "/\" (S . [y, z])) where y be Element of Y & ( rng ( min (R,S,x,z))) <> {}

    proof

      let X,Y,Z be non empty set;

      let R be RMembership_Func of X, Y;

      let S be RMembership_Func of Y, Z;

      let x be Element of X, z be Element of Z;

      set L = the set of all ((R . [x, y]) "/\" (S . [y, z])) where y be Element of Y;

      

       A1: Y = ( dom ( min (R,S,x,z))) & ( min (R,S,x,z)) is PartFunc of ( dom ( min (R,S,x,z))), ( rng ( min (R,S,x,z))) by FUNCT_2:def 1, RELSET_1: 4;

      for c be object holds c in L iff c in ( rng ( min (R,S,x,z)))

      proof

        let c be object;

        hereby

          assume c in L;

          then

          consider y be Element of Y such that

           A2: c = ((R . [x, y]) "/\" (S . [y, z]));

          c = (( min (R,S,x,z)) . y) by A2, FUZZY_4:def 2;

          hence c in ( rng ( min (R,S,x,z))) by A1, PARTFUN1: 4;

        end;

        assume c in ( rng ( min (R,S,x,z)));

        then

        consider y be Element of Y such that y in ( dom ( min (R,S,x,z))) and

         A3: c = (( min (R,S,x,z)) . y) by PARTFUN1: 3;

        c = ((R . [x, y]) "/\" (S . [y, z])) by A3, FUZZY_4:def 2;

        hence thesis;

      end;

      hence ( rng ( min (R,S,x,z))) = L by TARSKI: 2;

      thus ( rng ( min (R,S,x,z))) <> {} ;

    end;

    

     Lm6: for X,Y,Z be non empty set holds for R be RMembership_Func of X, Y holds for S be RMembership_Func of Y, Z holds for x be Element of X, z be Element of Z holds ((R (#) S) . [x, z]) = ( "\/" ( the set of all ((R . [x, y]) "/\" (S . [y, z])) where y be Element of Y,( RealPoset [. 0 , 1.])))

    proof

      let X,Y,Z be non empty set;

      let R be RMembership_Func of X, Y;

      let S be RMembership_Func of Y, Z;

      let x be Element of X, z be Element of Z;

      set L = the set of all ((R . [x, y]) "/\" (S . [y, z])) where y be Element of Y;

       [x, z] in [:X, Z:];

      then

       A1: ((R (#) S) . (x,z)) = ( upper_bound ( rng ( min (R,S,x,z)))) by FUZZY_4:def 3;

      

       A2: for b be Element of ( RealPoset [. 0 , 1.]) st b is_>=_than L holds ((R (#) S) . [x, z]) <<= b

      proof

        let b be Element of ( RealPoset [. 0 , 1.]);

        assume

         A3: b is_>=_than the set of all ((R . [x, y]) "/\" (S . [y, z])) where y be Element of Y;

        

         A4: ( rng ( min (R,S,x,z))) c= [. 0 , 1.] by RELAT_1:def 19;

        

         A5: L = ( rng ( min (R,S,x,z))) by Lm5;

        for r be Real st r in ( rng ( min (R,S,x,z))) holds r <= b

        proof

          let r be Real;

          assume

           A6: r in ( rng ( min (R,S,x,z)));

          then

          reconsider r as Element of ( RealPoset [. 0 , 1.]) by A4, LFUZZY_0:def 3;

          r <<= b by A3, A5, A6, LATTICE3:def 9;

          hence thesis by LFUZZY_0: 3;

        end;

        then ( upper_bound ( rng ( min (R,S,x,z)))) <= b by SEQ_4: 144;

        hence thesis by A1, LFUZZY_0: 3;

      end;

      for b be Element of ( RealPoset [. 0 , 1.]) st b in L holds ((R (#) S) . [x, z]) >>= b

      proof

        let b be Element of ( RealPoset [. 0 , 1.]);

        assume b in L;

        then

        consider y be Element of Y such that

         A7: b = ((R . [x, y]) "/\" (S . [y, z]));

        ( dom ( min (R,S,x,z))) = Y & b = (( min (R,S,x,z)) . y) by A7, FUNCT_2:def 1, FUZZY_4:def 2;

        then b <= ( upper_bound ( rng ( min (R,S,x,z)))) by FUZZY_4: 1;

        hence thesis by A1, LFUZZY_0: 3;

      end;

      then ((R (#) S) . [x, z]) is_>=_than L by LATTICE3:def 9;

      hence thesis by A2, YELLOW_0: 32;

    end;

    

     Lm7: for R be RMembership_Func of X, X, Q be Subset of ( FuzzyLattice [:X, X:]), x,z be Element of X holds { ( "\/" ( the set of all ((R . [x, y]) "/\" (r . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.]))) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q } = { ( "\/" ( the set of all ((R . [x, y]) "/\" (( @ r9) . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.]))) where r9 be Element of ( FuzzyLattice [:X, X:]) : r9 in Q }

    proof

      let R be RMembership_Func of X, X;

      let Q be Subset of ( FuzzyLattice [:X, X:]);

      let x,z be Element of X;

      set FL = ( FuzzyLattice [:X, X:]);

      defpred P[ Element of FL] means $1 in Q;

      deffunc F( Element of FL) = ( "\/" ( the set of all ((R . [x, y]) "/\" ($1 . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.])));

      deffunc G( Element of FL) = ( "\/" ( the set of all ((R . [x, y]) "/\" (( @ $1) . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.])));

      for r be Element of FL st r in Q holds ( "\/" ( the set of all ((R . [x, y]) "/\" (r . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.]))) = ( "\/" ( the set of all ((R . [x, y]) "/\" (( @ r) . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.])))

      proof

        let r be Element of FL;

        assume r in Q;

         the set of all ((R . [x, y]) "/\" (r . [y, z])) where y be Element of X = the set of all ((R . [x, y]) "/\" (( @ r) . [y, z])) where y be Element of X

        proof

          deffunc g( Element of X) = ((R . [x, $1]) "/\" (( @ r) . [$1, z]));

          deffunc f( Element of X) = ((R . [x, $1]) "/\" (r . [$1, z]));

          defpred P[ Element of X] means not contradiction;

          

           A1: for y be Element of X holds f(y) = g(y) by LFUZZY_0:def 5;

          thus { f(y) where y be Element of X : P[y] } = { g(y) where y be Element of X : P[y] } from FRAENKEL:sch 5( A1);

        end;

        hence thesis;

      end;

      then

       A2: for r be Element of FL st P[r] holds F(r) = G(r);

      thus { F(r) where r be Element of ( FuzzyLattice [:X, X:]) : P[r] } = { G(r) where r be Element of ( FuzzyLattice [:X, X:]) : P[r] } from FRAENKEL:sch 6( A2);

    end;

    

     Lm8: for R be RMembership_Func of X, X, Q be Subset of ( FuzzyLattice [:X, X:]), x,z be Element of X holds { ( "\/" ( the set of all ((R . [x, y]) "/\" (( @ r) . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.]))) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q } = { ((R (#) ( @ r)) . [x, z]) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q }

    proof

      let R be RMembership_Func of X, X;

      let Q be Subset of ( FuzzyLattice [:X, X:]);

      let x,z be Element of X;

      set FL = ( FuzzyLattice [:X, X:]);

      defpred P[ Element of FL] means $1 in Q;

      deffunc F( Element of FL) = ( "\/" ( the set of all ((R . [x, y]) "/\" (( @ $1) . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.])));

      deffunc G( Element of FL) = ((R (#) ( @ $1)) . [x, z]);

      

       A1: for r be Element of FL st P[r] holds F(r) = G(r) by Lm6;

      thus { F(r) where r be Element of ( FuzzyLattice [:X, X:]) : P[r] } = { G(r) where r be Element of ( FuzzyLattice [:X, X:]) : P[r] } from FRAENKEL:sch 6( A1);

    end;

    

     Lm9: for R be RMembership_Func of X, X, Q be Subset of ( FuzzyLattice [:X, X:]), x,z be Element of X holds { ((R (#) ( @ r)) . [x, z]) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q } = ( pi ({ (R (#) ( @ r)) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q }, [x, z]))

    proof

      let R be RMembership_Func of X, X;

      let Q be Subset of ( FuzzyLattice [:X, X:]);

      let x,z be Element of X;

      set FL = ( FuzzyLattice [:X, X:]), A = { ((R (#) ( @ r)) . [x, z]) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q }, B = ( pi ({ (R (#) ( @ r)) where r be Element of FL : r in Q }, [x, z]));

      thus A c= B

      proof

        let a be object;

        assume a in A;

        then

        consider r be Element of FL such that

         A1: a = ((R (#) ( @ r)) . [x, z]) and

         A2: r in Q;

        (R (#) ( @ r)) in { (R (#) ( @ r9)) where r9 be Element of FL : r9 in Q } by A2;

        hence thesis by A1, CARD_3:def 6;

      end;

      thus B c= A

      proof

        let b be object;

        assume b in B;

        then

        consider f be Function such that

         A3: f in { (R (#) ( @ r9)) where r9 be Element of FL : r9 in Q } and

         A4: b = (f . [x, z]) by CARD_3:def 6;

        ex r be Element of FL st f = (R (#) ( @ r)) & r in Q by A3;

        hence thesis by A4;

      end;

    end;

    

     Lm10: for R be RMembership_Func of X, X, Q be Subset of ( FuzzyLattice [:X, X:]), x,z be Element of X holds ( "\/" ( the set of all ( "\/" ({ ((R . [x, y]) "/\" (r . [y, z])) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q },( RealPoset [. 0 , 1.]))) where y be Element of X,( RealPoset [. 0 , 1.]))) = ( "\/" ({ ( "\/" ( the set of all ((R . [x, y]) "/\" (r9 . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.]))) where r9 be Element of ( FuzzyLattice [:X, X:]) : r9 in Q },( RealPoset [. 0 , 1.])))

    proof

      let R be RMembership_Func of X, X;

      let Q be Subset of ( FuzzyLattice [:X, X:]);

      let x,z be Element of X;

      set FL = ( FuzzyLattice [:X, X:]), RP = ( RealPoset [. 0 , 1.]);

      defpred P[ Element of X] means not contradiction;

      defpred Q[ Element of ( FuzzyLattice [:X, X:])] means $1 in Q;

      deffunc F( Element of X, Element of ( FuzzyLattice [:X, X:])) = ((R . [x, $1]) "/\" ($2 . [$1, z]));

      

       A1: for y be Element of X, r be Element of FL st P[y] & Q[r] holds F(y,r) = F(y,r);

      thus ( "\/" ({ ( "\/" ({ F(y,r) where r be Element of FL : Q[r] },RP)) where y be Element of X : P[y] },RP)) = ( "\/" ({ ( "\/" ({ F(y9,r9) where y9 be Element of X : P[y9] },RP)) where r9 be Element of FL : Q[r9] },RP)) from LFUZZY_0:sch 5( A1);

    end;

    theorem :: LFUZZY_1:34

    

     Th34: for R be RMembership_Func of X, X, Q be Subset of ( FuzzyLattice [:X, X:]) holds (R (#) ( @ ( "\/" (Q,( FuzzyLattice [:X, X:]))))) = ( "\/" ({ (R (#) ( @ r)) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q },( FuzzyLattice [:X, X:])))

    proof

      let R be RMembership_Func of X, X;

      let Q be Subset of ( FuzzyLattice [:X, X:]);

      set FL = ( FuzzyLattice [:X, X:]), RP = ( RealPoset [. 0 , 1.]);

      ( "\/" ({ (R (#) ( @ r)) where r be Element of FL : r in Q },FL)) = ( @ ( "\/" ({ (R (#) ( @ r)) where r be Element of FL : r in Q },FL))) by LFUZZY_0:def 5;

      then

      reconsider F = ( "\/" ({ (R (#) ( @ r)) where r be Element of FL : r in Q },FL)) as RMembership_Func of X, X;

      for x,z be Element of X holds ((R (#) ( @ ( "\/" (Q,FL)))) . (x,z)) = (F . (x,z))

      proof

        let x,z be Element of X;

        

         A1: { (R (#) ( @ r)) where r be Element of FL : r in Q } c= the carrier of ( FuzzyLattice [:X, X:])

        proof

          let t be object;

          assume t in { (R (#) ( @ r)) where r be Element of FL : r in Q };

          then

          consider r be Element of ( FuzzyLattice [:X, X:]) such that

           A2: t = (R (#) ( @ r)) and r in Q;

          (( [:X, X:],(R (#) ( @ r))) @ ) = (R (#) ( @ r)) by LFUZZY_0:def 6;

          hence thesis by A2;

        end;

        

        thus ((R (#) ( @ ( "\/" (Q,FL)))) . (x,z)) = ( "\/" ( the set of all ((R . (x,y)) "/\" (( @ ( "\/" (Q,FL))) . (y,z))) where y be Element of X,RP)) by LFUZZY_0: 22

        .= ( "\/" ( the set of all ((R . [x, y]) "/\" ( "\/" (( pi (Q, [y, z])),RP))) where y be Element of X,RP)) by Lm2

        .= ( "\/" ( the set of all ( "\/" ({ ((R . [x, y]) "/\" b) where b be Element of RP : b in ( pi (Q, [y, z])) },RP)) where y be Element of X,RP)) by Lm3

        .= ( "\/" ( the set of all ( "\/" ({ ((R . [x, y]) "/\" (r . [y, z])) where r be Element of FL : r in Q },RP)) where y be Element of X,RP)) by Lm4

        .= ( "\/" ({ ( "\/" ( the set of all ((R . [x, y]) "/\" (r . [y, z])) where y be Element of X,RP)) where r be Element of FL : r in Q },RP)) by Lm10

        .= ( "\/" ({ ( "\/" ( the set of all ((R . [x, y]) "/\" (( @ r) . [y, z])) where y be Element of X,RP)) where r be Element of FL : r in Q },RP)) by Lm7

        .= ( "\/" ({ ((R (#) ( @ r)) . [x, z]) where r be Element of FL : r in Q },RP)) by Lm8

        .= ( "\/" (( pi ({ (R (#) ( @ r)) where r be Element of FL : r in Q }, [x, z])),RP)) by Lm9

        .= (F . (x,z)) by A1, Th32;

      end;

      hence thesis by Th2;

    end;

    theorem :: LFUZZY_1:35

    

     Th35: for R be RMembership_Func of X, X, Q be Subset of ( FuzzyLattice [:X, X:]) holds (( @ ( "\/" (Q,( FuzzyLattice [:X, X:])))) (#) R) = ( "\/" ({ (( @ r) (#) R) where r be Element of ( FuzzyLattice [:X, X:]) : r in Q },( FuzzyLattice [:X, X:])))

    proof

      let R be RMembership_Func of X, X;

      let Q be Subset of ( FuzzyLattice [:X, X:]);

      set FL = ( FuzzyLattice [:X, X:]), RP = ( RealPoset [. 0 , 1.]);

      ( "\/" ({ (( @ r) (#) R) where r be Element of FL : r in Q },FL)) = ( @ ( "\/" ({ (( @ r) (#) R) where r be Element of FL : r in Q },FL))) by LFUZZY_0:def 5;

      then

      reconsider F = ( "\/" ({ (( @ r) (#) R) where r be Element of FL : r in Q },FL)) as RMembership_Func of X, X;

      for x,z be Element of X holds ((( @ ( "\/" (Q,FL))) (#) R) . (x,z)) = (F . (x,z))

      proof

        let x,z be Element of X;

        

         A1: { (( @ r) (#) R) where r be Element of FL : r in Q } c= the carrier of ( FuzzyLattice [:X, X:])

        proof

          let t be object;

          assume t in { (( @ r) (#) R) where r be Element of FL : r in Q };

          then

          consider r be Element of ( FuzzyLattice [:X, X:]) such that

           A2: t = (( @ r) (#) R) and r in Q;

          (( [:X, X:],(( @ r) (#) R)) @ ) = (( @ r) (#) R) by LFUZZY_0:def 6;

          hence thesis by A2;

        end;

        

         A3: the set of all (( "\/" (( pi (Q, [x, y])),RP)) "/\" (R . [y, z])) where y be Element of X = the set of all ( "\/" ({ (b "/\" (R . [y9, z])) where b be Element of RP : b in ( pi (Q, [x, y9])) },RP)) where y9 be Element of X

        proof

          deffunc G( Element of X) = ( "\/" ({ (b "/\" (R . [$1, z])) where b be Element of RP : b in ( pi (Q, [x, $1])) },RP));

          deffunc F( Element of X) = (( "\/" (( pi (Q, [x, $1])),RP)) "/\" (R . [$1, z]));

          defpred P[ Element of X] means not contradiction;

          for y be Element of X holds (( "\/" (( pi (Q, [x, y])),( RealPoset [. 0 , 1.]))) "/\" (R . [y, z])) = ( "\/" ({ (b "/\" (R . [y, z])) where b be Element of RP : b in ( pi (Q, [x, y])) },RP))

          proof

            ( FuzzyLattice [:X, X:]) = (( RealPoset [. 0 , 1.]) |^ [:X, X:]) by LFUZZY_0:def 4

            .= ( product ( [:X, X:] --> ( RealPoset [. 0 , 1.]))) by YELLOW_1:def 5;

            then

            reconsider Q as Subset of ( product ( [:X, X:] --> ( RealPoset [. 0 , 1.])));

            let y be Element of X;

            ( pi (Q, [x, y])) is Subset of ( RealPoset [. 0 , 1.]) by FUNCOP_1: 7;

            hence thesis by LFUZZY_0: 15;

          end;

          then

           A4: for y be Element of X holds F(y) = G(y);

          { F(y) where y be Element of X : P[y] } = { G(y9) where y9 be Element of X : P[y9] } from FRAENKEL:sch 5( A4);

          hence thesis;

        end;

        

         A5: the set of all ( "\/" ({ (b "/\" (R . [y, z])) where b be Element of RP : b in ( pi (Q, [x, y])) },RP)) where y be Element of X = the set of all ( "\/" ({ ((r . [x, y9]) "/\" (R . [y9, z])) where r be Element of FL : r in Q },RP)) where y9 be Element of X

        proof

          deffunc G( Element of X) = ( "\/" ({ ((r . [x, $1]) "/\" (R . [$1, z])) where r be Element of FL : r in Q },RP));

          deffunc F( Element of X) = ( "\/" ({ (b "/\" (R . [$1, z])) where b be Element of RP : b in ( pi (Q, [x, $1])) },RP));

          defpred P[ Element of X] means not contradiction;

          for y be Element of X holds ( "\/" ({ (b "/\" (R . [y, z])) where b be Element of RP : b in ( pi (Q, [x, y])) },RP)) = ( "\/" ({ ((r . [x, y]) "/\" (R . [y, z])) where r be Element of FL : r in Q },RP))

          proof

            let y be Element of X;

            set A = { (b "/\" (R . [y, z])) where b be Element of RP : b in ( pi (Q, [x, y])) }, B = { ((r . [x, y]) "/\" (R . [y, z])) where r be Element of FL : r in Q };

            

             A6: B c= A

            proof

              let a be object;

              assume a in B;

              then

              consider r be Element of FL such that

               A7: a = ((r . [x, y]) "/\" (R . [y, z])) and

               A8: r in Q;

              (r . [x, y]) in ( pi (Q, [x, y])) by A8, CARD_3:def 6;

              hence thesis by A7;

            end;

            A c= B

            proof

              let a be object;

              assume a in A;

              then

              consider b be Element of RP such that

               A9: a = (b "/\" (R . [y, z])) and

               A10: b in ( pi (Q, [x, y]));

              ex f be Function st f in Q & b = (f . [x, y]) by A10, CARD_3:def 6;

              hence thesis by A9;

            end;

            hence thesis by A6, XBOOLE_0:def 10;

          end;

          then

           A11: for y be Element of X holds F(y) = G(y);

          thus { F(y) where y be Element of X : P[y] } = { G(y) where y be Element of X : P[y] } from FRAENKEL:sch 5( A11);

        end;

        

         A12: ( "\/" ( the set of all ( "\/" ({ ((r . [x, y]) "/\" (R . [y, z])) where r be Element of FL : r in Q },RP)) where y be Element of X,RP)) = ( "\/" ({ ( "\/" ( the set of all ((r9 . [x, y]) "/\" (R . [y, z])) where y be Element of X,RP)) where r9 be Element of FL : r9 in Q },RP))

        proof

          deffunc F( Element of X, Element of ( FuzzyLattice [:X, X:])) = (($2 . [x, $1]) "/\" (R . [$1, z]));

          defpred Q[ Element of ( FuzzyLattice [:X, X:])] means $1 in Q;

          defpred P[ Element of X] means not contradiction;

          

           A13: for y be Element of X, r be Element of FL st P[y] & Q[r] holds F(y,r) = F(y,r);

          thus ( "\/" ({ ( "\/" ({ F(y,r) where r be Element of FL : Q[r] },RP)) where y be Element of X : P[y] },RP)) = ( "\/" ({ ( "\/" ({ F(y9,r9) where y9 be Element of X : P[y9] },RP)) where r9 be Element of FL : Q[r9] },RP)) from LFUZZY_0:sch 5( A13);

        end;

        

         A14: { ( "\/" ( the set of all ((r . [x, y]) "/\" (R . [y, z])) where y be Element of X,RP)) where r be Element of FL : r in Q } = { ( "\/" ( the set of all ((( @ r9) . [x, y]) "/\" (R . [y, z])) where y be Element of X,RP)) where r9 be Element of FL : r9 in Q }

        proof

          deffunc G( Element of FL) = ( "\/" ( the set of all ((( @ $1) . [x, y]) "/\" (R . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.])));

          deffunc F( Element of FL) = ( "\/" ( the set of all (($1 . [x, y]) "/\" (R . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.])));

          defpred P[ Element of FL] means $1 in Q;

          for r be Element of FL st r in Q holds ( "\/" ( the set of all ((r . [x, y]) "/\" (R . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.]))) = ( "\/" ( the set of all ((( @ r) . [x, y]) "/\" (R . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.])))

          proof

            let r be Element of FL;

            assume r in Q;

             the set of all ((r . [x, y]) "/\" (R . [y, z])) where y be Element of X = the set of all ((( @ r) . [x, y]) "/\" (R . [y, z])) where y be Element of X

            proof

              deffunc g( Element of X) = ((( @ r) . [x, $1]) "/\" (R . [$1, z]));

              deffunc f( Element of X) = ((r . [x, $1]) "/\" (R . [$1, z]));

              defpred P[ Element of X] means not contradiction;

              

               A15: for y be Element of X holds f(y) = g(y) by LFUZZY_0:def 5;

              thus { f(y) where y be Element of X : P[y] } = { g(y) where y be Element of X : P[y] } from FRAENKEL:sch 5( A15);

            end;

            hence thesis;

          end;

          then

           A16: for r be Element of FL st P[r] holds F(r) = G(r);

          thus { F(r) where r be Element of ( FuzzyLattice [:X, X:]) : P[r] } = { G(r) where r be Element of ( FuzzyLattice [:X, X:]) : P[r] } from FRAENKEL:sch 6( A16);

        end;

        

         A17: { ((( @ r) (#) R) . [x, z]) where r be Element of FL : r in Q } = ( pi ({ (( @ r) (#) R) where r be Element of FL : r in Q }, [x, z]))

        proof

          set A = { ((( @ r) (#) R) . [x, z]) where r be Element of FL : r in Q }, B = ( pi ({ (( @ r) (#) R) where r be Element of FL : r in Q }, [x, z]));

          thus A c= B

          proof

            let a be object;

            assume a in A;

            then

            consider r be Element of FL such that

             A18: a = ((( @ r) (#) R) . [x, z]) and

             A19: r in Q;

            (( @ r) (#) R) in { (( @ r9) (#) R) where r9 be Element of FL : r9 in Q } by A19;

            hence thesis by A18, CARD_3:def 6;

          end;

          thus B c= A

          proof

            let b be object;

            assume b in B;

            then

            consider f be Function such that

             A20: f in { (( @ r9) (#) R) where r9 be Element of FL : r9 in Q } and

             A21: b = (f . [x, z]) by CARD_3:def 6;

            ex r be Element of FL st f = (( @ r) (#) R) & r in Q by A20;

            hence thesis by A21;

          end;

        end;

        

         A22: the set of all ((( @ ( "\/" (Q,FL))) . [x, y]) "/\" (R . [y, z])) where y be Element of X = the set of all (( "\/" (( pi (Q, [x, y])),RP)) "/\" (R . [y, z])) where y be Element of X

        proof

          deffunc G( Element of X) = (( "\/" (( pi (Q, [x, $1])),RP)) "/\" (R . [$1, z]));

          deffunc F( Element of X) = ((( @ ( "\/" (Q,FL))) . [x, $1]) "/\" (R . [$1, z]));

          defpred P[ Element of X] means not contradiction;

          for y be Element of X holds ((( @ ( "\/" (Q,( FuzzyLattice [:X, X:])))) . [x, y]) "/\" (R . [y, z])) = (( "\/" (( pi (Q, [x, y])),( RealPoset [. 0 , 1.]))) "/\" (R . [y, z]))

          proof

            let y be Element of X;

            (( @ ( "\/" (Q,( FuzzyLattice [:X, X:])))) . [x, y]) = (( "\/" (Q,( FuzzyLattice [:X, X:]))) . [x, y]) by LFUZZY_0:def 5

            .= ( "\/" (( pi (Q, [x, y])),( RealPoset [. 0 , 1.]))) by Th32;

            hence thesis;

          end;

          then

           A23: for y be Element of X holds F(y) = G(y);

          thus { F(y) where y be Element of X : P[y] } = { G(y9) where y9 be Element of X : P[y9] } from FRAENKEL:sch 5( A23);

        end;

        

         A24: { ( "\/" ( the set of all ((( @ r) . [x, y]) "/\" (R . [y, z])) where y be Element of X,RP)) where r be Element of FL : r in Q } = { ((( @ r9) (#) R) . [x, z]) where r9 be Element of FL : r9 in Q }

        proof

          deffunc G( Element of FL) = ((( @ $1) (#) R) . [x, z]);

          deffunc F( Element of FL) = ( "\/" ( the set of all ((( @ $1) . [x, y]) "/\" (R . [y, z])) where y be Element of X,( RealPoset [. 0 , 1.])));

          defpred P[ Element of FL] means $1 in Q;

          

           A25: for r be Element of FL st P[r] holds F(r) = G(r) by Lm6;

          thus { F(r) where r be Element of ( FuzzyLattice [:X, X:]) : P[r] } = { G(r) where r be Element of ( FuzzyLattice [:X, X:]) : P[r] } from FRAENKEL:sch 6( A25);

        end;

        

        thus ((( @ ( "\/" (Q,FL))) (#) R) . (x,z)) = ( "\/" ( the set of all ((( @ ( "\/" (Q,FL))) . [x, y]) "/\" (R . [y, z])) where y be Element of X,RP)) by Lm6

        .= (F . (x,z)) by A1, A22, A3, A5, A12, A14, A24, A17, Th32;

      end;

      hence thesis by Th2;

    end;

    theorem :: LFUZZY_1:36

    

     Th36: for R be RMembership_Func of X, X holds (( TrCl R) (#) ( TrCl R)) = ( "\/" ({ ((i iter R) (#) (j iter R)) where i be Element of NAT , j be Element of NAT : i > 0 & j > 0 },( FuzzyLattice [:X, X:])))

    proof

      let R be RMembership_Func of X, X;

      set Q = { (n iter R) where n be Element of NAT : n > 0 }, FL = ( FuzzyLattice [:X, X:]);

      

       A1: Q c= the carrier of FL

      proof

        let q be object;

        assume q in Q;

        then

        consider i be Element of NAT such that

         A2: q = (i iter R) and i > 0 ;

        (( [:X, X:],(i iter R)) @ ) = (i iter R) by LFUZZY_0:def 6;

        hence thesis by A2;

      end;

      

       A3: { ( "\/" ({ (( @ r) (#) ( @ s)) where s be Element of FL : s in Q },FL)) where r be Element of FL : r in Q } = { ( "\/" ({ (( [:X, X:],(( @ r9) (#) ( @ s9))) @ ) where s9 be Element of FL : s9 in Q },FL)) where r9 be Element of FL : r9 in Q }

      proof

        deffunc G( Element of FL) = ( "\/" ({ (( [:X, X:],(( @ $1) (#) ( @ s))) @ ) where s be Element of FL : s in Q },FL));

        deffunc F( Element of FL) = ( "\/" ({ (( @ $1) (#) ( @ s)) where s be Element of FL : s in Q },FL));

        defpred P[ Element of FL] means $1 in Q;

        for r be Element of FL holds ( "\/" ({ (( @ r) (#) ( @ s)) where s be Element of FL : s in Q },FL)) = ( "\/" ({ (( [:X, X:],(( @ r) (#) ( @ s))) @ ) where s be Element of FL : s in Q },FL))

        proof

          let r be Element of FL;

          { (( @ r) (#) ( @ s)) where s be Element of FL : s in Q } = { (( [:X, X:],(( @ r) (#) ( @ s))) @ ) where s be Element of FL : s in Q }

          proof

            deffunc g( Element of FL) = (( [:X, X:],(( @ r) (#) ( @ $1))) @ );

            deffunc f( Element of FL) = (( @ r) (#) ( @ $1));

            defpred P[ Element of FL] means $1 in Q;

            

             A4: for s be Element of FL holds f(s) = g(s) by LFUZZY_0:def 6;

            { f(s) where s be Element of FL : P[s] } = { g(s) where s be Element of FL : P[s] } from FRAENKEL:sch 5( A4);

            hence thesis;

          end;

          hence thesis;

        end;

        then

         A5: for r be Element of FL holds F(r) = G(r);

        { F(r) where r be Element of FL : P[r] } = { G(r) where r be Element of FL : P[r] } from FRAENKEL:sch 5( A5);

        hence thesis;

      end;

      defpred R[ Element of FL] means $1 in Q;

      defpred P[ Element of FL] means $1 in Q;

      deffunc f( Element of FL, Element of FL) = (( [:X, X:],(( @ $1) (#) ( @ $2))) @ );

      

       A6: { (( @ r) (#) ( @ s)) where r be Element of FL, s be Element of FL : r in Q & s in Q } = { ((i iter R) (#) (j iter R)) where i be Element of NAT , j be Element of NAT : i > 0 & j > 0 }

      proof

        set A = { (( @ r) (#) ( @ s)) where r be Element of FL, s be Element of FL : r in Q & s in Q }, B = { ((i iter R) (#) (j iter R)) where i be Element of NAT , j be Element of NAT : i > 0 & j > 0 };

        thus A c= B

        proof

          let a be object;

          assume a in A;

          then

          consider r,s be Element of FL such that

           A7: a = (( @ r) (#) ( @ s)) and

           A8: r in Q & s in Q;

          

           A9: r = ( @ r) & s = ( @ s) by LFUZZY_0:def 5;

          (ex i be Element of NAT st r = (i iter R) & i > 0 ) & ex j be Element of NAT st s = (j iter R) & j > 0 by A8;

          hence thesis by A7, A9;

        end;

        thus B c= A

        proof

          let b be object;

          assume b in B;

          then

          consider i,j be Element of NAT such that

           A10: b = ((i iter R) (#) (j iter R)) and

           A11: i > 0 & j > 0 ;

          (j iter R) = (( [:X, X:],(j iter R)) @ ) by LFUZZY_0:def 6;

          then

          reconsider s = (j iter R) as Element of FL;

          (i iter R) = (( [:X, X:],(i iter R)) @ ) by LFUZZY_0:def 6;

          then

          reconsider r = (i iter R) as Element of FL;

          

           A12: ( @ r) = r & ( @ s) = s by LFUZZY_0:def 5;

          (i iter R) in Q & (j iter R) in Q by A11;

          hence thesis by A10, A12;

        end;

      end;

      

       A13: { (( [:X, X:],(( @ r) (#) ( @ s))) @ ) where r be Element of FL, s be Element of FL : r in Q & s in Q } = { (( @ r) (#) ( @ s)) where r be Element of FL, s be Element of FL : r in Q & s in Q }

      proof

        deffunc G( Element of FL, Element of FL) = (( @ $1) (#) ( @ $2));

        deffunc F( Element of FL, Element of FL) = (( [:X, X:],(( @ $1) (#) ( @ $2))) @ );

        defpred P[ Element of FL, Element of FL] means $1 in Q & $2 in Q;

        

         A14: for r be Element of FL, s be Element of FL holds F(r,s) = G(r,s) by LFUZZY_0:def 6;

        { F(r,s) where r be Element of FL, s be Element of FL : P[r, s] } = { G(r,s) where r be Element of FL, s be Element of FL : P[r, s] } from FRAENKEL:sch 7( A14);

        hence thesis;

      end;

      

       A15: ( "\/" (Q,FL)) = ( @ ( "\/" (Q,FL))) by LFUZZY_0:def 5;

      { (( @ r) (#) ( TrCl R)) where r be Element of FL : r in Q } = { ( "\/" ({ (( @ r9) (#) ( @ s)) where s be Element of FL : s in Q },FL)) where r9 be Element of FL : r9 in Q }

      proof

        set A = { (( @ r) (#) ( TrCl R)) where r be Element of FL : r in Q }, B = { ( "\/" ({ (( @ r9) (#) ( @ s)) where s be Element of FL : s in Q },FL)) where r9 be Element of FL : r9 in Q };

        thus A c= B

        proof

          let a be object;

          assume a in A;

          then

          consider r be Element of FL such that

           A16: a = (( @ r) (#) ( TrCl R)) and

           A17: r in Q;

          a = ( "\/" ({ (( @ r) (#) ( @ s)) where s be Element of FL : s in Q },FL)) by A15, A1, A16, Th34;

          hence thesis by A17;

        end;

        thus B c= A

        proof

          let a be object;

          assume a in B;

          then

          consider r be Element of FL such that

           A18: a = ( "\/" ({ (( @ r) (#) ( @ s)) where s be Element of FL : s in Q },FL)) and

           A19: r in Q;

          a = (( @ r) (#) ( TrCl R)) by A15, A1, A18, Th34;

          hence thesis by A19;

        end;

      end;

      

      hence (( TrCl R) (#) ( TrCl R)) = ( "\/" ({ ( "\/" ({ f(r,s) where s be Element of FL : R[s] },FL)) where r be Element of FL : P[r] },FL)) by A15, A1, A3, Th35

      .= ( "\/" ({ f(r,s) where r be Element of FL, s be Element of FL : P[r] & R[s] },FL)) from LFUZZY_0:sch 1

      .= ( "\/" ({ ((i iter R) (#) (j iter R)) where i be Element of NAT , j be Element of NAT : i > 0 & j > 0 },FL)) by A6, A13;

    end;

    registration

      let X be non empty set;

      let R be RMembership_Func of X, X;

      cluster ( TrCl R) -> transitive;

      coherence

      proof

        set FL = ( FuzzyLattice [:X, X:]), RP = ( RealPoset [. 0 , 1.]), A = { ((i iter R) (#) (j iter R)) where i be Element of NAT , j be Element of NAT : i > 0 & j > 0 };

        for c be Element of [:X, X:] holds ((( TrCl R) (#) ( TrCl R)) . c) <= (( TrCl R) . c)

        proof

          let c be Element of [:X, X:];

          

           A1: A c= the carrier of ( FuzzyLattice [:X, X:])

          proof

            let t be object;

            assume t in A;

            then

            consider i,j be Element of NAT such that

             A2: t = ((i iter R) (#) (j iter R)) and i > 0 and j > 0 ;

            (( [:X, X:],((i iter R) (#) (j iter R))) @ ) = ((i iter R) (#) (j iter R)) by LFUZZY_0:def 6;

            hence thesis by A2;

          end;

          for b be Element of RP st b in ( pi (A,c)) holds b <<= (( TrCl R) . c)

          proof

            let b be Element of RP;

            assume b in ( pi (A,c));

            then

            consider f be Function such that

             A3: f in A and

             A4: b = (f . c) by CARD_3:def 6;

            consider i,j be Element of NAT such that

             A5: f = ((i iter R) (#) (j iter R)) and

             A6: i > 0 and j > 0 by A3;

            

             A7: f = ((i + j) iter R) by A5, Th27;

            reconsider f as RMembership_Func of X, X by A5;

            f c= ( TrCl R) by A6, A7, Th31;

            then (f . c) <= (( TrCl R) . c);

            hence thesis by A4, LFUZZY_0: 3;

          end;

          then (( TrCl R) . c) is_>=_than ( pi (A,c)) by LATTICE3:def 9;

          then

           A8: ( "\/" (( pi (A,c)),RP)) <<= (( TrCl R) . c) by YELLOW_0: 32;

          ((( TrCl R) (#) ( TrCl R)) . c) = (( "\/" (A,FL)) . c) by Th36

          .= ( "\/" (( pi (A,c)),RP)) by A1, Th32;

          hence thesis by A8, LFUZZY_0: 3;

        end;

        then (( TrCl R) (#) ( TrCl R)) c= ( TrCl R);

        hence thesis;

      end;

    end

    theorem :: LFUZZY_1:37

    

     Th37: for R be RMembership_Func of X, X, n be Nat st R is transitive & n > 0 holds (n iter R) c= R

    proof

      let R be RMembership_Func of X, X;

      let n be Nat;

      assume that

       A1: R is transitive and

       A2: n > 0 ;

      reconsider n as non zero Element of NAT by A2, ORDINAL1:def 12;

      defpred P[ Nat] means ($1 iter R) c= R;

      

       A3: (R (#) R) c= R by A1;

      

       A4: for k be non zero Nat st P[k] holds P[(k + 1)]

      proof

        let k be non zero Nat;

        assume P[k];

        then ((k iter R) (#) R) c= (R (#) R) by Th6;

        then ((k + 1) iter R) c= (R (#) R) by Th26;

        hence thesis by A3, Th5;

      end;

      

       A5: P[1] by Th25;

      for k be non zero Nat holds P[k] from NAT_1:sch 10( A5, A4);

      then P[n];

      hence thesis;

    end;

    theorem :: LFUZZY_1:38

    

     Th38: for R be RMembership_Func of X, X st R is transitive holds R = ( TrCl R)

    proof

      let R be RMembership_Func of X, X;

      assume

       A1: R is transitive;

      for c be Element of [:X, X:] holds (( TrCl R) . c) <= (R . c)

      proof

        set Q = { (n iter R) where n be Element of NAT : n > 0 }, RP = ( RealPoset [. 0 , 1.]);

        let c be Element of [:X, X:];

        for b be Element of RP st b in ( pi (Q,c)) holds b <<= (R . c)

        proof

          let b be Element of RP;

          assume b in ( pi (Q,c));

          then

          consider f be Function such that

           A2: f in Q and

           A3: b = (f . c) by CARD_3:def 6;

          consider n be Element of NAT such that

           A4: f = (n iter R) and

           A5: n > 0 by A2;

          (n iter R) c= R by A1, A5, Th37;

          then ((n iter R) . c) <= (R . c);

          hence thesis by A3, A4, LFUZZY_0: 3;

        end;

        then

         A6: (R . c) is_>=_than ( pi (Q,c)) by LATTICE3:def 9;

        Q c= the carrier of ( FuzzyLattice [:X, X:])

        proof

          let t be object;

          assume t in Q;

          then

          consider i be Element of NAT such that

           A7: t = (i iter R) and i > 0 ;

          (( [:X, X:],(i iter R)) @ ) = (i iter R) by LFUZZY_0:def 6;

          hence thesis by A7;

        end;

        then (( TrCl R) . c) = ( "\/" (( pi (Q,c)),RP)) by Th32;

        then (( TrCl R) . c) <<= (R . c) by A6, YELLOW_0: 32;

        hence thesis by LFUZZY_0: 3;

      end;

      then

       A8: ( TrCl R) c= R;

      R c= ( TrCl R) by Th30;

      hence thesis by A8, Th3;

    end;

    theorem :: LFUZZY_1:39

    

     Th39: for R,S be RMembership_Func of X, X, n be Nat st R c= S holds (n iter R) c= (n iter S)

    proof

      let R,S be RMembership_Func of X, X;

      let n be Nat;

      defpred P[ Nat] means ($1 iter R) c= ($1 iter S);

      assume

       A1: R c= S;

      

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

      proof

        let k be Nat;

        assume

         A3: P[k];

        ((k iter R) (#) R) = ((k + 1) iter R) & ((k iter S) (#) S) = ((k + 1) iter S) by Th26;

        hence thesis by A1, A3, Th6;

      end;

      ( 0 iter R) = ( Imf (X,X)) by Th24

      .= ( 0 iter S) by Th24;

      then

       A4: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: LFUZZY_1:40

    for R,S be RMembership_Func of X, X st S is transitive & R c= S holds ( TrCl R) c= S

    proof

      let R,S be RMembership_Func of X, X;

      assume that

       A1: S is transitive and

       A2: R c= S;

      for c be Element of [:X, X:] holds (( TrCl R) . c) <= (( TrCl S) . c)

      proof

        set Q = { (n iter R) where n be Element of NAT : n > 0 }, RP = ( RealPoset [. 0 , 1.]);

        let c be Element of [:X, X:];

        for b be Element of RP st b in ( pi (Q,c)) holds b <<= (( TrCl S) . c)

        proof

          let b be Element of RP;

          assume b in ( pi (Q,c));

          then

          consider f be Function such that

           A3: f in Q and

           A4: b = (f . c) by CARD_3:def 6;

          consider n be Element of NAT such that

           A5: f = (n iter R) and

           A6: n > 0 by A3;

          

           A7: (n iter S) c= ( TrCl S) by A6, Th31;

          (n iter R) c= (n iter S) by A2, Th39;

          then (n iter R) c= ( TrCl S) by A7, Th5;

          then ((n iter R) . c) <= (( TrCl S) . c);

          hence thesis by A4, A5, LFUZZY_0: 3;

        end;

        then (( TrCl S) . c) is_>=_than ( pi (Q,c)) by LATTICE3:def 9;

        then

         A8: ( "\/" (( pi (Q,c)),RP)) <<= (( TrCl S) . c) by YELLOW_0: 32;

        Q c= the carrier of ( FuzzyLattice [:X, X:])

        proof

          let t be object;

          assume t in Q;

          then

          consider i be Element of NAT such that

           A9: t = (i iter R) and i > 0 ;

          (( [:X, X:],(i iter R)) @ ) = (i iter R) by LFUZZY_0:def 6;

          hence thesis by A9;

        end;

        then (( TrCl R) . c) = ( "\/" (( pi (Q,c)),RP)) by Th32;

        hence thesis by A8, LFUZZY_0: 3;

      end;

      then ( TrCl R) c= ( TrCl S);

      hence thesis by A1, Th38;

    end;