:: Lattice of Fuzzy Sets
::  by Takashi Mitsuishi and Grzegorz Bancerek
::
:: Received August 12, 2003
:: Copyright (c) 2003-2016 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, ORDERS_2, XREAL_0, STRUCT_0, TARSKI, XXREAL_0, MEASURE5,
      XXREAL_1, XBOOLE_0, SUBSET_1, CARD_1, RELAT_2, LATTICE3, EQREL_1,
      LATTICES, XXREAL_2, YELLOW_0, REAL_1, SEQ_4, REWRITE1, TREES_2, LATTICE2,
      WAYBEL_0, RELAT_1, FUNCT_1, ORDINAL2, YELLOW_1, WAYBEL_3, PBOOLE, CARD_3,
      WAYBEL_1, NEWTON, FUNCOP_1, FUNCT_2, MONOID_0, FUZZY_1, PARTFUN1,
      QC_LANG1, FUZZY_2, VALUED_1, ZFMISC_1, LFUZZY_0, MEMBERED;
 notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1,
      DOMAIN_1, ORDINAL1, PARTFUN1, SUBSET_1, NUMBERS, XXREAL_2, XREAL_0,
      MEMBERED, SEQ_4, RCOMP_1, RELSET_1, STRUCT_0, ORDERS_2, PBOOLE, MONOID_0,
      LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1, WAYBEL_3, FUZZY_1,
      FUZZY_2, FUZZY_4, MEASURE5, FUNCOP_1, XXREAL_0;
 constructors DOMAIN_1, SQUARE_1, LATTICE3, MONOID_0, ORDERS_3, WAYBEL_1,
      WAYBEL_3, INTEGRA1, FUZZY_4, SEQ_4, RELSET_1, FUZZY_1, BINOP_2;
 registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0,
      LATTICE3, YELLOW_0, MONOID_0, YELLOW_1, WAYBEL_1, WAYBEL_2, WAYBEL_3,
      WAYBEL10, WAYBEL17, ORDERS_4, ORDERS_2, FUNCOP_1;
 requirements BOOLE, SUBSET, NUMERALS, REAL;
 definitions TARSKI, RELAT_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1;
 equalities XBOOLE_0, BINOP_1;
 expansions TARSKI, XBOOLE_0, LATTICE3, YELLOW_0, WAYBEL_0, WAYBEL_1, BINOP_1;
 theorems ZFMISC_1, ORDERS_2, WAYBEL_1, FUNCT_1, XBOOLE_1, LATTICE3, YELLOW_0,
      INTEGRA1, XBOOLE_0, TARSKI, SEQ_4, JORDAN5A, FUNCT_2, YELLOW_2, WAYBEL_3,
      YELLOW_3, CARD_3, YELLOW_1, FUNCOP_1, FUZZY_2, FUZZY_4, FUZZY_1,
      PARTFUN1, MONOID_0, WAYBEL_0, XXREAL_0, XXREAL_1, XXREAL_2, RELSET_1,
      RELAT_1, MEASURE5, MEMBERED;
 schemes YELLOW_0, PBOOLE, YELLOW_3, FRAENKEL;

begin :: Posets of Real Numbers

definition
  let R be RelStr;
  attr R is real means
  : Def1:
  the carrier of R c= REAL & for x,y being 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;
  attr R is interval means
  : Def2:
  R is real & ex a,b being 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 being RelStr;
    assume
A1: the carrier of R is empty;
    hence the carrier of R c= REAL;
    thus thesis by A1;
  end;
end;

theorem Th1:
  for X being real-membered set ex R being 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 being Real st $1=x & $2=y & x<=y;
    consider L being non empty strict RelStr such that
A2: the carrier of L = Y and
A3: for a,b being 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 being 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 being strict RelStr such that
A1: the carrier of R = X & R is real by Th1;
    take R;
    thus thesis by A1;
  end;
end;

theorem Th2:
  for R1,R2 being 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;
  func RealPoset X -> real strict RelStr means
  : Def3:
  the carrier of it = X;
  existence
  proof
    ex R being 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 Th3:
  for R being non empty real RelStr for x,y being 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;
  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;
  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 a"\/"b with max(a,b);
  compatibility
  proof
A1: for d being 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 a"/\"b with min(a,b);
  compatibility
  proof
A3: for d being Element of R st d <<= a & d <<= b holds min(a,b) >>= d
    proof
      let d being 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
  a"\/"b = max(a,b);

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

theorem 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 being 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 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 being 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 being non empty RelStr;
    assume
A1: R is real;
    given x,y being 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 Th8:
  for R being interval non empty RelStr, X being set holds ex_sup_of X,R
proof
  let R being interval non empty RelStr;
  let X being set;
  consider a,b being 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 being Element of R st Y is_<=_than a & for b being 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 being 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 being Real st z in Y holds z <= y
        proof
          let z being 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 being 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 being 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 being 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 being 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 being 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 being 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 :: Product of Heyting Lattices

theorem Th9:
  for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
  sup-Semilattice holds product J is with_suprema
proof
  let I being non empty set;
  let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  such that
A1: for i being Element of I holds J.i is sup-Semilattice;
  set IT = product J;
  for x,y being Element of IT ex z being Element of IT st x <= z & y <= z
  & for z9 being Element of IT st x <= z9 & y <= z9 holds z <= z9
  proof
    let x,y being 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 being Element of I holds z.i is Element of J.i
    proof
      let i being 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 being Element of I holds x.i <= z.i & y.i <= z.i
    proof
      let i being 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 being Element of I holds z.i <= z9.i
    proof
      let i being 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 Th10:
  for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
  Semilattice holds product J is with_infima
proof
  let I being non empty set;
  let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  such that
A1: for i being Element of I holds J.i is Semilattice;
  set IT = product J;
  for x,y being Element of IT ex z being Element of IT st x >= z & y >= z
  & for z9 being Element of IT st x >= z9 & y >= z9 holds z >= z9
  proof
    let x,y being 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 being Element of I holds z.i is Element of J.i
    proof
      let i being 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 being Element of I holds x.i >= z.i & y.i >= z.i
    proof
      let i being 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 being Element of I holds z.i >= z9.i
    proof
      let i being 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 Th11:
  for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
  Semilattice for f,g being Element of product J, i being Element of I holds (f
  "/\" g).i = (f.i) "/\" (g.i)
proof
  let I being non empty set;
  let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  such that
A1: for i being Element of I holds J.i is Semilattice;
  let f,g being Element of product J;
  let i being Element of I;
A2: J.i is Semilattice by A1;
  for i being 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 being Element of I holds z.i is Element of J.i
    proof
      let i being 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 being Element of I holds z.i <= f.i & z.i <= g.i
    proof
      let i being 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 being Element of I holds (f "/\" g).i >= f.i "/\" g.i
    proof
      let i being 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 Th12:
  for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being Element of I holds J.i is
sup-Semilattice for f,g being Element of product J, i being Element of I holds
  (f "\/" g).i = (f.i) "\/" (g.i)
proof
  let I being non empty set;
  let J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  such that
A1: for i being Element of I holds J.i is sup-Semilattice;
  let f,g being Element of product J;
  let i being Element of I;
A2: J.i is sup-Semilattice by A1;
  for i being 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 being Element of I holds z.i is Element of J.i
    proof
      let i being 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 being Element of I holds z.i >= f.i & z.i >= g.i
    proof
      let i being 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 being Element of I holds (f "\/" g).i <= f.i "\/" g.i
    proof
      let i being 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 Th13:
  for I being non empty set for J being RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i being 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 being Element of I holds J.i is Heyting complete LATTICE;
A2: for i being 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 being 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 being 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 being 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 being 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 being 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 being Element of A holds (A --> R).i is complete Heyting LATTICE
    by FUNCOP_1:7;
    then product (A --> R) is complete Heyting by Th13;
    hence thesis by YELLOW_1:def 5;
  end;
end;

begin :: Lattice of Fuzzy Sets

definition
  let A be non empty set;
  func FuzzyLattice A -> Heyting complete LATTICE equals
  (RealPoset [. 0,1 .])
  |^ A;
  coherence;
end;

theorem Th14:
  for A being 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 being non empty set holds FuzzyLattice A is constituted-Functions
proof
  let A be non empty set;
  for a being 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 being 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 Th15:
  for R being complete Heyting LATTICE, X being Subset of R, y be
Element of R holds "\/"(X,R) "/\" y = "\/"({x "/\" y where x is 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 is Element of R: x in X}, W = {x "/\" y where x is
  Element of R: x in X};
A1: W c= Z
  proof
    let w be object;
    assume w in W;
    then ex x being 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 being Element of R st z = y "/\" x & x in X;
    hence thesis;
  end;
  then
  ( for z being 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 being non empty set for a being 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 being 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;
  func @a -> Membership_Func of X equals
  a;
  coherence by Lm2;
end;

Lm3: for X be non empty set 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;
  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;
  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;
  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;
  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 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
    proof
      let c be Element of C;
      set f1 = f.c, g1=g.c;
      (C --> RealPoset [. 0,1 .]).c = RealPoset [. 0,1 .] & f1 <= g1 by A3,
FUNCOP_1:7;
      hence thesis by Th3;
    end;
    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,FUNCOP_1:7,WAYBEL_3:28;
    hence thesis by Th3;
  end;
  hence thesis by A2;
end;

theorem
  s <<= t iff for c holds @s.c <= @t.c
proof
  (C,@s)@ = s & (C,@t)@ = t;
  hence thesis by Th16;
end;

theorem 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 being Element of C holds J.c is sup-Semilattice)& J.c =
    RealPoset [. 0 ,1 .] by FUNCOP_1:7;
    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
  s "\/" t = max(@s, @t)
proof
  (C,@s)@ = s & (C,@t)@ = t;
  hence thesis by Th18;
end;

theorem 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 being Element of C holds J.c is Semilattice)& J.c = RealPoset
    [. 0,1 .] by FUNCOP_1:7;
    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
  s "/\" t = min(@s, @t)
proof
  (C,@s)@ = s & (C,@t)@ = t;
  hence thesis by Th20;
end;

begin :: Associativity of composition of fuzzy relations

scheme
  SupDistributivity { L() -> complete LATTICE, X, Y() -> non empty set, F(set,
set) -> Element of L(), P,Q[set]}: "\/"({ "\/"({F(x,y) where y is Element of Y(
  ): Q[y]}, L()) where x is Element of X(): P[x] }, L()) = "\/"({F(x,y) where x
  is Element of X(), y is Element of Y(): P[x] & Q[y]}, L()) proof
  defpred R[set] means ex x being Element of X() st P[x] & for a being set
  holds a in $1 iff ex y being Element of Y() st a = F(x,y) & Q[y];
A1: "\/" ({ "\/"(A,L()) where A is Subset of L(): R[A] },L()) = "\/" (union
  {A where A is Subset of L(): R[A]}, L()) from YELLOW_3:sch 5;
A2: {F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y] }
  c= union {A where A is Subset of L(): R[A]}
  proof
    let a be object;
    assume a in {F(x,y) where x is Element of X(), y is Element of Y() : P[x
    ] & Q[y]};
    then consider x being Element of X(), y being 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 is Element of Y(): Q[y9]};
    A1 c= the carrier of L()
    proof
      let b be object;
      assume b in A1;
      then ex y9 being 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 is 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 is Element of Y(): Q[y]}, L()) where x is
  Element of X(): P[x] } c= { "\/"(A,L()) where A is Subset of L(): R[A] }
  proof
    let a be object;
    assume a in { "\/"({F(x,y) where y is Element of Y(): Q[y]}, L()) where
    x is Element of X(): P[x] };
    then consider x being Element of X() such that
A8: a = "\/"({F(x,y) where y is Element of Y(): Q[y]}, L()) and
A9: P[x];
    ex A1 being Subset of L() st a = "\/"(A1,L()) & R[A1]
    proof
      set A2 = {F(x,y) where y is Element of Y(): Q[y]};
      A2 c= the carrier of L()
      proof
        let b be object;
        assume b in A2;
        then ex y being 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 is Subset of L(): R[A] } c= { "\/"({F(x,y) where
  y is Element of Y(): Q[y]}, L()) where x is Element of X(): P[x] }
  proof
    let a be object;
    assume a in { "\/"(A,L()) where A is Subset of L(): R[A] };
    then consider A1 being Subset of L() such that
A11: a = "\/"(A1,L()) and
A12: R[A1];
    consider x being Element of X() such that
A13: P[x] and
A14: for a being set holds a in A1 iff ex y being Element of Y() st a
    = F(x,y) & Q[y] by A12;
    now
      let a be object;
      a in {F(x,y) where y is Element of Y(): Q[y]} iff ex y being
      Element of Y() st a = F(x,y) & Q[y];
      hence a in A1 iff a in {F(x,y) where y is Element of Y(): Q[y]} by A14;
    end;
    then A1 = {F(x,y) where y is Element of Y(): Q[y]} by TARSKI:2;
    hence thesis by A11,A13;
  end;
  union {A where A is Subset of L(): R[A]} c= {F(x,y) where x is Element
  of X(), y is Element of Y(): P[x] & Q[y]}
  proof
    let a be object;
    assume a in union {A where A is Subset of L(): R[A]};
    then consider A1 be set such that
A15: a in A1 and
A16: A1 in {A where A is Subset of L(): R[A]} by TARSKI:def 4;
    consider A2 being Subset of L() such that
A17: A1 = A2 and
A18: R[A2] by A16;
    consider x being Element of X() such that
A19: P[x] and
A20: for a being set holds a in A2 iff ex y being Element of Y() st a =
    F(x,y) & Q[y] by A18;
    ex y being Element of Y() st a = F(x,y) & Q[y] by A15,A17,A20;
    hence thesis by A19;
  end;
  then union {A where A is Subset of L(): R[A]} = {F(x,y) where x is Element
  of X( ), y is Element of Y(): P[x] & Q[y]} by A2;
  hence thesis by A1,A10,A7,XBOOLE_0:def 10;
end;

scheme
  SupDistributivity9 { L() -> complete LATTICE, X, Y() -> non empty set, F(set
,set) -> Element of L(), P,Q[set]}: "\/"({ "\/"({F(x,y) where x is Element of X
  (): P[x]},L()) where y is Element of Y(): Q[y] }, L()) = "\/"({F(x,y) where x
  is Element of X(), y is Element of Y(): P[x] & Q[y]}, L()) proof
  defpred R[set] means ex y being Element of Y() st Q[y] & for a being set
  holds a in $1 iff ex x being Element of X() st a = F(x,y) & P[x];
A1: "\/" ({ "\/"(A,L()) where A is Subset of L(): R[A] },L()) = "\/" (union
  {A where A is Subset of L(): R[A]}, L()) from YELLOW_3:sch 5;
A2: {F(x,y) where x is Element of X(), y is Element of Y(): P[x] & Q[y] }
  c= union {A where A is Subset of L(): R[A]}
  proof
    let a be object;
    assume a in {F(x,y) where x is Element of X(), y is Element of Y() : P[x
    ] & Q[y]};
    then consider x being Element of X(), y being Element of Y() such that
A3: a = F(x,y) & P[x] and
A4: Q[y];
    set A1 = {F(x9,y) where x9 is Element of X(): P[x9]};
    A1 c= the carrier of L()
    proof
      let b be object;
      assume b in A1;
      then ex x9 being 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 is Subset of L(): R[A]};
    a in A1 by A3;
    hence thesis by A5,TARSKI:def 4;
  end;
A6: { "\/"({F(x,y) where x is Element of X(): P[x]}, L()) where y is
  Element of Y(): Q[y] } c= { "\/"(A,L()) where A is Subset of L(): R[A] }
  proof
    let a be object;
    assume a in { "\/"({F(x,y) where x is Element of X(): P[x]}, L()) where
    y is Element of Y(): Q[y] };
    then consider y being Element of Y() such that
A7: a = "\/"({F(x,y) where x is Element of X(): P[x]}, L()) and
A8: Q[y];
    ex A1 being Subset of L() st a = "\/"(A1,L()) & R[A1]
    proof
      set A2 = {F(x,y) where x is Element of X(): P[x]};
      A2 c= the carrier of L()
      proof
        let b be object;
        assume b in A2;
        then ex x being 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 is Subset of L(): R[A] } c= { "\/"({F(x,y) where
  x is Element of X(): P[x]}, L()) where y is Element of Y(): Q[y] }
  proof
    let a be object;
    assume a in { "\/"(A,L()) where A is Subset of L(): R[A] };
    then consider A1 being Subset of L() such that
A10: a = "\/"(A1,L()) and
A11: R[A1];
    consider y being Element of Y() such that
A12: Q[y] and
A13: for a being set holds a in A1 iff ex x being Element of X() st a
    = F(x,y) & P[x] by A11;
    now
      let a be object;
      a in {F(x,y) where x is Element of X(): P[x]} iff ex x being
      Element of X() st a = F(x,y) & P[x];
      hence a in A1 iff a in {F(x,y) where x is Element of X(): P[x]} by A13;
    end;
    then A1 = {F(x,y) where x is Element of X(): P[x]} by TARSKI:2;
    hence thesis by A10,A12;
  end;
  union {A where A is Subset of L(): R[A]} c= {F(x,y) where x is Element
  of X(), y is Element of Y(): P[x] & Q[y]}
  proof
    let a be object;
    assume a in union {A where A is Subset of L(): R[A]};
    then consider A1 be set such that
A14: a in A1 and
A15: A1 in {A where A is Subset of L(): R[A]} by TARSKI:def 4;
    consider A2 being Subset of L() such that
A16: A1 = A2 and
A17: R[A2] by A15;
    consider y being Element of Y() such that
A18: Q[y] and
A19: for a being set holds a in A2 iff ex x being Element of X() st a =
    F(x,y) & P[x] by A17;
    ex x being Element of X() st a = F(x,y) & P[x] by A14,A16,A19;
    hence thesis by A18;
  end;
  then union {A where A is Subset of L(): R[A]} = {F(x,y) where x is Element
  of X( ), y is Element of Y(): P[x] & Q[y]} by A2;
  hence thesis by A1,A9,A6,XBOOLE_0:def 10;
end;

scheme
  FraenkelF9R9{ A() -> non empty set,B() -> non empty set, F1, F2(set,set) ->
set, P[set,set] } : { F1(u1,v1) where u1 is (Element of A()), v1 is Element of
B() : P[u1,v1] } = { F2(u2,v2) where u2 is (Element of A()), v2 is Element of B
  () : P[u2,v2] }
provided
A1: for u being (Element of A()), v being Element of B() st P[u,v] holds
F1(u,v) = F2(u,v)
proof
  set A = { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[
u1,v1] }, C = { F2(u3,v3) where u3 is (Element of A()), v3 is 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 being (Element of A()), v being 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 being (Element of A()), v being 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
  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 is (Element of A()), v1
  is Element of B() : P[u1,v1] } = { F2(u2,v2) where u2 is (Element of A()), v2
  is Element of B() : Q[u2,v2] }
provided
A1: for u being (Element of A()), v being Element of B() holds P[u,v]
iff Q[u,v] and
A2: for u being (Element of A()), v being Element of B() st P[u,v] holds
F1(u,v) = F2(u,v)
proof
  set A = { F1(u1,v1) where u1 is (Element of A()), v1 is Element of B() : P[
u1,v1] }, B = { F2(u2,v2) where u2 is (Element of A()), v2 is Element of B() :
Q[u2,v2] }, C = { F2(u3,v3) where u3 is (Element of A()), v3 is 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
  SupCommutativity { L() -> complete LATTICE, X, Y() -> non empty set, F1, F2(
set,set) -> Element of L(), P,Q[set]}: "\/"({ "\/"({F1(x,y) where y is Element
of Y(): Q[y]}, L()) where x is Element of X(): P[x] }, L()) = "\/"({ "\/"({F2(
x9,y9) where x9 is Element of X(): P[x9]}, L()) where y9 is Element of Y(): Q[
  y9] }, L())
provided
A1: for x being Element of X(), y being Element of Y() st P[x] & Q[y]
holds F1(x,y) = F2(x,y)
proof
  defpred X[set,set] means P[$1] & Q[$2];
A2: for x being Element of X(), y being Element of Y() holds X[x,y] iff X[x,
  y];
A3: for x being Element of X(), y being Element of Y() st X[x,y] holds F1(x,
  y) = F2(x,y) by A1;
A4: {F1(x9,y9) where x9 is Element of X(), y9 is Element of Y(): X[x9,y9]} =
  {F2(x,y) where x is Element of X(), y is Element of Y(): X[x,y]} from
  FraenkelF699R(A2,A3);
A5: "\/"({ "\/"({F1(x,y) where y is Element of Y(): Q[y]}, L()) where x is
  Element of X(): P[x] }, L()) ="\/"({F1(x,y) where x is Element of X(), y is
  Element of Y(): P[x] & Q[y]}, L()) from SupDistributivity;
  "\/"({ "\/"({F2(x9,y9) where x9 is Element of X(): P[x9]}, L()) where y9
  is Element of Y(): Q[y9] }, L()) ="\/"({F2(x9,y9) where x9 is Element of X(),
  y9 is Element of Y(): P[x9] & Q[y9]}, L()) from SupDistributivity9
    .="\/"({F1(x9,y9) where x9 is Element of X(), y9 is Element of Y(): P[x9
  ] & Q[y9]}, L()) by A4;
  hence thesis by A5;
end;

Lm4: for X,Y,Z being non empty set for R being RMembership_Func of X,Y for S
being RMembership_Func of Y,Z for x being Element of X, z being Element of Z
holds rng min(R,S,x,z) =
the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y
& rng min(R,S,x,z) <> {}
proof
  let X,Y,Z being non empty set;
  let R being RMembership_Func of X,Y;
  let S being RMembership_Func of Y,Z;
  let x being Element of X, z being Element of Z;
  set L = the set of all R.(x,y) "/\" S.(y,z) where y is 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 being 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 being 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 Th22:
  for X,Y,Z being non empty set for R being RMembership_Func of X,
Y for S being RMembership_Func of Y,Z for x being Element of X, z being Element
of Z holds (R (#) S).(x,z) =
"\/"((the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y),
RealPoset [. 0,1 .])
proof
  let X,Y,Z being non empty set;
  let R being RMembership_Func of X,Y;
  let S being RMembership_Func of Y,Z;
  let x being Element of X, z being Element of Z;
  set L = the set of all R.(x,y) "/\" S.(y,z) where y is 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 being 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 is 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 being 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 being 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 being 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 being non empty set for R being RMembership_Func of X,Y for S
being RMembership_Func of Y,Z for x being Element of X, z being Element of Z
for a being Element of RealPoset [. 0,1 .] holds (R (#) S).(x,z) "/\" a = "\/"(
(the set of all R.(x,y) "/\" S.(y,z) "/\" a where y is Element of Y),
RealPoset [. 0,1 .])
proof
  let X,Y,Z being non empty set;
  let R being RMembership_Func of X,Y;
  let S being RMembership_Func of Y,Z;
  let x being Element of X, z being Element of Z;
  let a being Element of RealPoset [. 0,1 .];
A1: the set of all R.(x,y) "/\" S.(y,z) where y is 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 is Element of Y;
    then ex t being Element of Y st d = R.(x,t) "/\" S.(t,z);
    hence thesis;
  end;
  set A = {b "/\" a where b is Element of RealPoset [. 0,1 .]:
  b in the set of all R.(x,y)
  "/\" S.(y,z) where y is Element of Y};
  set B = the set of all R.(x,y) "/\" S.(y,z) "/\" a where y is 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 being 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 is Element of Y;
      ex y being 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 being 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 is 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 is Element of Y), RealPoset [. 0,1 .]) "/\" a by Th22
    .= "\/"({b "/\" a where b is Element of RealPoset [. 0,1 .]:
    b in the set of all R.(x,y) "/\" S.(y,z) where y is Element of Y},
    RealPoset [. 0,1 .]) by A1,Th15;
  hence thesis by A2,TARSKI:2;
end;

Lm6: for X,Y,Z being non empty set for R being RMembership_Func of X,Y for S
being RMembership_Func of Y,Z for x being Element of X, z being Element of Z
for a being Element of RealPoset [. 0,1 .] holds a "/\" (R (#) S).(x,z) = "\/"(
(the set of all a "/\" R.(x,y) "/\" S.(y,z) where y is Element of Y),
RealPoset [. 0,1 .])
proof
  let X,Y,Z being non empty set;
  let R being RMembership_Func of X,Y;
  let S being RMembership_Func of Y,Z;
  let x being Element of X, z being Element of Z;
  let a being Element of RealPoset [. 0,1 .];
  set A = the set of all a "/\" R.(x,y) "/\" S.(y,z) where y is Element of Y;
  set B = the set of all R.(x,y) "/\" S.(y,z) "/\" a where y is 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 being 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 being 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
  for X,Y,Z,W being non empty set for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z for T being 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 being object st x in X & w in W
    holds ((R (#) S) (#) T).(x,w) = (R (#) (S (#) T)).(x,w)
  proof
    let x,w being 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 is Element of Y), RealPoset [. 0,1 .]) where z is Element of Z;
    set B = the set of all (R (#) S).(x,z) "/\" T.(z,w)
    where z is Element of Z;
    set C = the set of all "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\"
    T.(z,w)  where z is Element of Z),
    RealPoset [. 0,1 .]) where y is Element of Y;
    set D = the set of all R.(x,y) "/\" ((S (#) T).(y,w))
    where y is 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 being Element of Z such that
A5:     a = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w)
        where y is 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 being 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 is Element of Y), RealPoset [. 0,1 .]) by A6,Lm5;
      hence thesis;
    end;
A7: for y being Element of Y, z being Element of Z st X[y] & X[z] holds U
    (y,z) = U(y,z);
A8: "\/"({"\/"({U(y,z) where z is Element of Z: X[z]}, RealPoset [. 0,1
.]) where y is Element of Y :X[y]}, RealPoset [. 0,1 .]) ="\/"({"\/"({U(y1,z1)
where y1 is Element of Y: X[y1]}, RealPoset [. 0,1 .]) where z1 is 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 being Element of Y such that
A9:     c = "\/"((the set of all R.(x,y) "/\" S.(y,z) "/\" T.(z,w) where z is
        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 being 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 is 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
is Element of Z), RealPoset [. 0,1 .]) & (R (#) (S (#) T)).(
    x, w) = "\/"((the set of all R.(x,y) "/\" ((S (#) T).(y,w))
    where y is Element of Y), RealPoset [. 0,1 .]) by Th22;
    hence thesis by A4,A11,A8,TARSKI:2;
  end;
  thus thesis by A1;
end;