lfuzzy_0.miz

    begin

    definition

      let R be RelStr;

      :: LFUZZY_0:def1

      attr R is real means

      : Def1: the carrier of R c= REAL & for x,y be Real st x in the carrier of R & y in the carrier of R holds [x, y] in the InternalRel of R iff x <= y;

    end

    definition

      let R be RelStr;

      :: LFUZZY_0:def2

      attr R is interval means

      : Def2: R is real & ex a,b be Real st a <= b & the carrier of R = [.a, b.];

    end

    registration

      cluster interval -> real non empty for RelStr;

      coherence by XXREAL_1: 1;

    end

    registration

      cluster empty -> real for RelStr;

      coherence

      proof

        let R be RelStr;

        assume

         A1: the carrier of R is empty;

        hence the carrier of R c= REAL ;

        thus thesis by A1;

      end;

    end

    theorem :: LFUZZY_0:1



     Th1: for X be real-membered set holds ex R be strict RelStr st the carrier of R = X & R is real

    proof

      let X be real-membered set;

      per cases ;

        suppose

         A1: X is empty;

        set E = the empty strict RelStr;

        take E;

        thus thesis by A1;

      end;

        suppose X is non empty;

        then

        reconsider Y = X as non empty set;

        defpred X[ set, set] means ex x,y be Real st $1 = x & $2 = y & x <= y;

        consider L be non empty strict RelStr such that

         A2: the carrier of L = Y and

         A3: for a,b be Element of L holds a <= b iff X[a, b] from YELLOW_0:sch 1;

        take L;

        thus the carrier of L = X by A2;

        thus the carrier of L c= REAL by A2, MEMBERED: 3;

        let x,y be Real;

        assume x in the carrier of L & y in the carrier of L;

        then

        reconsider a = x, b = y as Element of L;

        a <= b iff [x, y] in the InternalRel of L by ORDERS_2:def 5;

        then [x, y] in the InternalRel of L iff ex x,y be Real st a = x & b = y & x <= y by A3;

        hence thesis;

      end;

    end;

    registration

      cluster interval strict for RelStr;

      existence

      proof

        set X = [. 0 , 1 qua Real.];

        consider R be strict RelStr such that

         A1: the carrier of R = X & R is real by Th1;

        take R;

        thus thesis by A1;

      end;

    end

    theorem :: LFUZZY_0:2



     Th2: for R1,R2 be real RelStr st the carrier of R1 = the carrier of R2 holds the RelStr of R1 = the RelStr of R2

    proof

      let R1,R2 be real RelStr such that

       A1: the carrier of R1 = the carrier of R2;

      set X = the carrier of R1;

      the InternalRel of R1 = the InternalRel of R2

      proof

        let a,b be object;



         A2: X c= REAL by Def1;

        hereby

          assume

           A3: [a, b] in the InternalRel of R1;

          then

           A4: a in X & b in X by ZFMISC_1: 87;

          then

          reconsider a9 = a, b9 = b as Element of REAL by A2;

          a9 <= b9 by A3, A4, Def1;

          hence [a, b] in the InternalRel of R2 by A1, A4, Def1;

        end;

        assume

         A5: [a, b] in the InternalRel of R2;

        then

         A6: a in X & b in X by A1, ZFMISC_1: 87;

        then

        reconsider a9 = a, b9 = b as Element of REAL by A2;

        a9 <= b9 by A1, A5, A6, Def1;

        hence thesis by A6, Def1;

      end;

      hence thesis by A1;

    end;

    registration

      let R be non empty real RelStr;

      cluster -> real for Element of R;

      coherence

      proof

        let x be Element of R;

        the carrier of R c= REAL by Def1;

        hence thesis;

      end;

    end

    definition

      let X be real-membered set;

      :: LFUZZY_0:def3

      func RealPoset X -> real strict RelStr means

      : Def3: the carrier of it = X;

      existence

      proof

        ex R be strict RelStr st the carrier of R = X & R is real by Th1;

        hence thesis;

      end;

      uniqueness by Th2;

    end

    registration

      let X be non empty real-membered set;

      cluster ( RealPoset X) -> non empty;

      coherence by Def3;

    end

    notation

      let R be RelStr;

      let x,y be Element of R;

      synonym x <<= y for x <= y;

      synonym y >>= x for x <= y;

      antonym x ~<= y for x <= y;

      antonym y ~>= x for x <= y;

    end

    theorem :: LFUZZY_0:3



     Th3: for R be non empty real RelStr holds for x,y be Element of R holds x <= y iff x <<= y

    proof

      let R be non empty real RelStr;

      let x,y be Element of R;

       [x, y] in the InternalRel of R iff x <= y by Def1;

      hence thesis by ORDERS_2:def 5;

    end;

    registration

      cluster real -> reflexive antisymmetric transitive for RelStr;

      coherence

      proof

        let R be RelStr such that

         A1: R is real;

        per cases ;

          suppose R is empty;

          hence thesis;

        end;

          suppose R is non empty;

          then

          reconsider R9 = R as non empty real RelStr by A1;



           A2: R9 is antisymmetric

          proof

            let x,y be Element of R9;

            assume x <<= y & x >>= y;

            then x <= y & x >= y by Th3;

            hence thesis by XXREAL_0: 1;

          end;



           A3: R9 is transitive

          proof

            let x,y,z be Element of R9;

            assume x <<= y & y <<= z;

            then x <= y & y <= z by Th3;

            then x <= z by XXREAL_0: 2;

            hence thesis by Th3;

          end;

          R9 is reflexive by Th3;

          hence thesis by A2, A3;

        end;

      end;

    end

    registration

      cluster -> connected for real non empty RelStr;

      coherence

      proof

        let R be non empty real RelStr;

        let x,y be Element of R;

        x <= y or x >= y;

        hence thesis by Th3;

      end;

    end

    definition

      let R be non empty real RelStr;

      let x,y be Element of R;

      :: original: max

      redefine

      func max (x,y) -> Element of R ;

      coherence by XXREAL_0: 16;

    end

    definition

      let R be non empty real RelStr;

      let x,y be Element of R;

      :: original: min

      redefine

      func min (x,y) -> Element of R ;

      coherence by XXREAL_0: 15;

    end

    registration

      cluster -> with_suprema with_infima for real non empty RelStr;

      coherence ;

    end

    reserve x,y,z for Real,

R for real non empty RelStr,

a,b for Element of R;

    registration

      let R;

      let a,b be Element of R;

      identify max (a,b) with a "\/" b;

      compatibility

      proof



         A1: for d be Element of R st d >>= a & d >>= b holds ( max (a,b)) <<= d

        proof

          let d be Element of R;

          assume d >>= a & d >>= b;

          then d >= a & d >= b by Th3;

          then ( max (a,b)) <= d by XXREAL_0: 28;

          hence thesis by Th3;

        end;

        ( max (a,b)) >= b by XXREAL_0: 25;

        then

         A2: ( max (a,b)) >>= b by Th3;

        ( max (a,b)) >= a by XXREAL_0: 25;

        then ( max (a,b)) >>= a by Th3;

        hence thesis by A2, A1, YELLOW_0: 22;

      end;

      identify min (a,b) with a "/\" b;

      compatibility

      proof



         A3: for d be Element of R st d <<= a & d <<= b holds ( min (a,b)) >>= d

        proof

          let d be Element of R;

          assume d <<= a & d <<= b;

          then d <= a & d <= b by Th3;

          then d <= ( min (a,b)) by XXREAL_0: 20;

          hence thesis by Th3;

        end;

        ( min (a,b)) <= b by XXREAL_0: 17;

        then

         A4: ( min (a,b)) <<= b by Th3;

        ( min (a,b)) <= a by XXREAL_0: 17;

        then ( min (a,b)) <<= a by Th3;

        hence thesis by A4, A3, YELLOW_0: 23;

      end;

    end

    theorem :: LFUZZY_0:4

    (a "\/" b) = ( max (a,b));

    theorem :: LFUZZY_0:5

    (a "/\" b) = ( min (a,b));

    theorem :: LFUZZY_0:6



     Th6: (ex x st x in the carrier of R & for y st y in the carrier of R holds x <= y) iff R is lower-bounded

    proof

      hereby

        given x such that

         A1: x in the carrier of R and

         A2: for y st y in the carrier of R holds x <= y;

        reconsider a = x as Element of R by A1;

        for b st b in the carrier of R holds a <<= b by A2, Th3;

        then a is_<=_than the carrier of R;

        hence R is lower-bounded;

      end;

      given x be Element of R such that

       A3: x is_<=_than the carrier of R;

      take x;

      thus x in the carrier of R;

      let y;

      assume y in the carrier of R;

      then

      reconsider b = y as Element of R;

      x <<= b by A3;

      hence thesis by Th3;

    end;

    theorem :: LFUZZY_0:7



     Th7: (ex x st x in the carrier of R & for y st y in the carrier of R holds x >= y) iff R is upper-bounded

    proof

      hereby

        given x such that

         A1: x in the carrier of R and

         A2: for y st y in the carrier of R holds x >= y;

        reconsider a = x as Element of R by A1;

        for b st b in the carrier of R holds a >>= b by A2, Th3;

        then a is_>=_than the carrier of R;

        hence R is upper-bounded;

      end;

      given x be Element of R such that

       A3: x is_>=_than the carrier of R;

      take x;

      thus x in the carrier of R;

      let y;

      assume y in the carrier of R;

      then

      reconsider b = y as Element of R;

      x >>= b by A3;

      hence thesis by Th3;

    end;

    registration

      cluster interval -> bounded for non empty RelStr;

      coherence

      proof

        let R be non empty RelStr;

        assume

         A1: R is real;

        given x,y be Real such that

         A2: x <= y and

         A3: the carrier of R = [.x, y.];

        ex x st x in the carrier of R & for y st y in the carrier of R holds x <= y

        proof

          take x;

          thus x in the carrier of R by A2, A3, XXREAL_1: 1;

          let z;

          assume z in the carrier of R;

          hence thesis by A3, XXREAL_1: 1;

        end;

        then

         A4: R is lower-bounded by A1, Th6;

        ex x st x in the carrier of R & for y st y in the carrier of R holds x >= y

        proof

          take y;

          thus y in the carrier of R by A2, A3, XXREAL_1: 1;

          let z;

          assume z in the carrier of R;

          hence thesis by A3, XXREAL_1: 1;

        end;

        then R is upper-bounded by A1, Th7;

        hence thesis by A4;

      end;

    end

    theorem :: LFUZZY_0:8



     Th8: for R be interval non empty RelStr, X be set holds ex_sup_of (X,R)

    proof

      let R be interval non empty RelStr;

      let X be set;

      consider a,b be Real such that

       A1: a <= b and

       A2: the carrier of R = [.a, b.] by Def2;

      reconsider a, b as Real;

      reconsider Y = (X /\ [.a, b.]) as Subset of REAL ;

       [.a, b.] is non empty closed_interval by A1, MEASURE5: 14;

      then

       A3: [.a, b.] is bounded_above by INTEGRA1: 3;

      then

       A4: Y is bounded_above by XBOOLE_1: 17, XXREAL_2: 43;



       A5: (X /\ [.a, b.]) c= [.a, b.] by XBOOLE_1: 17;

      ex a be Element of R st Y is_<=_than a & for b be Element of R st Y is_<=_than b holds a <<= b

      proof

        per cases ;

          suppose

           A6: Y is empty;

          reconsider x = a as Element of R by A1, A2, XXREAL_1: 1;

          take x;

          thus Y is_<=_than x by A6;

          let y be Element of R;

          x <= y by A2, XXREAL_1: 1;

          hence thesis by Th3;

        end;

          suppose

           A7: Y is non empty;

          set c = the Element of Y;



           A8: c in Y by A7;

          reconsider c as Real;



           A9: a <= c by A5, A8, XXREAL_1: 1;

          c <= ( upper_bound Y) by A4, A7, SEQ_4:def 1;

          then

           A10: a <= ( upper_bound Y) by A9, XXREAL_0: 2;

          ( upper_bound [.a, b.]) = b by A1, JORDAN5A: 19;

          then ( upper_bound Y) <= b by A3, A7, SEQ_4: 48, XBOOLE_1: 17;

          then

          reconsider x = ( upper_bound Y) as Element of R by A2, A10, XXREAL_1: 1;



           A11: for y be Element of R st Y is_<=_than y holds x <<= y

          proof

            let y be Element of R;

            assume

             A12: Y is_<=_than y;

            for z be Real st z in Y holds z <= y

            proof

              let z be Real;

              assume

               A13: z in Y;

              then

              reconsider z as Element of R by A2, XBOOLE_0:def 4;

              z <<= y by A12, A13;

              hence thesis by Th3;

            end;

            then ( upper_bound Y) <= y by A7, SEQ_4: 144;

            hence thesis by Th3;

          end;

          take x;

          for b be Element of R st b in Y holds b <<= x

          proof

            let b be Element of R;

            assume b in Y;

            then b <= ( upper_bound Y) by A4, SEQ_4:def 1;

            hence thesis by Th3;

          end;

          hence thesis by A11;

        end;

      end;

      then ex_sup_of (Y,R) by YELLOW_0: 15;

      hence thesis by A2, YELLOW_0: 50;

    end;

    registration

      cluster -> complete for interval non empty RelStr;

      coherence

      proof

        let R be interval non empty RelStr;

        for X be Subset of R holds ex_sup_of (X,R) by Th8;

        hence thesis by YELLOW_0: 53;

      end;

    end

    registration

      cluster -> distributive for Chain;

      coherence

      proof

        let C be Chain;

        for x,y,z be Element of C holds (x "/\" (y "\/" z)) = ((x "/\" y) "\/" (x "/\" z))

        proof

          let x,y,z be Element of C;



           A1: x <= x;

          per cases by WAYBEL_0:def 29;

            suppose

             A2: x <= y & x <= z & y <= z;



            then

             A3: (x "/\" (y "\/" z)) = (x "/\" z) by YELLOW_0: 24

            .= x by A2, YELLOW_0: 25;

            ((x "/\" y) "\/" (x "/\" z)) = (x "\/" (x "/\" z)) by A2, YELLOW_0: 25

            .= (x "\/" x) by A2, YELLOW_0: 25

            .= x by A1, YELLOW_0: 24;

            hence thesis by A3;

          end;

            suppose

             A4: x <= y & x <= z & y >= z;



            then

             A5: (x "/\" (y "\/" z)) = (x "/\" y) by YELLOW_0: 24

            .= x by A4, YELLOW_0: 25;

            ((x "/\" y) "\/" (x "/\" z)) = (x "\/" (x "/\" z)) by A4, YELLOW_0: 25

            .= (x "\/" x) by A4, YELLOW_0: 25

            .= x by A1, YELLOW_0: 24;

            hence thesis by A5;

          end;

            suppose

             A6: x <= y & x >= z & y <= z;

            then z <= y by YELLOW_0:def 2;

            then

             A7: z = y by A6, YELLOW_0:def 3;



             A8: (x "/\" (y "\/" z)) = (x "/\" z) by A6, YELLOW_0: 24

            .= z by A6, YELLOW_0: 25;

            ((x "/\" y) "\/" (x "/\" z)) = (x "\/" (x "/\" z)) by A6, YELLOW_0: 25

            .= (x "\/" z) by A6, YELLOW_0: 25

            .= x by A6, YELLOW_0: 24;

            hence thesis by A6, A7, A8, YELLOW_0:def 3;

          end;

            suppose

             A9: x <= y & x >= z & y >= z;



            then

             A10: (x "/\" (y "\/" z)) = (x "/\" y) by YELLOW_0: 24

            .= x by A9, YELLOW_0: 25;

            ((x "/\" y) "\/" (x "/\" z)) = (x "\/" (x "/\" z)) by A9, YELLOW_0: 25

            .= (x "\/" z) by A9, YELLOW_0: 25

            .= x by A9, YELLOW_0: 24;

            hence thesis by A10;

          end;

            suppose

             A11: x >= y & x <= z & y <= z;



            then

             A12: (x "/\" (y "\/" z)) = (x "/\" z) by YELLOW_0: 24

            .= x by A11, YELLOW_0: 25;

            ((x "/\" y) "\/" (x "/\" z)) = (y "\/" (x "/\" z)) by A11, YELLOW_0: 25

            .= (y "\/" x) by A11, YELLOW_0: 25

            .= x by A11, YELLOW_0: 24;

            hence thesis by A12;

          end;

            suppose

             A13: x >= y & x <= z & y >= z;

            then z >= y by YELLOW_0:def 2;

            then

             A14: z = y by A13, YELLOW_0:def 3;



             A15: (x "/\" (y "\/" z)) = (x "/\" y) by A13, YELLOW_0: 24

            .= y by A13, YELLOW_0: 25;

            ((x "/\" y) "\/" (x "/\" z)) = (y "\/" (x "/\" z)) by A13, YELLOW_0: 25

            .= (y "\/" x) by A13, YELLOW_0: 25

            .= x by A13, YELLOW_0: 24;

            hence thesis by A13, A14, A15, YELLOW_0:def 3;

          end;

            suppose

             A16: x >= y & x >= z & y <= z;



            then

             A17: (x "/\" (y "\/" z)) = (x "/\" z) by YELLOW_0: 24

            .= z by A16, YELLOW_0: 25;

            ((x "/\" y) "\/" (x "/\" z)) = (y "\/" (x "/\" z)) by A16, YELLOW_0: 25

            .= (y "\/" z) by A16, YELLOW_0: 25

            .= z by A16, YELLOW_0: 24;

            hence thesis by A17;

          end;

            suppose

             A18: x >= y & x >= z & y >= z;



            then

             A19: (x "/\" (y "\/" z)) = (x "/\" y) by YELLOW_0: 24

            .= y by A18, YELLOW_0: 25;

            ((x "/\" y) "\/" (x "/\" z)) = (y "\/" (x "/\" z)) by A18, YELLOW_0: 25

            .= (y "\/" z) by A18, YELLOW_0: 25

            .= y by A18, YELLOW_0: 24;

            hence thesis by A19;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      cluster -> Heyting for interval non empty RelStr;

      coherence

      proof

        let R be interval non empty RelStr;

        thus R is LATTICE;

        let x be Element of R;

        set f = (x "/\" );

        f is sups-preserving

        proof

          let X be Subset of R;

          assume ex_sup_of (X,R);

           A1:

          now

            let b be Element of R such that

             A2: b is_>=_than (f .: X);

            per cases ;

              suppose

               A3: x is_>=_than X;

              b is_>=_than X

              proof

                let a be Element of R;

                assume

                 A4: a in X;

                then x >>= a by A3;

                then (x "/\" a) = a by YELLOW_0: 25;

                then

                 A5: a = (f . a) by WAYBEL_1:def 18;

                (f . a) in (f .: X) by A4, FUNCT_2: 35;

                hence thesis by A2, A5;

              end;

              then

               A6: b >>= ( sup X) by YELLOW_0: 32;

              x >>= ( sup X) by A3, YELLOW_0: 32;

              then (x "/\" ( sup X)) = ( sup X) by YELLOW_0: 25;

              hence (f . ( sup X)) <<= b by A6, WAYBEL_1:def 18;

            end;

              suppose not x is_>=_than X;

              then

              consider a be Element of R such that

               A7: a in X and

               A8: not x >>= a;



               A9: x <<= a by A8, WAYBEL_0:def 29;

              a <<= ( sup X) by A7, YELLOW_2: 22;

              then x <<= ( sup X) by A9, ORDERS_2: 3;

              then x = (x "/\" ( sup X)) by YELLOW_0: 25;

              then

               A10: x = (f . ( sup X)) by WAYBEL_1:def 18;



               A11: (f . a) in (f .: X) by A7, FUNCT_2: 35;

              x = (x "/\" a) by A9, YELLOW_0: 25

              .= (f . a) by WAYBEL_1:def 18;

              hence (f . ( sup X)) <<= b by A2, A10, A11;

            end;

          end;

          thus ex_sup_of ((f .: X),R) by Th8;

          (f . ( sup X)) is_>=_than (f .: X)

          proof

            let a be Element of R;



             A12: (f . ( sup X)) = (x "/\" ( sup X)) & x <<= x by WAYBEL_1:def 18, YELLOW_0:def 1;

            assume a in (f .: X);

            then

            consider y be object such that

             A13: y in the carrier of R and

             A14: y in X & a = (f . y) by FUNCT_2: 64;

            reconsider y as Element of R by A13;

            y <<= ( sup X) & a = (x "/\" y) by A14, WAYBEL_1:def 18, YELLOW_2: 22;

            hence thesis by A12, YELLOW_3: 2;

          end;

          hence thesis by A1, YELLOW_0: 30;

        end;

        hence thesis by WAYBEL_1: 17;

      end;

    end

    registration

      cluster [. 0 , 1.] -> non empty;

      coherence by MEASURE5: 14;

    end

    registration

      cluster ( RealPoset [. 0 , 1.]) -> interval;

      coherence by Def3;

    end

    begin

    theorem :: LFUZZY_0:9



     Th9: for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is sup-Semilattice holds ( product J) is with_suprema

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that

       A1: for i be Element of I holds (J . i) is sup-Semilattice;

      set IT = ( product J);

      for x,y be Element of IT holds ex z be Element of IT st x <= z & y <= z & for z9 be Element of IT st x <= z9 & y <= z9 holds z <= z9

      proof

        let x,y be Element of IT;

        deffunc U( Element of I) = ((x . $1) "\/" (y . $1));

        consider z be ManySortedSet of I such that

         A2: for i be Element of I holds (z . i) = U(i) from PBOOLE:sch 5;



         A3: for i be Element of I holds (z . i) is Element of (J . i)

        proof

          let i be Element of I;

          (z . i) = ((x . i) "\/" (y . i)) by A2;

          hence thesis;

        end;

        ( dom z) = I by PARTFUN1:def 2;

        then

        reconsider z as Element of ( product J) by A3, WAYBEL_3: 27;

        take z;

        for i be Element of I holds (x . i) <= (z . i) & (y . i) <= (z . i)

        proof

          let i be Element of I;

          (J . i) is antisymmetric with_suprema RelStr & (z . i) = ((x . i) "\/" (y . i)) by A1, A2;

          hence thesis by YELLOW_0: 22;

        end;

        hence x <= z & y <= z by WAYBEL_3: 28;

        let z9 be Element of IT;

        assume that

         A4: x <= z9 and

         A5: y <= z9;

        for i be Element of I holds (z . i) <= (z9 . i)

        proof

          let i be Element of I;



           A6: (z9 . i) >= (y . i) & (z . i) = ((x . i) "\/" (y . i)) by A2, A5, WAYBEL_3: 28;

          (J . i) is antisymmetric with_suprema RelStr & (z9 . i) >= (x . i) by A1, A4, WAYBEL_3: 28;

          hence thesis by A6, YELLOW_0: 22;

        end;

        hence thesis by WAYBEL_3: 28;

      end;

      hence thesis;

    end;

    theorem :: LFUZZY_0:10



     Th10: for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is Semilattice holds ( product J) is with_infima

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that

       A1: for i be Element of I holds (J . i) is Semilattice;

      set IT = ( product J);

      for x,y be Element of IT holds ex z be Element of IT st x >= z & y >= z & for z9 be Element of IT st x >= z9 & y >= z9 holds z >= z9

      proof

        let x,y be Element of IT;

        deffunc U( Element of I) = ((x . $1) "/\" (y . $1));

        consider z be ManySortedSet of I such that

         A2: for i be Element of I holds (z . i) = U(i) from PBOOLE:sch 5;



         A3: for i be Element of I holds (z . i) is Element of (J . i)

        proof

          let i be Element of I;

          (z . i) = ((x . i) "/\" (y . i)) by A2;

          hence thesis;

        end;

        ( dom z) = I by PARTFUN1:def 2;

        then

        reconsider z as Element of ( product J) by A3, WAYBEL_3: 27;

        take z;

        for i be Element of I holds (x . i) >= (z . i) & (y . i) >= (z . i)

        proof

          let i be Element of I;

          (J . i) is antisymmetric with_infima RelStr & (z . i) = ((x . i) "/\" (y . i)) by A1, A2;

          hence thesis by YELLOW_0: 23;

        end;

        hence x >= z & y >= z by WAYBEL_3: 28;

        let z9 be Element of IT;

        assume that

         A4: x >= z9 and

         A5: y >= z9;

        for i be Element of I holds (z . i) >= (z9 . i)

        proof

          let i be Element of I;



           A6: (z9 . i) <= (y . i) & (z . i) = ((x . i) "/\" (y . i)) by A2, A5, WAYBEL_3: 28;

          (J . i) is antisymmetric with_infima RelStr & (x . i) >= (z9 . i) by A1, A4, WAYBEL_3: 28;

          hence thesis by A6, YELLOW_0: 23;

        end;

        hence thesis by WAYBEL_3: 28;

      end;

      hence thesis;

    end;

    theorem :: LFUZZY_0:11



     Th11: for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is Semilattice holds for f,g be Element of ( product J), i be Element of I holds ((f "/\" g) . i) = ((f . i) "/\" (g . i))

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that

       A1: for i be Element of I holds (J . i) is Semilattice;

      let f,g be Element of ( product J);

      let i be Element of I;



       A2: (J . i) is Semilattice by A1;

      for i be Element of I holds (J . i) is antisymmetric by A1;

      then

       A3: ( product J) is antisymmetric with_infima by A1, Th10, WAYBEL_3: 30;

      then g >= (f "/\" g) by YELLOW_0: 23;

      then

       A4: (g . i) >= ((f "/\" g) . i) by WAYBEL_3: 28;



       A5: ((f "/\" g) . i) >= ((f . i) "/\" (g . i))

      proof

        deffunc U( Element of I) = ((f . $1) "/\" (g . $1));

        consider z be ManySortedSet of I such that

         A6: for i be Element of I holds (z . i) = U(i) from PBOOLE:sch 5;



         A7: for i be Element of I holds (z . i) is Element of (J . i)

        proof

          let i be Element of I;

          (z . i) = ((f . i) "/\" (g . i)) by A6;

          hence thesis;

        end;

        ( dom z) = I by PARTFUN1:def 2;

        then

        reconsider z as Element of ( product J) by A7, WAYBEL_3: 27;

        for i be Element of I holds (z . i) <= (f . i) & (z . i) <= (g . i)

        proof

          let i be Element of I;

          (J . i) is antisymmetric with_infima RelStr & (z . i) = ((f . i) "/\" (g . i)) by A1, A6;

          hence thesis by YELLOW_0: 23;

        end;

        then z <= f & z <= g by WAYBEL_3: 28;

        then

         A8: (f "/\" g) >= z by A3, YELLOW_0: 23;

        for i be Element of I holds ((f "/\" g) . i) >= ((f . i) "/\" (g . i))

        proof

          let i be Element of I;

          ((f . i) "/\" (g . i)) = (z . i) by A6;

          hence thesis by A8, WAYBEL_3: 28;

        end;

        hence thesis;

      end;

      f >= (f "/\" g) by A3, YELLOW_0: 23;

      then (f . i) >= ((f "/\" g) . i) by WAYBEL_3: 28;

      then ((f "/\" g) . i) <= ((f . i) "/\" (g . i)) by A2, A4, YELLOW_0: 23;

      hence thesis by A2, A5, YELLOW_0:def 3;

    end;

    theorem :: LFUZZY_0:12



     Th12: for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is sup-Semilattice holds for f,g be Element of ( product J), i be Element of I holds ((f "\/" g) . i) = ((f . i) "\/" (g . i))

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that

       A1: for i be Element of I holds (J . i) is sup-Semilattice;

      let f,g be Element of ( product J);

      let i be Element of I;



       A2: (J . i) is sup-Semilattice by A1;

      for i be Element of I holds (J . i) is antisymmetric by A1;

      then

       A3: ( product J) is antisymmetric with_suprema by A1, Th9, WAYBEL_3: 30;

      then g <= (f "\/" g) by YELLOW_0: 22;

      then

       A4: (g . i) <= ((f "\/" g) . i) by WAYBEL_3: 28;



       A5: ((f "\/" g) . i) <= ((f . i) "\/" (g . i))

      proof

        deffunc U( Element of I) = ((f . $1) "\/" (g . $1));

        consider z be ManySortedSet of I such that

         A6: for i be Element of I holds (z . i) = U(i) from PBOOLE:sch 5;



         A7: for i be Element of I holds (z . i) is Element of (J . i)

        proof

          let i be Element of I;

          (z . i) = ((f . i) "\/" (g . i)) by A6;

          hence thesis;

        end;

        ( dom z) = I by PARTFUN1:def 2;

        then

        reconsider z as Element of ( product J) by A7, WAYBEL_3: 27;

        for i be Element of I holds (z . i) >= (f . i) & (z . i) >= (g . i)

        proof

          let i be Element of I;

          (J . i) is antisymmetric with_suprema RelStr & (z . i) = ((f . i) "\/" (g . i)) by A1, A6;

          hence thesis by YELLOW_0: 22;

        end;

        then z >= f & z >= g by WAYBEL_3: 28;

        then

         A8: (f "\/" g) <= z by A3, YELLOW_0: 22;

        for i be Element of I holds ((f "\/" g) . i) <= ((f . i) "\/" (g . i))

        proof

          let i be Element of I;

          ((f . i) "\/" (g . i)) = (z . i) by A6;

          hence thesis by A8, WAYBEL_3: 28;

        end;

        hence thesis;

      end;

      f <= (f "\/" g) by A3, YELLOW_0: 22;

      then (f . i) <= ((f "\/" g) . i) by WAYBEL_3: 28;

      then ((f "\/" g) . i) >= ((f . i) "\/" (g . i)) by A2, A4, YELLOW_0: 22;

      hence thesis by A2, A5, YELLOW_0:def 3;

    end;

    theorem :: LFUZZY_0:13



     Th13: for I be non empty set holds for J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st for i be Element of I holds (J . i) is Heyting complete LATTICE holds ( product J) is complete Heyting

    proof

      let I be non empty set;

      let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I such that

       A1: for i be Element of I holds (J . i) is Heyting complete LATTICE;



       A2: for i be Element of I holds (J . i) is complete LATTICE by A1;

      set H = ( product J);

      reconsider H as complete LATTICE by A2, WAYBEL_3: 31;

      H = H;

      hence ( product J) is complete & ( product J) is LATTICE;

      let f be Element of ( product J);

      reconsider g = f as Element of H;

      reconsider F = (f "/\" ) as Function of H, H;



       A3: for i be Element of I holds (J . i) is Semilattice by A1;

      F is sups-preserving

      proof

        let X be Subset of H;

        reconsider Y = (F .: X), X9 = X as Subset of ( product J);

        reconsider sX = ( sup X) as Element of ( product J);

        assume ex_sup_of (X,H);

        thus ex_sup_of ((F .: X),H) by YELLOW_0: 17;

        reconsider f1 = ( sup (F .: X)), f2 = (F . ( sup X)) as Element of ( product J);

         A4:

        now

          let x be object;

          assume x in ( dom f1);

          then

          reconsider i = x as Element of I by WAYBEL_3: 27;



           A5: (J . i) is complete Heyting LATTICE by A1;

          then

           A6: ex_sup_of (( pi (X9,i)),(J . i)) by YELLOW_0: 17;



           A7: (((f . i) "/\" ) .: ( pi (X9,i))) c= ( pi (Y,i))

          proof

            let b be object;

            assume b in (((f . i) "/\" ) .: ( pi (X9,i)));

            then

            consider f4 be object such that f4 in ( dom ((f . i) "/\" )) and

             A8: f4 in ( pi (X9,i)) and

             A9: b = (((f . i) "/\" ) . f4) by FUNCT_1:def 6;

            consider f5 be Function such that

             A10: f5 in X9 and

             A11: f4 = (f5 . i) by A8, CARD_3:def 6;

            reconsider f5 as Element of ( product J) by A10;

            (f "/\" f5) = ((f "/\" ) . f5) by WAYBEL_1:def 18;

            then

             A12: (f "/\" f5) in ((f "/\" ) .: X) by A10, FUNCT_2: 35;

            (((f . i) "/\" ) . f4) = ((f . i) "/\" (f5 . i)) by A11, WAYBEL_1:def 18

            .= ((f "/\" f5) . i) by A3, Th11;

            hence thesis by A9, A12, CARD_3:def 6;

          end;

          ( pi (Y,i)) c= (((f . i) "/\" ) .: ( pi (X9,i)))

          proof

            let a be object;

            assume a in ( pi (Y,i));

            then

            consider f3 be Function such that

             A13: f3 in Y and

             A14: a = (f3 . i) by CARD_3:def 6;

            reconsider f3 as Element of ( product J) by A13;

            consider h be object such that

             A15: h in ( dom F) and

             A16: h in X and

             A17: f3 = (F . h) by A13, FUNCT_1:def 6;

            reconsider h as Element of ( product J) by A15;



             A18: (h . i) in ( pi (X9,i)) by A16, CARD_3:def 6;

            (f3 . i) = ((f "/\" h) . i) by A17, WAYBEL_1:def 18

            .= ((f . i) "/\" (h . i)) by A3, Th11

            .= (((f . i) "/\" ) . (h . i)) by WAYBEL_1:def 18;

            hence thesis by A14, A18, FUNCT_2: 35;

          end;

          then

           A19: ( pi (Y,i)) = (((f . i) "/\" ) .: ( pi (X9,i))) by A7;

          ((f . i) "/\" ) is lower_adjoint by A5, WAYBEL_1:def 19;

          then

           A20: ((f . i) "/\" ) preserves_sup_of ( pi (X9,i)) by A5, WAYBEL_0:def 33;

          f2 = (g "/\" ( sup X)) by WAYBEL_1:def 18;



          then (f2 . i) = ((f . i) "/\" (sX . i)) by A3, Th11

          .= ((f . i) "/\" ( sup ( pi (X9,i)))) by A2, WAYBEL_3: 32

          .= (((f . i) "/\" ) . ( sup ( pi (X9,i)))) by WAYBEL_1:def 18

          .= ( sup (((f . i) "/\" ) .: ( pi (X9,i)))) by A20, A6;

          hence (f1 . x) = (f2 . x) by A2, A19, WAYBEL_3: 32;

        end;

        ( dom f1) = I & ( dom f2) = I by WAYBEL_3: 27;

        hence thesis by A4, FUNCT_1: 2;

      end;

      hence thesis by WAYBEL_1: 17;

    end;

    registration

      let A be non empty set;

      let R be complete Heyting LATTICE;

      cluster (R |^ A) -> Heyting;

      coherence

      proof

        for i be Element of A holds ((A --> R) . i) is complete Heyting LATTICE;

        then ( product (A --> R)) is complete Heyting by Th13;

        hence thesis by YELLOW_1:def 5;

      end;

    end

    begin

    definition

      let A be non empty set;

      :: LFUZZY_0:def4

      func FuzzyLattice A -> Heyting complete LATTICE equals (( RealPoset [. 0 , 1.]) |^ A);

      coherence ;

    end

    theorem :: LFUZZY_0:14



     Th14: for A be non empty set holds the carrier of ( FuzzyLattice A) = ( Funcs (A, [. 0 , 1.]))

    proof

      let A be non empty set;



      thus the carrier of ( FuzzyLattice A) = ( Funcs (A,the carrier of ( RealPoset [. 0 , 1.]))) by YELLOW_1: 28

      .= ( Funcs (A, [. 0 , 1.])) by Def3;

    end;



     Lm1: for A be non empty set holds ( FuzzyLattice A) is constituted-Functions

    proof

      let A be non empty set;

      for a be Element of ( FuzzyLattice A) holds a is Function

      proof

        let a be Element of ( FuzzyLattice A);

        a in the carrier of ( FuzzyLattice A);

        then a in ( Funcs (A, [. 0 , 1.])) by Th14;

        then ex f be Function st a = f & ( dom f) = A & ( rng f) c= [. 0 , 1.] by FUNCT_2:def 2;

        hence thesis;

      end;

      hence thesis by MONOID_0:def 1;

    end;

    registration

      let A be non empty set;

      cluster ( FuzzyLattice A) -> constituted-Functions;

      coherence by Lm1;

    end

    theorem :: LFUZZY_0:15



     Th15: for R be complete Heyting LATTICE, X be Subset of R, y be Element of R holds (( "\/" (X,R)) "/\" y) = ( "\/" ({ (x "/\" y) 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;

      set Z = { (y "/\" x) where x be Element of R : x in X }, W = { (x "/\" y) where x be Element of R : x in X };



       A1: W c= Z

      proof

        let w be object;

        assume w in W;

        then ex x be Element of R st w = (x "/\" y) & x in X;

        hence thesis;

      end;

      Z c= W

      proof

        let z be object;

        assume z in Z;

        then ex x be Element of R st z = (y "/\" x) & x in X;

        hence thesis;

      end;

      then (for z be Element of R holds (z "/\" ) is lower_adjoint & ex_sup_of (X,R)) & Z = W by A1, WAYBEL_1:def 19, YELLOW_0: 17;

      hence thesis by WAYBEL_1: 63;

    end;



     Lm2: for X be non empty set holds for a be Element of ( FuzzyLattice X) holds a is Membership_Func of X

    proof

      let X be non empty set;

      let a be Element of ( FuzzyLattice X);

      a in the carrier of ( FuzzyLattice X);

      then a in ( Funcs (X, [. 0 , 1.])) by Th14;

      then

       A1: ex f be Function st a = f & ( dom f) = X & ( rng f) c= [. 0 , 1.] by FUNCT_2:def 2;

      then

      reconsider a as PartFunc of X, [. 0 , 1.] by RELSET_1: 4;

      reconsider a as PartFunc of X, REAL by RELSET_1: 7;

      a is Function of X, REAL by A1, FUNCT_2:def 1;

      hence thesis;

    end;

    definition

      let X be non empty set;

      let a be Element of ( FuzzyLattice X);

      :: LFUZZY_0:def5

      func @ a -> Membership_Func of X equals a;

      coherence by Lm2;

    end



     Lm3: for X be non empty set holds for f be Membership_Func of X holds f is Element of ( FuzzyLattice X)

    proof

      let X be non empty set;

      let f be Membership_Func of X;

      ( dom f) = X & ( rng f) c= [. 0 , 1.] by FUNCT_2:def 1, RELAT_1:def 19;

      then f in ( Funcs (X, [. 0 , 1.])) by FUNCT_2:def 2;

      hence thesis by Th14;

    end;

    definition

      let X be non empty set;

      let f be Membership_Func of X;

      :: LFUZZY_0:def6

      func (X,f) @ -> Element of ( FuzzyLattice X) equals f;

      coherence by Lm3;

    end

    definition

      let X be non empty set;

      let f be Membership_Func of X;

      let x be Element of X;

      :: original: .

      redefine

      func f . x -> Element of ( RealPoset [. 0 , 1.]) ;

      coherence

      proof

         0 <= (f . x) & (f . x) <= 1 by FUZZY_2: 1;

        then (f . x) in [. 0 , 1.] by XXREAL_1: 1;

        hence thesis by Def3;

      end;

    end

    definition

      let X,Y be non empty set;

      let f be RMembership_Func of X, Y;

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

      :: original: .

      redefine

      func f . (x,y) -> Element of ( RealPoset [. 0 , 1.]) ;

      coherence

      proof

        (f . [x, y]) is Element of ( RealPoset [. 0 , 1.]);

        hence thesis;

      end;

    end

    definition

      let X be non empty set;

      let f be Element of ( FuzzyLattice X);

      let x be Element of X;

      :: original: .

      redefine

      func f . x -> Element of ( RealPoset [. 0 , 1.]) ;

      coherence

      proof

         0 <= (( @ f) . x) by FUZZY_2: 1;

        hence thesis;

      end;

    end

    reserve C for non empty set,

c for Element of C,

f,g for Membership_Func of C,

s,t for Element of ( FuzzyLattice C);

    theorem :: LFUZZY_0:16



     Th16: (for c holds (f . c) <= (g . c)) iff ((C,f) @ ) <<= ((C,g) @ )

    proof



       A1: (( RealPoset [. 0 , 1.]) |^ C) = ( product (C --> ( RealPoset [. 0 , 1.]))) by YELLOW_1:def 5;



       A2: (for c holds (f . c) <= (g . c)) implies ((C,f) @ ) <<= ((C,g) @ )

      proof

        set f9 = ((C,f) @ ), g9 = ((C,g) @ );

        reconsider f9, g9 as Element of ( product (C --> ( RealPoset [. 0 , 1.]))) by YELLOW_1:def 5;

        assume

         A3: for c holds (f . c) <= (g . c);

        for c holds (f9 . c) <<= (g9 . c) by A3, Th3;

        hence thesis by A1, WAYBEL_3: 28;

      end;

      ((C,f) @ ) <<= ((C,g) @ ) implies for c holds (f . c) <= (g . c)

      proof

        reconsider ff = ((C,f) @ ), gg = ((C,g) @ ) as Element of ( product (C --> ( RealPoset [. 0 , 1.]))) by YELLOW_1:def 5;

        assume

         A4: ((C,f) @ ) <<= ((C,g) @ );

        let c;

        ((C --> ( RealPoset [. 0 , 1.])) . c) = ( RealPoset [. 0 , 1.]) & (ff . c) <<= (gg . c) by A1, A4, WAYBEL_3: 28;

        hence thesis by Th3;

      end;

      hence thesis by A2;

    end;

    theorem :: LFUZZY_0:17

    s <<= t iff for c holds (( @ s) . c) <= (( @ t) . c)

    proof

      ((C,( @ s)) @ ) = s & ((C,( @ t)) @ ) = t;

      hence thesis by Th16;

    end;

    theorem :: LFUZZY_0:18



     Th18: ( max (f,g)) = (((C,f) @ ) "\/" ((C,g) @ ))

    proof

      set fg = (((C,f) @ ) "\/" ((C,g) @ )), R = ( RealPoset [. 0 , 1.]), J = (C --> R);



       A1: (( RealPoset [. 0 , 1.]) |^ C) = ( product (C --> ( RealPoset [. 0 , 1.]))) by YELLOW_1:def 5;

      now

        let c;

        (for c be Element of C holds (J . c) is sup-Semilattice) & (J . c) = ( RealPoset [. 0 , 1.]);



        hence (( @ fg) . c) = ((((C,f) @ ) . c) "\/" (((C,g) @ ) . c)) by A1, Th12

        .= ( max ((f . c),(g . c)));

      end;

      hence thesis by FUZZY_1:def 4;

    end;

    theorem :: LFUZZY_0:19

    (s "\/" t) = ( max (( @ s),( @ t)))

    proof

      ((C,( @ s)) @ ) = s & ((C,( @ t)) @ ) = t;

      hence thesis by Th18;

    end;

    theorem :: LFUZZY_0:20



     Th20: ( min (f,g)) = (((C,f) @ ) "/\" ((C,g) @ ))

    proof

      set fg = (((C,f) @ ) "/\" ((C,g) @ )), R = ( RealPoset [. 0 , 1.]), J = (C --> R);



       A1: (( RealPoset [. 0 , 1.]) |^ C) = ( product (C --> ( RealPoset [. 0 , 1.]))) by YELLOW_1:def 5;

      now

        let c;

        (for c be Element of C holds (J . c) is Semilattice) & (J . c) = ( RealPoset [. 0 , 1.]);



        hence (( @ fg) . c) = ((((C,f) @ ) . c) "/\" (((C,g) @ ) . c)) by A1, Th11

        .= ( min ((f . c),(g . c)));

      end;

      hence thesis by FUZZY_1:def 3;

    end;

    theorem :: LFUZZY_0:21

    (s "/\" t) = ( min (( @ s),( @ t)))

    proof

      ((C,( @ s)) @ ) = s & ((C,( @ t)) @ ) = t;

      hence thesis by Th20;

    end;

    begin

    scheme :: LFUZZY_0:sch1

    SupDistributivity { L() -> complete LATTICE , X,Y() -> non empty set , F( set, set) -> Element of L() , P,Q[ set] } :

( "\/" ({ ( "\/" ({ F(x,y) where y be Element of Y() : Q[y] },L())) where x be Element of X() : P[x] },L())) = ( "\/" ({ F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] },L()));

      defpred R[ set] means ex x be Element of X() st P[x] & for a be set holds a in $1 iff ex y be Element of Y() st a = F(x,y) & Q[y];



       A1: ( "\/" ({ ( "\/" (A,L())) where A be Subset of L() : R[A] },L())) = ( "\/" (( union { A where A be Subset of L() : R[A] }),L())) from YELLOW_3:sch 5;



       A2: { F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] } c= ( union { A where A be Subset of L() : R[A] })

      proof

        let a be object;

        assume a in { F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] };

        then

        consider x be Element of X(), y be Element of Y() such that

         A3: a = F(x,y) and

         A4: P[x] and

         A5: Q[y];

        set A1 = { F(x,y9) where y9 be Element of Y() : Q[y9] };

        A1 c= the carrier of L()

        proof

          let b be object;

          assume b in A1;

          then ex y9 be Element of Y() st b = F(x,y9) & Q[y9];

          hence thesis;

        end;

        then

        reconsider A1 as Subset of L();

         R[A1]

        proof

          take x;

          thus P[x] by A4;

          let a be set;

          thus thesis;

        end;

        then

         A6: A1 in { A where A be Subset of L() : R[A] };

        a in A1 by A3, A5;

        hence thesis by A6, TARSKI:def 4;

      end;



       A7: { ( "\/" ({ F(x,y) where y be Element of Y() : Q[y] },L())) where x be Element of X() : P[x] } c= { ( "\/" (A,L())) where A be Subset of L() : R[A] }

      proof

        let a be object;

        assume a in { ( "\/" ({ F(x,y) where y be Element of Y() : Q[y] },L())) where x be Element of X() : P[x] };

        then

        consider x be Element of X() such that

         A8: a = ( "\/" ({ F(x,y) where y be Element of Y() : Q[y] },L())) and

         A9: P[x];

        ex A1 be Subset of L() st a = ( "\/" (A1,L())) & R[A1]

        proof

          set A2 = { F(x,y) where y be Element of Y() : Q[y] };

          A2 c= the carrier of L()

          proof

            let b be object;

            assume b in A2;

            then ex y be Element of Y() st b = F(x,y) & Q[y];

            hence thesis;

          end;

          then

          reconsider A1 = A2 as Subset of L();

           R[A1]

          proof

            take x;

            thus P[x] by A9;

            thus thesis;

          end;

          hence thesis by A8;

        end;

        hence thesis;

      end;



       A10: { ( "\/" (A,L())) where A be Subset of L() : R[A] } c= { ( "\/" ({ F(x,y) where y be Element of Y() : Q[y] },L())) where x be Element of X() : P[x] }

      proof

        let a be object;

        assume a in { ( "\/" (A,L())) where A be Subset of L() : R[A] };

        then

        consider A1 be Subset of L() such that

         A11: a = ( "\/" (A1,L())) and

         A12: R[A1];

        consider x be Element of X() such that

         A13: P[x] and

         A14: for a be set holds a in A1 iff ex y be Element of Y() st a = F(x,y) & Q[y] by A12;

        now

          let a be object;

          a in { F(x,y) where y be Element of Y() : Q[y] } iff ex y be Element of Y() st a = F(x,y) & Q[y];

          hence a in A1 iff a in { F(x,y) where y be Element of Y() : Q[y] } by A14;

        end;

        then A1 = { F(x,y) where y be Element of Y() : Q[y] } by TARSKI: 2;

        hence thesis by A11, A13;

      end;

      ( union { A where A be Subset of L() : R[A] }) c= { F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] }

      proof

        let a be object;

        assume a in ( union { A where A be Subset of L() : R[A] });

        then

        consider A1 be set such that

         A15: a in A1 and

         A16: A1 in { A where A be Subset of L() : R[A] } by TARSKI:def 4;

        consider A2 be Subset of L() such that

         A17: A1 = A2 and

         A18: R[A2] by A16;

        consider x be Element of X() such that

         A19: P[x] and

         A20: for a be set holds a in A2 iff ex y be Element of Y() st a = F(x,y) & Q[y] by A18;

        ex y be Element of Y() st a = F(x,y) & Q[y] by A15, A17, A20;

        hence thesis by A19;

      end;

      then ( union { A where A be Subset of L() : R[A] }) = { F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] } by A2;

      hence thesis by A1, A10, A7, XBOOLE_0:def 10;

    end;

    scheme :: LFUZZY_0:sch2

    SupDistributivity9 { L() -> complete LATTICE , X,Y() -> non empty set , F( set, set) -> Element of L() , P,Q[ set] } :

( "\/" ({ ( "\/" ({ F(x,y) where x be Element of X() : P[x] },L())) where y be Element of Y() : Q[y] },L())) = ( "\/" ({ F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] },L()));

      defpred R[ set] means ex y be Element of Y() st Q[y] & for a be set holds a in $1 iff ex x be Element of X() st a = F(x,y) & P[x];



       A1: ( "\/" ({ ( "\/" (A,L())) where A be Subset of L() : R[A] },L())) = ( "\/" (( union { A where A be Subset of L() : R[A] }),L())) from YELLOW_3:sch 5;



       A2: { F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] } c= ( union { A where A be Subset of L() : R[A] })

      proof

        let a be object;

        assume a in { F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] };

        then

        consider x be Element of X(), y be Element of Y() such that

         A3: a = F(x,y) & P[x] and

         A4: Q[y];

        set A1 = { F(x9,y) where x9 be Element of X() : P[x9] };

        A1 c= the carrier of L()

        proof

          let b be object;

          assume b in A1;

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

          hence thesis;

        end;

        then

        reconsider A1 as Subset of L();

         R[A1]

        proof

          take y;

          thus Q[y] by A4;

          let a be set;

          thus thesis;

        end;

        then

         A5: A1 in { A where A be Subset of L() : R[A] };

        a in A1 by A3;

        hence thesis by A5, TARSKI:def 4;

      end;



       A6: { ( "\/" ({ F(x,y) where x be Element of X() : P[x] },L())) where y be Element of Y() : Q[y] } c= { ( "\/" (A,L())) where A be Subset of L() : R[A] }

      proof

        let a be object;

        assume a in { ( "\/" ({ F(x,y) where x be Element of X() : P[x] },L())) where y be Element of Y() : Q[y] };

        then

        consider y be Element of Y() such that

         A7: a = ( "\/" ({ F(x,y) where x be Element of X() : P[x] },L())) and

         A8: Q[y];

        ex A1 be Subset of L() st a = ( "\/" (A1,L())) & R[A1]

        proof

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

          A2 c= the carrier of L()

          proof

            let b be object;

            assume b in A2;

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

            hence thesis;

          end;

          then

          reconsider A1 = A2 as Subset of L();

           R[A1]

          proof

            take y;

            thus Q[y] by A8;

            thus thesis;

          end;

          hence thesis by A7;

        end;

        hence thesis;

      end;



       A9: { ( "\/" (A,L())) where A be Subset of L() : R[A] } c= { ( "\/" ({ F(x,y) where x be Element of X() : P[x] },L())) where y be Element of Y() : Q[y] }

      proof

        let a be object;

        assume a in { ( "\/" (A,L())) where A be Subset of L() : R[A] };

        then

        consider A1 be Subset of L() such that

         A10: a = ( "\/" (A1,L())) and

         A11: R[A1];

        consider y be Element of Y() such that

         A12: Q[y] and

         A13: for a be set holds a in A1 iff ex x be Element of X() st a = F(x,y) & P[x] by A11;

        now

          let a be object;

          a in { F(x,y) where x be Element of X() : P[x] } iff ex x be Element of X() st a = F(x,y) & P[x];

          hence a in A1 iff a in { F(x,y) where x be Element of X() : P[x] } by A13;

        end;

        then A1 = { F(x,y) where x be Element of X() : P[x] } by TARSKI: 2;

        hence thesis by A10, A12;

      end;

      ( union { A where A be Subset of L() : R[A] }) c= { F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] }

      proof

        let a be object;

        assume a in ( union { A where A be Subset of L() : R[A] });

        then

        consider A1 be set such that

         A14: a in A1 and

         A15: A1 in { A where A be Subset of L() : R[A] } by TARSKI:def 4;

        consider A2 be Subset of L() such that

         A16: A1 = A2 and

         A17: R[A2] by A15;

        consider y be Element of Y() such that

         A18: Q[y] and

         A19: for a be set holds a in A2 iff ex x be Element of X() st a = F(x,y) & P[x] by A17;

        ex x be Element of X() st a = F(x,y) & P[x] by A14, A16, A19;

        hence thesis by A18;

      end;

      then ( union { A where A be Subset of L() : R[A] }) = { F(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] } by A2;

      hence thesis by A1, A9, A6, XBOOLE_0:def 10;

    end;

    scheme :: LFUZZY_0:sch3

    FraenkelF9R9 { A() -> non empty set , B() -> non empty set , F1,F2( set, set) -> set , P[ set, set] } :

{ F1(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] } = { F2(u2,v2) where u2 be Element of A(), v2 be Element of B() : P[u2, v2] }

      provided

       A1: for u be Element of A(), v be Element of B() st P[u, v] holds F1(u,v) = F2(u,v);

      set A = { F1(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] }, C = { F2(u3,v3) where u3 be Element of A(), v3 be Element of B() : P[u3, v3] };

      for a be object holds a in A iff a in C

      proof

        let a be object;

        hereby

          assume a in A;

          then

          consider u be Element of A(), v be Element of B() such that

           A2: a = F1(u,v) and

           A3: P[u, v];

          a = F2(u,v) by A1, A2, A3;

          hence a in C by A3;

        end;

        assume a in C;

        then

        consider u be Element of A(), v be Element of B() such that

         A4: a = F2(u,v) and

         A5: P[u, v];

        a = F1(u,v) by A1, A4, A5;

        hence thesis by A5;

      end;

      hence thesis by TARSKI: 2;

    end;

    scheme :: LFUZZY_0:sch4

    FraenkelF699R { A() -> non empty set , B() -> non empty set , F1,F2( set, set) -> set , P[ set, set], Q[ set, set] } :

{ F1(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] } = { F2(u2,v2) where u2 be Element of A(), v2 be Element of B() : Q[u2, v2] }

      provided

       A1: for u be Element of A(), v be Element of B() holds P[u, v] iff Q[u, v]

       and

       A2: for u be Element of A(), v be Element of B() st P[u, v] holds F1(u,v) = F2(u,v);

      set A = { F1(u1,v1) where u1 be Element of A(), v1 be Element of B() : P[u1, v1] }, B = { F2(u2,v2) where u2 be Element of A(), v2 be Element of B() : Q[u2, v2] }, C = { F2(u3,v3) where u3 be Element of A(), v3 be Element of B() : P[u3, v3] };



       A3: C = B from FRAENKEL:sch 4( A1);

      A = C from FraenkelF9R9( A2);

      hence thesis by A3;

    end;

    scheme :: LFUZZY_0:sch5

    SupCommutativity { L() -> complete LATTICE , X,Y() -> non empty set , F1,F2( set, set) -> Element of L() , P,Q[ set] } :

( "\/" ({ ( "\/" ({ F1(x,y) where y be Element of Y() : Q[y] },L())) where x be Element of X() : P[x] },L())) = ( "\/" ({ ( "\/" ({ F2(x9,y9) where x9 be Element of X() : P[x9] },L())) where y9 be Element of Y() : Q[y9] },L()))

      provided

       A1: for x be Element of X(), y be Element of Y() st P[x] & Q[y] holds F1(x,y) = F2(x,y);

      defpred X[ set, set] means P[$1] & Q[$2];



       A2: for x be Element of X(), y be Element of Y() holds X[x, y] iff X[x, y];



       A3: for x be Element of X(), y be Element of Y() st X[x, y] holds F1(x,y) = F2(x,y) by A1;



       A4: { F1(x9,y9) where x9 be Element of X(), y9 be Element of Y() : X[x9, y9] } = { F2(x,y) where x be Element of X(), y be Element of Y() : X[x, y] } from FraenkelF699R( A2, A3);



       A5: ( "\/" ({ ( "\/" ({ F1(x,y) where y be Element of Y() : Q[y] },L())) where x be Element of X() : P[x] },L())) = ( "\/" ({ F1(x,y) where x be Element of X(), y be Element of Y() : P[x] & Q[y] },L())) from SupDistributivity;

      ( "\/" ({ ( "\/" ({ F2(x9,y9) where x9 be Element of X() : P[x9] },L())) where y9 be Element of Y() : Q[y9] },L())) = ( "\/" ({ F2(x9,y9) where x9 be Element of X(), y9 be Element of Y() : P[x9] & Q[y9] },L())) from SupDistributivity9

      .= ( "\/" ({ F1(x9,y9) where x9 be Element of X(), y9 be Element of Y() : P[x9] & Q[y9] },L())) by A4;

      hence thesis by A5;

    end;



     Lm4: 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;

      ex d be set st d in ( rng ( min (R,S,x,z)))

      proof

        set y = the Element of Y;

        take (( min (R,S,x,z)) . y);

        thus thesis by A1, PARTFUN1: 4;

      end;

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

    end;

    theorem :: LFUZZY_0:22



     Th22: 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 Lm4;



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

        proof

          let r be Real;

          assume

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

          then

          reconsider r as Element of ( RealPoset [. 0 , 1.]) by A4, Def3;

          r <<= b by A3, A5, A7;

          hence thesis by Th3;

        end;

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

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

        hence thesis by A1, Th3;

      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

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

        reconsider b as Real;

        ( dom ( min (R,S,x,z))) = Y & b = (( min (R,S,x,z)) . y) by A8, 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, Th3;

      end;

      then ((R (#) S) . [x, z]) is_>=_than L;

      hence thesis by A2, YELLOW_0: 32;

    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 for a be Element of ( RealPoset [. 0 , 1.]) holds (((R (#) S) . (x,z)) "/\" a) = ( "\/" ( the set of all (((R . (x,y)) "/\" (S . (y,z))) "/\" a) 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;

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



       A1: the set of all ((R . (x,y)) "/\" (S . (y,z))) where y be Element of Y c= the carrier of ( RealPoset [. 0 , 1.])

      proof

        let d be object;

        assume d in the set of all ((R . (x,y)) "/\" (S . (y,z))) where y be Element of Y;

        then ex t be Element of Y st d = ((R . (x,t)) "/\" (S . (t,z)));

        hence thesis;

      end;

      set A = { (b "/\" a) where b be Element of ( RealPoset [. 0 , 1.]) : b in the set of all ((R . (x,y)) "/\" (S . (y,z))) where y be Element of Y };

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



       A2: for c be object holds c in A iff c in B

      proof

        let c be object;

        hereby

          assume c in A;

          then

          consider b be Element of ( RealPoset [. 0 , 1.]) such that

           A3: c = (b "/\" a) and

           A4: b in the set of all ((R . (x,y)) "/\" (S . (y,z))) where y be Element of Y;

          ex y be Element of Y st b = ((R . (x,y)) "/\" (S . (y,z))) by A4;

          hence c in B by A3;

        end;

        assume c in B;

        then

        consider y be Element of Y such that

         A5: c = (((R . (x,y)) "/\" (S . (y,z))) "/\" a);

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

        hence thesis by A5;

      end;

      (((R (#) S) . (x,z)) "/\" a) = (( "\/" ( the set of all ((R . (x,y)) "/\" (S . (y,z))) where y be Element of Y,( RealPoset [. 0 , 1.]))) "/\" a) by Th22

      .= ( "\/" ({ (b "/\" a) where b be Element of ( RealPoset [. 0 , 1.]) : b in the set of all ((R . (x,y)) "/\" (S . (y,z))) where y be Element of Y },( RealPoset [. 0 , 1.]))) by A1, Th15;

      hence thesis by A2, TARSKI: 2;

    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 for a be Element of ( RealPoset [. 0 , 1.]) holds (a "/\" ((R (#) S) . (x,z))) = ( "\/" ( the set of all ((a "/\" (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;

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

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

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

      for b be object holds b in A iff b in B

      proof

        let b be object;

        hereby

          assume b in A;

          then

          consider y be Element of Y such that

           A1: b = ((a "/\" (R . (x,y))) "/\" (S . (y,z)));

          b = (((R . (x,y)) "/\" (S . (y,z))) "/\" a) by A1, LATTICE3: 16;

          hence b in B;

        end;

        assume b in B;

        then

        consider y be Element of Y such that

         A2: b = (((R . (x,y)) "/\" (S . (y,z))) "/\" a);

        b = ((a "/\" (R . (x,y))) "/\" (S . (y,z))) by A2, LATTICE3: 16;

        hence thesis;

      end;

      then A = B by TARSKI: 2;

      hence thesis by Lm5;

    end;

    theorem :: LFUZZY_0:23

    for X,Y,Z,W be non empty set holds for R be RMembership_Func of X, Y holds for S be RMembership_Func of Y, Z holds for T be RMembership_Func of Z, W holds ((R (#) S) (#) T) = (R (#) (S (#) T))

    proof

      let X,Y,Z,W be non empty set;

      let R be RMembership_Func of X, Y;

      let S be RMembership_Func of Y, Z;

      let T be RMembership_Func of Z, W;



       A1: for x,w be object st x in X & w in W holds (((R (#) S) (#) T) . (x,w)) = ((R (#) (S (#) T)) . (x,w))

      proof

        let x,w be object;

        assume that

         A2: x in X and

         A3: w in W;

        reconsider w as Element of W by A3;

        reconsider x as Element of X by A2;

        set A = the set of all ( "\/" ( the set of all (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y be Element of Y,( RealPoset [. 0 , 1.]))) where z be Element of Z;

        set B = the set of all (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z be Element of Z;

        set C = the set of all ( "\/" ( the set of all (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z be Element of Z,( RealPoset [. 0 , 1.]))) where y be Element of Y;

        set D = the set of all ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y be Element of Y;

        defpred X[ set] means not contradiction;

        deffunc U( Element of Y, Element of Z) = (((R . (x,$1)) "/\" (S . ($1,$2))) "/\" (T . ($2,w)));



         A4: for a be object holds a in A iff a in B

        proof

          let a be object;

          hereby

            assume a in A;

            then

            consider z be Element of Z such that

             A5: a = ( "\/" ( the set of all (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y be Element of Y,( RealPoset [. 0 , 1.])));

            a = (((R (#) S) . (x,z)) "/\" (T . (z,w))) by A5, Lm5;

            hence a in B;

          end;

          assume a in B;

          then

          consider z be Element of Z such that

           A6: a = (((R (#) S) . (x,z)) "/\" (T . (z,w)));

          a = ( "\/" ( the set of all (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y be Element of Y,( RealPoset [. 0 , 1.]))) by A6, Lm5;

          hence thesis;

        end;



         A7: for y be Element of Y, z be Element of Z st X[y] & X[z] holds U(y,z) = U(y,z);



         A8: ( "\/" ({ ( "\/" ({ U(y,z) where z be Element of Z : X[z] },( RealPoset [. 0 , 1.]))) where y be Element of Y : X[y] },( RealPoset [. 0 , 1.]))) = ( "\/" ({ ( "\/" ({ U(y1,z1) where y1 be Element of Y : X[y1] },( RealPoset [. 0 , 1.]))) where z1 be Element of Z : X[z1] },( RealPoset [. 0 , 1.]))) from SupCommutativity( A7);

        for c be object holds c in C iff c in D

        proof

          let c be object;

          hereby

            assume c in C;

            then

            consider y be Element of Y such that

             A9: c = ( "\/" ( the set of all (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z be Element of Z,( RealPoset [. 0 , 1.])));

            c = ((R . (x,y)) "/\" ((S (#) T) . (y,w))) by A9, Lm6;

            hence c in D;

          end;

          assume c in D;

          then

          consider y be Element of Y such that

           A10: c = ((R . (x,y)) "/\" ((S (#) T) . (y,w)));

          c = ( "\/" ( the set of all (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z be Element of Z,( RealPoset [. 0 , 1.]))) by A10, Lm6;

          hence thesis;

        end;

        then

         A11: C = D by TARSKI: 2;

        (((R (#) S) (#) T) . (x,w)) = ( "\/" ( the set of all (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z be Element of Z,( RealPoset [. 0 , 1.]))) & ((R (#) (S (#) T)) . (x,w)) = ( "\/" ( the set of all ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y be Element of Y,( RealPoset [. 0 , 1.]))) by Th22;

        hence thesis by A4, A11, A8, TARSKI: 2;

      end;

      thus thesis by A1;

    end;