:: Basic Formal Properties of Triangular Norms and Conorms
::  by Adam Grabowski
:: 
:: Received June 27, 2017
:: Copyright (c) 2017-2018 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, XXREAL_1, REAL_1, XXREAL_0, SUBSET_1, CARD_1, ARYTM_1,
      ARYTM_3, FUNCT_1, XBOOLE_0, RELAT_1, XREAL_0, FUNCT_7, FUZNORM1,
      ZFMISC_1, BINOP_1, MSAFREE2, MEMBERED;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
      MEMBERED, ZFMISC_1, BINOP_1, VALUED_0, RELAT_1, XXREAL_2, XREAL_0,
      COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, REAL_1, SEQ_4, RCOMP_1,
      PRE_TOPC, TOPS_2, METRIC_1, DOMAIN_1, STRUCT_0, TOPMETR, TSEP_1, TMAP_1,
      FUZZY_1, BORSUK_1, MEASURE5;
 constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, CONNSP_1, TOPS_2,
      TMAP_1, TOPMETR, XXREAL_2, BINOP_2, RVSUM_1, PCOMPS_1, BINOP_1, FUZZY_1,
      XREAL_0, INTEGRA1, MESFUNC5, EXTREAL1;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
      MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, TOPMETR, CONNSP_1,
      ORDINAL1, INTEGRA1, INTEGRA2, MEASURE5, EXTREAL1, SUPINF_1, SUPINF_2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, FUNCT_2, XXREAL_2, SUBSET_1;
 equalities SUBSET_1, STRUCT_0, BINOP_1, ORDINAL1, PARTFUN1;
 expansions TARSKI, FUNCT_2, XXREAL_2;
 theorems SUBSET_1, FUNCT_1, FUNCT_2, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1,
      BINOP_1, ZFMISC_1, FUZZY_2;
 schemes BINOP_1, SCHEME1;

begin :: Preliminaries

registration
  cluster [.0,1.] -> non empty;
  coherence by XXREAL_1:1;
end;

theorem MinIn01:
  for a,b being Element of [.0,1.] holds
    min (a,b) in [.0,1.]
  proof
    let a,b be Element of [.0,1.];
    min (a,b) = a or min (a,b) = b by XXREAL_0:15;
    hence thesis;
  end;

theorem MaxIn01:
  for a,b being Element of [.0,1.] holds
    max (a,b) in [.0,1.]
  proof
    let a,b be Element of [.0,1.];
    max (a,b) = a or max (a,b) = b by XXREAL_0:16;
    hence thesis;
  end;

theorem Lemma1:
  for a,b being Element of [.0,1.] holds
    a * b in [.0,1.]
  proof
    let a,b be Element of [.0,1.];
A0: 1 >= a >= 0 & 1 >= b >= 0 by XXREAL_1:1; then
    1 >= a * b by XREAL_1:160;
    hence thesis by XXREAL_1:1,A0;
  end;

theorem Lemma2:
  for a,b being Element of [.0,1.] holds
    max (0, a + b - 1) in [.0,1.]
  proof
    let a,b be Element of [.0,1.];
A1: max (0, a + b - 1) >= 0 by XXREAL_0:25;
    a <= 1 & b <= 1 by XXREAL_1:1; then
    a + b <= 1 + 1 by XREAL_1:7; then
A2: a + b - 1 <= 2 - 1 by XREAL_1:9;
    max (0, a + b - 1) = 0 or max (0, a + b - 1) = a + b - 1
      by XXREAL_0:16;
    hence thesis by A1,XXREAL_1:1,A2;
  end;

theorem Lemma2a:
  for a,b being Element of [.0,1.] holds
    min (a + b, 1) in [.0,1.]
  proof
    let a,b be Element of [.0,1.];
A1: min (a + b, 1) <= 1 by XXREAL_0:17;
A2: a >= 0 & b >= 0 by XXREAL_1:1;
    min (1, a + b) = 1 or min (1, a + b) = a + b by XXREAL_0:15;
    hence thesis by A1,XXREAL_1:1,A2;
  end;

theorem Lemma3:
  for a,b,c being Element of [.0,1.] holds
    max (0,max(0,a+b-1)+c-1) = max (0,a+max(0,b+c-1)-1)
  proof
    let a,b,c be Element of [.0,1.];
A1: 0 <= a & 0 <= b & 0 <= c by XXREAL_1:1;
zz: c - 0 <= 1 by XXREAL_1:1; then
    c - 1 <= 0 by XREAL_1:12; then
y2: (c-1) + (a + b -1) <= 0 + (a + b -1) by XREAL_1:6;
      per cases;
      suppose
Z0:     0 <= a + b - 1 & 0 <= b+c-1; then
Z1:     max (0,a+b-1) = a + b -1 by XXREAL_0:def 10;
        max (0,b+c-1) = b + c -1 by Z0,XXREAL_0:def 10;
        hence thesis by Z1;
      end;
      suppose
Z0:     0 > a + b - 1 & 0 <= b+c-1; then
Z1:     max (0,a+b-1) = 0 by XXREAL_0:def 10;
Z2:     max (0,b+c-1) = b + c - 1 by Z0,XXREAL_0:def 10;
        max (0,max(0,a+b-1)+c-1) = 0 by zz,XXREAL_0:def 10,Z1,XREAL_1:12
          .= max (0,a+max(0,b+c-1)-1) by Z2,y2,Z0,XXREAL_0:def 10;
        hence thesis;
      end;
      suppose
Z0:     0 > a + b - 1 & 0 > b + c-1; then
Z3:     c-1 < 0 & a - 1 < 0 by XREAL_1:9,A1,XREAL_1:31;
Z1:     max (0,a+b-1) = 0 by Z0,XXREAL_0:def 10;
Z2:     max (0,b+c-1) = 0 by Z0,XXREAL_0:def 10;
        max (0,max(0,a+b-1)+c-1) = 0 by Z3,XXREAL_0:def 10,Z1
          .= max (0,a+max(0,b+c-1)-1) by Z2,Z3,XXREAL_0:def 10;
        hence thesis;
      end;
      suppose
Z0:     0 <= a + b - 1 & 0 > b+c-1;
ds:     a - 0 <= 1 by XXREAL_1:1; then
        a - 1 <= 0 by XREAL_1:12; then
sb:     a-1+(b+c-1) <= 0 + 0 by Z0;
Z1:     max (0,a+b-1) = a + b -1 by Z0,XXREAL_0:def 10;
        max (0,max(0,a+b-1)+c-1) = 0 by sb,XXREAL_0:def 10,Z1
          .= max (0,a+0-1) by XXREAL_0:def 10,XREAL_1:12,ds
          .= max (0,a+max(0,b+c-1)-1) by Z0,XXREAL_0:def 10;
        hence thesis;
      end;
  end;

theorem OpIn01:
  for a being Element of [.0,1.] holds
    1 - a in [.0,1.]
  proof
    let a be Element of [.0,1.];
    0 <= a <= 1 by XXREAL_1:1; then
    1 - 1 <= 1 - a <= 1 - 0 by XREAL_1:13;
    hence thesis by XXREAL_1:1;
  end;

theorem abMinab01:
  for a, b being Element of [.0,1.] holds
    a + b - a * b in [.0,1.]
  proof
    let a, b be Element of [.0,1.];
S1: 1 - b in [.0,1.] by OpIn01; then
    a * (1 - b) in [.0,1.] by Lemma1; then
B1: a * (1 - b) >= 0 by XXREAL_1:1;
a0: b >= 0 by XXREAL_1:1;
S2: a <= 1 & b <= 1 by XXREAL_1:1;
    0 <= 1 - b <= 1 by S1,XXREAL_1:1; then
    a * (1 - b) <= 1 * (1 - b) by S2,XREAL_1:64; then
    a * (1 - b) + b <= 1 - b + b by XREAL_1:6;
    hence thesis by XXREAL_1:1,a0,B1;
  end;

theorem HamIn01:
  for a, b being Element of [.0,1.] holds
    (a * b) / (a + b - a * b) in [.0,1.]
  proof
    let a, b be Element of [.0,1.];
A1: a * b in [.0,1.] by Lemma1;
    a + b - a * b in [.0,1.] by abMinab01; then
A2: a + b - a * b >= 0 by XXREAL_1:1;
T0: a * b >= 0 by A1,XXREAL_1:1;
    0 <= a & b <= 1 by XXREAL_1:1; then
S1: a * b <= a by XREAL_1:153;
    0 <= b & a <= 1 by XXREAL_1:1; then
    a * b <= b by XREAL_1:153; then
    a * b + a * b <= a + b by S1,XREAL_1:7; then
    a * b <= a + b - a * b by XREAL_1:19; then
    (a * b) / (a + b - a * b) <= 1 by XREAL_1:183,T0;
    hence thesis by T0,A2,XXREAL_1:1;
  end;

theorem DiffMax:
  for a,b being Element of [.0,1.] st max (a,b) <> 1 holds
    a <> 1 & b <> 1
  proof
    let a,b be Element of [.0,1.];
    assume
A1: max (a,b) <> 1;
A2: a <= 1 & b <= 1 by XXREAL_1:1;
    assume a = 1 or b = 1; then
    per cases;
    suppose a = 1;
      hence thesis by A1,A2,XXREAL_0:def 10;
    end;
    suppose b = 1;
      hence thesis by A1,A2,XXREAL_0:def 10;
    end;
  end;

theorem Lemacik:
  for x, y being Element of [.0,1.] holds
    x * y = x + y implies x = 0
  proof
    let x, y be Element of [.0,1.];
    assume x * y = x + y; then
z1: y * (1 - x) = -x;
    assume x <> 0; then
    0 < x <= 1 by XXREAL_1:1; then
A4: -x < -0 by XREAL_1:25;
    1 - x in [.0,1.] by OpIn01; then
A2: 0 <= 1 - x & 1 - x <= 1 by XXREAL_1:1;
    y < 0 by A4,A2,z1;
    hence thesis by XXREAL_1:1;
  end;

theorem MaxMin:
  for a,b being Element of [.0,1.] holds
    max (a,b) = 1 - min (1-a,1-b)
  proof
    let a,b be Element of [.0,1.];
    per cases;
    suppose
A1:   a <= b; then
      min (1-a,1-b) = 1 - b by XXREAL_0:def 9,XREAL_1:10;
      hence thesis by A1,XXREAL_0:def 10;
    end;
    suppose
A1:   a > b; then
      min (1-a,1-b) = 1 - a by XXREAL_0:def 9,XREAL_1:10;
      hence thesis by A1,XXREAL_0:def 10;
    end;
  end;

theorem LukasiDual:
  for a,b being Element of [.0,1.] holds
    min (a+b,1) = 1 - max (0,1-a+(1-b)-1)
  proof
    let a,b be Element of [.0,1.];
    per cases;
    suppose
A1:   a + b <= 1; then
A2:   a + b - (a + b) <= 1 - (a + b) by XREAL_1:9;
      min (a + b, 1) = 1 - (1 - a - b) by A1,XXREAL_0:def 9
         .= 1 - max (0,1-a+(1-b)-1) by A2,XXREAL_0:def 10;
      hence thesis;
    end;
    suppose
A1:   a + b > 1; then
A2:   a + b - (a + b) > 1 - (a + b) by XREAL_1:9;
      min (a+b,1) = 1 - 0 by A1,XXREAL_0:def 9
         .= 1 - max (0,1-a+(1-b)-1) by A2,XXREAL_0:def 10;
      hence thesis;
    end;
  end;

theorem HamCoIn01:
  for a,b being Element of [.0,1.] holds
    (a + b - 2 * a * b) / (1 - a * b) in [.0,1.]
  proof
    let a,b be Element of [.0,1.];
    0 <= a & b <= 1 by XXREAL_1:1; then
S1: a * b <= a by XREAL_1:153;
S2: 0 <= b & a <= 1 by XXREAL_1:1; then
    a * b <= b by XREAL_1:153; then
    a * b + a * b <= a + b by S1,XREAL_1:7; then
S5: a * b - a * b <= a + b - a * b - a * b by XREAL_1:9,19;
    1 - b in [.0,1.] by OpIn01; then
    1 - b >= 0 by XXREAL_1:1; then
    a * (1 - b) <= 1 * (1 - b) by S2,XREAL_1:64; then
    a - a * b + b <= 1 - b + b by XREAL_1:6; then
    a + b - a * b - a * b <= 1 - a * b by XREAL_1:9; then
B9: (a + b - 2 * a * b) / (1 - a * b) <= 1 by XREAL_1:183,S5;
    a * b in [.0,1.] by Lemma1; then
    a * b <= 1 by XXREAL_1:1; then
    1 - a * b >= 1 - 1 by XREAL_1:10;
    hence thesis by XXREAL_1:1,B9,S5;
  end;

registration let f be BinOp of [.0,1.];
             let a, b be Real;
  cluster f.(a,b) -> real;
  coherence
  proof
    per cases;
    suppose
      a in [.0,1.] & b in [.0,1.]; then
      f.(a,b) in [.0,1.] by BINOP_1:17;
      hence thesis;
    end;
    suppose
      not a in [.0,1.] or not b in [.0,1.]; then
      not [a,b] in dom f by ZFMISC_1:87;
      hence thesis by FUNCT_1:def 2;
    end;
  end;
end;

theorem NormIn01:
  for a,b being Real,
      t being BinOp of [.0,1.] holds
   t.(a,b) in [.0,1.]
  proof
    let a,b be Real;
    let t be BinOp of [.0,1.];
    per cases;
    suppose a in [.0,1.] & b in [.0,1.]; then
      [a,b] in [:[.0,1.], [.0,1.]:] by ZFMISC_1:87;
      hence thesis by FUNCT_2:5;
    end;
    suppose not a in [.0,1.] or not b in [.0,1.]; then
      not [a,b] in dom t by ZFMISC_1:87; then
      t. [a,b] = 0 by FUNCT_1:def 2;
      hence thesis by XXREAL_1:1;
    end;
  end;

theorem CoIn01:
  for f being BinOp of [.0,1.],
      a, b being Real holds
   1 - f.(1 - a, 1 - b) in [.0,1.]
  proof
    let f be BinOp of [.0,1.];
    let a,b be Real;
    per cases;
    suppose a in [.0,1.] & b in [.0,1.]; then
      reconsider aa = a, bb = b as Element of [.0,1.];
      f.(1-aa, 1-bb) in [.0,1.] by NormIn01;
      hence thesis by OpIn01;
    end;
    suppose not a in [.0,1.] or not b in [.0,1.];
      f.(1-a,1-b) in [.0,1.] by NormIn01;
      hence thesis by OpIn01;
    end;
  end;

theorem MES57: ::: move theorems from MESFUNC5 to XXREAL_0
  for x,y,k being Real st k <= 0 holds
    k*min(x,y) = max(k*x,k*y) & k*max(x,y) = min(k*x,k*y)
proof
  let x,y,k be Real;
  assume
A1: k <= 0;
  hereby
    per cases by XXREAL_0:16;
    suppose
      max(x,y) = x; then
A2:   y <= x by XXREAL_0:def 10;
      then max(k*x,k*y) = k*y by XXREAL_0:def 10,A1,XREAL_1:65;
      hence k*min(x,y) = max(k*x,k*y) by A2,XXREAL_0:def 9;
    end;
    suppose
      max(x,y) = y; then
A3:   x <= y by XXREAL_0:def 10;
      then max(k*x,k*y) = k*x by XXREAL_0:def 10,A1,XREAL_1:65;
      hence k*min(x,y) = max(k*x,k*y) by A3,XXREAL_0:def 9;
    end;
  end;
  per cases by XXREAL_0:15;
  suppose
    min(x,y) = x; then
A4: x <= y by XXREAL_0:def 9;
    then min(k*x,k*y) = k*y by XXREAL_0:def 9,A1,XREAL_1:65;
    hence thesis by A4,XXREAL_0:def 10;
  end;
  suppose
    min(x,y) = y; then
A5: y <= x by XXREAL_0:def 9;
    then min(k*y,k*x) = k*x by XXREAL_0:def 9,A1,XREAL_1:65;
    hence thesis by A5,XXREAL_0:def 10;
  end;
end;

begin :: Basic Example of a Triangular Norm and Conorm: min and max

definition let A be real-membered set;
           let f be BinOp of A;
  attr f is monotonic means :MonDef:
    for a,b,c,d being Element of A st
      a <= c & b <= d holds f.(a,b) <= f.(c,d);
  attr f is with-1-identity means :IdDef:
    for a being Element of A holds f.(a,1) = a;
  attr f is with-1-annihilating means
    for a being Element of A holds f.(a,1) = 1;
  attr f is with-0-identity means :ZeroDef:
    for a being Element of A holds f.(a,0) = a;
  attr f is with-0-annihilating means
    for a being Element of A holds f.(a,0) = 0;
end;

scheme ExBinOp { A() -> non empty real-membered set, F(Real, Real) -> set } :
  ex f being BinOp of A() st
    for a,b being Element of A() holds f.(a,b) = F(a,b)
  provided
A2:  for a,b being Element of A() holds F(a,b) in A()
  proof
    set A = A();
    deffunc F(Element of A, Element of A) = In (F($1,$2),A);
    ex f being Function of [:A,A:], A st
    for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being BinOp of A such that
A1: for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y);
    take f;
    let a,b be Element of A;
    f.(a,b) = F(a,b) by A1;
    hence thesis by SUBSET_1:def 8,A2;
  end;

definition
  func minnorm -> BinOp of [.0,1.] means :MinDef:
    for a,b being Element of [.0,1.] holds
      it.(a,b) = min (a,b);
  existence
  proof
    set A = [.0,1.];
    deffunc F(Element of A, Element of A) = In (min ($1,$2),A);
    ex f being Function of [:A,A:], A st
    for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being BinOp of A such that
A1: for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y);
    take f;
    let a,b be Element of [.0,1.];
A2: f.(a,b) = F(a,b) by A1;
    min (a,b) = a or min (a,b) = b by XXREAL_0:15;
    hence thesis by A2,SUBSET_1:def 8;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds f1.(a,b) = min (a,b) and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = min (a,b);
A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1
          .= dom f2 by FUNCT_2:def 1;
    for x,y being object st
      [x,y] in dom f1 holds f1.(x,y) = f2.(x,y)
    proof
      let x,y be object;
      assume [x,y] in dom f1; then
      reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87;
      f1.(xx,yy) = min (xx,yy) by A1
                .= f2.(xx,yy) by A2;
      hence thesis;
    end;
    hence thesis by A3,BINOP_1:20;
  end;
end;

registration
  cluster minnorm -> commutative associative monotonic with-1-identity;
  coherence
  proof
    set f = minnorm;
A1: for a,b being Element of [.0,1.] holds
      f.(a,b) = f.(b,a)
    proof
      let a,b be Element of [.0,1.];
      f.(a,b) = min(a,b) by MinDef
             .= f.(b,a) by MinDef;
      hence thesis;
    end;
AA: for a,b,c being Element of [.0,1.] holds
      f.(f.(a,b),c) = f.(a,f.(b,c))
    proof
      let a,b,c be Element of [.0,1.];
a2:   min (a,b) = a or min (a,b) = b by XXREAL_0:15;
a3:   min (b,c) = b or min (b,c) = c by XXREAL_0:15;
      f.(f.(a,b),c) = f.(min(a,b),c) by MinDef
      .= min (min(a,b),c) by MinDef,a2
      .= min (a,min(b,c)) by XXREAL_0:33
      .= f.(a,min(b,c)) by a3,MinDef
      .= f.(a,f.(b,c)) by MinDef;
      hence thesis;
    end;
D1: for a,b,c,d being Element of [.0,1.] st
      a <= c & b <= d holds f.(a,b) <= f.(c,d)
    proof
      let a,b,c,d be Element of [.0,1.];
      assume a <= c & b <= d; then
      min (a,b) <= min (c,d) by XXREAL_0:18; then
      min (a,b) <= f.(c,d) by MinDef;
      hence thesis by MinDef;
    end;
    for a being Element of [.0,1.] holds f.(a,1) = a
    proof
      let a be Element of [.0,1.];
T1:   1 in [.0,1.] by XXREAL_1:1;
      a <= 1 by XXREAL_1:1; then
      min (a,1) = a by XXREAL_0:def 9;
      hence thesis by MinDef,T1;
    end;
    hence thesis by BINOP_1:def 2,def 3,A1,AA,D1;
  end;
end;

registration
  cluster commutative associative monotonic with-1-identity
    for BinOp of [.0,1.];
  existence
  proof
    take minnorm;
    thus thesis;
  end;
end;

definition
  mode t-norm is
    commutative associative monotonic with-1-identity BinOp of [.0,1.];
end;

definition
  func maxnorm -> BinOp of [.0,1.] means :MaxDef:
    for a,b being Element of [.0,1.] holds
      it.(a,b) = max (a,b);
  existence
  proof
    set A = [.0,1.];
    deffunc F(Element of A, Element of A) = In (max ($1,$2),A);
    ex f being Function of [:A,A:], A st
    for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being BinOp of A such that
A1: for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y);
    take f;
    let a,b be Element of [.0,1.];
A2: f.(a,b) = F(a,b) by A1;
    max (a,b) = a or max (a,b) = b by XXREAL_0:16;
    hence thesis by A2,SUBSET_1:def 8;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds f1.(a,b) = max (a,b) and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = max (a,b);
A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1
          .= dom f2 by FUNCT_2:def 1;
    for x,y being object st
      [x,y] in dom f1 holds f1.(x,y) = f2.(x,y)
    proof
      let x,y be object;
      assume [x,y] in dom f1; then
      reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87;
      f1.(xx,yy) = max (xx,yy) by A1
                .= f2.(xx,yy) by A2;
      hence thesis;
    end;
    hence thesis by A3,BINOP_1:20;
  end;
end;

registration
  cluster maxnorm -> commutative associative monotonic with-0-identity;
  coherence
  proof
    set f = maxnorm;
A1: for a,b being Element of [.0,1.] holds
      f.(a,b) = f.(b,a)
    proof
      let a,b be Element of [.0,1.];
      f.(a,b) = max (a,b) by MaxDef
             .= f.(b,a) by MaxDef;
      hence thesis;
    end;
DD: for a,b,c being Element of [.0,1.] holds
      f.(f.(a,b),c) = f.(a,f.(b,c))
    proof
      let a,b,c be Element of [.0,1.];
a2:   max (a,b) = a or max (a,b) = b by XXREAL_0:16;
a3:   max (b,c) = b or max (b,c) = c by XXREAL_0:16;
      f.(f.(a,b),c) = f.(max(a,b),c) by MaxDef
      .= max (max(a,b),c) by MaxDef,a2
      .= max (a,max(b,c)) by XXREAL_0:34
      .= f.(a,max(b,c)) by a3,MaxDef
      .= f.(a,f.(b,c)) by MaxDef;
      hence thesis;
    end;
D1: for a,b,c,d being Element of [.0,1.] st
      a <= c & b <= d holds f.(a,b) <= f.(c,d)
    proof
      let a,b,c,d be Element of [.0,1.];
      assume a <= c & b <= d; then
      max (a,b) <= max (c,d) by XXREAL_0:26; then
      max (a,b) <= f.(c,d) by MaxDef;
      hence thesis by MaxDef;
    end;
    for a being Element of [.0,1.] holds f.(a,0) = a
    proof
      let a be Element of [.0,1.];
T1:   0 in [.0,1.] by XXREAL_1:1;
      a >= 0 by XXREAL_1:1; then
      max(a,0) = a by XXREAL_0:def 10;
      hence thesis by MaxDef,T1;
    end;
    hence thesis by BINOP_1:def 2,def 3,A1,DD,D1;
  end;
end;

registration
  cluster commutative associative monotonic with-0-identity
    for BinOp of [.0,1.];
  existence
  proof
    take maxnorm;
    thus thesis;
  end;
end;

definition
  mode t-conorm is
    commutative associative monotonic with-0-identity BinOp of [.0,1.];
end;

theorem NormIs0:
  for t being commutative monotonic with-1-identity BinOp of [.0,1.] holds
    for a being Element of [.0,1.] holds
      t.(a,0) = 0
  proof
    let t be commutative monotonic with-1-identity BinOp of [.0,1.];
    let a be Element of [.0,1.];
T0: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
T3: t.(1,0) = t.(0,1) by BINOP_1:def 2 .= 0 by T0,IdDef;
    for a being Element of [.0,1.] holds t.(a,0) = 0
    proof
      let a be Element of [.0,1.];
      t.(a,0) in [.0,1.] by NormIn01; then
T4:   0 <= t.(a,0) by XXREAL_1:1;
      a <= 1 by XXREAL_1:1;
      hence thesis by T4,T0,MonDef,T3;
    end;
    hence thesis;
  end;

theorem ConormIs1:
  for t being commutative monotonic with-0-identity BinOp of [.0,1.] holds
    for a being Element of [.0,1.] holds
      t.(a,1) = 1
  proof
    let t be commutative monotonic with-0-identity BinOp of [.0,1.];
    let a be Element of [.0,1.];
T0: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1; then
T3: t.(0,1) = t.(1,0) by BINOP_1:def 2 .= 1 by T0,ZeroDef;
    for a being Element of [.0,1.] holds t.(a,1) = 1
    proof
      let a be Element of [.0,1.];
      t.(a,1) in [.0,1.] by NormIn01; then
T4:   t.(a,1) <= 1 by XXREAL_1:1;
      0 <= a by XXREAL_1:1; then
      1 <= t.(a,1) by T0,MonDef,T3;
      hence thesis by XXREAL_0:1,T4;
    end;
    hence thesis;
  end;

registration
  cluster -> with-0-annihilating
    for commutative monotonic with-1-identity BinOp of [.0,1.];
  coherence by NormIs0;
  cluster -> with-1-annihilating
    for commutative monotonic with-0-identity BinOp of [.0,1.];
  coherence by ConormIs1;
end;

begin :: Further Examples of Triangular Norms

definition
  func prodnorm -> BinOp of [.0,1.] means :ProdDef:
    for a,b being Element of [.0,1.] holds
      it.(a,b) = a * b;
  existence
  proof
    set A = [.0,1.];
    deffunc F(Element of A, Element of A) = In ($1 * $2,A);
    ex f being Function of [:A,A:], A st
    for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being BinOp of A such that
A1: for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y);
    take f;
    let a,b be Element of [.0,1.];
    f.(a,b) = F(a,b) by A1;
    hence thesis by SUBSET_1:def 8,Lemma1;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds f1.(a,b) = a * b and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = a * b;
A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1
          .= dom f2 by FUNCT_2:def 1;
    for x,y being object st
      [x,y] in dom f1 holds f1.(x,y) = f2.(x,y)
    proof
      let x,y be object;
      assume [x,y] in dom f1; then
      reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87;
      f1.(xx,yy) = xx * yy by A1
                .= f2.(xx,yy) by A2;
      hence thesis;
    end;
    hence thesis by A3,BINOP_1:20;
  end;
end;

registration
  cluster prodnorm -> commutative associative monotonic with-1-identity;
  coherence
  proof
    set f = prodnorm;
A1: for a,b being Element of [.0,1.] holds
      f.(a,b) = f.(b,a)
    proof
      let a,b be Element of [.0,1.];
      f.(a,b) = a * b by ProdDef
             .= f.(b,a) by ProdDef;
      hence thesis;
    end;
C1: for a,b,c being Element of [.0,1.] holds
      f.(f.(a,b),c) = f.(a,f.(b,c))
    proof
      let a,b,c be Element of [.0,1.];
A2:   a * b in [.0,1.] by Lemma1;
A3:   b * c in [.0,1.] by Lemma1;
      f.(f.(a,b),c) = f.(a * b,c) by ProdDef
      .= (a * b) * c by ProdDef,A2
      .= a * (b * c)
      .= f.(a,b * c) by A3,ProdDef
      .= f.(a,f.(b,c)) by ProdDef;
      hence thesis;
    end;
D1: for a,b,c,d being Element of [.0,1.] st
      a <= c & b <= d holds f.(a,b) <= f.(c,d)
    proof
      let a,b,c,d be Element of [.0,1.];
B1:   0 <= a & 0 <= b by XXREAL_1:1;
      assume a <= c & b <= d; then
      a * b <= c * d by B1,XREAL_1:66; then
      a * b <= f.(c,d) by ProdDef;
      hence thesis by ProdDef;
    end;
T1: 1 in [.0,1.] by XXREAL_1:1;
    for a being Element of [.0,1.] holds f.(a,1) = a
    proof
      let a be Element of [.0,1.];
      a * 1 = a;
      hence thesis by ProdDef,T1;
    end;
    hence thesis by BINOP_1:def 2,def 3,A1,C1,D1;
  end;
end;

definition
  func probsum_conorm -> BinOp of [.0,1.] means :ProbSumDef:
    for a,b being Element of [.0,1.] holds
      it.(a,b) = a + b - a * b;
  existence
  proof
    set A = [.0,1.];
    deffunc F(Element of A, Element of A) = In ($1 + $2 - $1 * $2,A);
    ex f being Function of [:A,A:], A st
    for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being BinOp of A such that
A1: for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y);
    take f;
    let a,b be Element of [.0,1.];
    f.(a,b) = F(a,b) by A1;
    hence thesis by SUBSET_1:def 8,abMinab01;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds f1.(a,b) = a + b - a * b and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = a + b - a * b;
A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1
          .= dom f2 by FUNCT_2:def 1;
    for x,y being object st
      [x,y] in dom f1 holds f1.(x,y) = f2.(x,y)
    proof
      let x,y be object;
      assume [x,y] in dom f1; then
      reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87;
      f1.(xx,yy) = xx + yy - xx * yy by A1
                .= f2.(xx,yy) by A2;
      hence thesis;
    end;
    hence thesis by A3,BINOP_1:20;
  end;
end;

definition
  func Lukasiewicz_norm -> BinOp of [.0,1.] means :LukNorm:
    for a,b being Element of [.0,1.] holds
      it.(a,b) = max (0, a + b - 1);
  existence
  proof
    set A = [.0,1.];
    deffunc F(Element of A, Element of A) = In (max (0, $1 + $2 - 1),A);
    ex f being Function of [:A,A:], A st
    for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being BinOp of A such that
A1: for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y);
    take f;
    let a,b be Element of [.0,1.];
    reconsider aa = a, bb = b as Element of A;
    f.(a,b) = F(aa,bb) by A1;
    hence thesis by SUBSET_1:def 8,Lemma2;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds f1.(a,b) = max (0, a + b - 1) and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = max (0, a + b - 1);
A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1
          .= dom f2 by FUNCT_2:def 1;
    for x,y being object st
      [x,y] in dom f1 holds f1.(x,y) = f2.(x,y)
    proof
      let x,y be object;
      assume [x,y] in dom f1; then
      reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87;
      f1.(xx,yy) = max (0, xx + yy - 1) by A1
                .= f2.(xx,yy) by A2;
      hence thesis;
    end;
    hence thesis by A3,BINOP_1:20;
  end;
end;

registration
  cluster Lukasiewicz_norm -> commutative associative monotonic
    with-1-identity;
  coherence
  proof
    set f = Lukasiewicz_norm;
A1: for a,b being Element of [.0,1.] holds
      f.(a,b) = f.(b,a)
    proof
      let a,b be Element of [.0,1.];
      f.(a,b) = max (0, a + b - 1) by LukNorm
             .= f.(b,a) by LukNorm;
      hence thesis;
    end;
C1: for a,b,c being Element of [.0,1.] holds
      f.(f.(a,b),c) = f.(a,f.(b,c))
    proof
      let a,b,c be Element of [.0,1.];
      set B = max(0,a + b - 1);
      set C = max(0,b + c - 1);
G1:   B in [.0,1.] by Lemma2;
G2:   C in [.0,1.] by Lemma2;
      f.(f.(a,b),c) = f.(B,c) by LukNorm
      .= max (0,B+c-1) by LukNorm,G1
      .= max (0,a+C-1) by Lemma3
      .= f.(a,C) by LukNorm,G2
      .= f.(a,f.(b,c)) by LukNorm;
      hence thesis;
    end;
D1: for a,b,c,d being Element of [.0,1.] st
      a <= c & b <= d holds f.(a,b) <= f.(c,d)
    proof
      let a,b,c,d be Element of [.0,1.];
      assume a <= c & b <= d; then
      a + b <= c + d by XREAL_1:7; then
      a + b - 1 <= c + d - 1 by XREAL_1:9; then
      max (0, a + b - 1) <= max (0, c + d - 1) by XXREAL_0:26; then
      max (0, a + b - 1) <= f.(c,d) by LukNorm;
      hence thesis by LukNorm;
    end;
    for a being Element of [.0,1.] holds f.(a,1) = a
    proof
      let a be Element of [.0,1.];
T1:   1 in [.0,1.] by XXREAL_1:1;
T2:   0 <= a by XXREAL_1:1;
      f.(a,1) = max (0,a+1-1) by LukNorm,T1
             .= a by T2,XXREAL_0:def 10;
      hence thesis;
    end;
    hence thesis by BINOP_1:def 2,def 3,A1,C1,D1;
  end;
end;

definition
  func drastic_norm -> BinOp of [.0,1.] means :Drastic2Def:
    for a,b being Element of [.0,1.] holds
      (max (a,b) = 1 implies it.(a,b) = min (a,b)) &
      (max (a,b) <> 1 implies it.(a,b) = 0);
  existence
  proof
    set C = [.0,1.];
    defpred P[set,set] means $1 = 1 or $2 = 1;
    deffunc F(Element of C,Element of C) = In(min ($1,$2),C);
    deffunc G(Element of C,Element of C) = In(0,C);
    ex f being Function of [:C,C:],C st for c be Element of C,
    d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = F(c,d)) &
    (not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then
    consider f being Function of [:C,C:],C such that
A1: for c be Element of C, d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = F(c,d)) &
    (not P [c,d] implies f. [c,d] = G(c,d));
    take f;
A0: dom f = [:C,C:] by FUNCT_2:def 1;
    let a,b be Element of C;
cc: min (a,b) = a or min (a,b) = b by XXREAL_0:15;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
    (max (a,b) = 1 implies f.(a,b) = min (a,b)) &
    (max (a,b) <> 1 implies f.(a,b) = 0)
    proof
      thus max (a,b) = 1 implies f.(a,b) = min (a,b)
      proof
        assume max (a,b) = 1; then
        a = 1 or b = 1 by XXREAL_0:16; then
        f. [a,b] = F(a,b) by A1,AA
                .= min (a,b) by SUBSET_1:def 8,cc;
        hence thesis;
      end;
      assume
B0:   max (a,b) <> 1;
      a <> 1 & b <> 1
      proof
        assume a = 1 or b = 1; then
        per cases;
        suppose
Z1:       a = 1; then
          b <= a by XXREAL_1:1;
          hence thesis by B0,XXREAL_0:def 10,Z1;
        end;
        suppose
Z1:       b = 1; then
          a <= b by XXREAL_1:1;
          hence thesis by B0,XXREAL_0:def 10,Z1;
        end;
      end; then
      f. [a,b] = G(a,b) by A1,AA
                .= 0 by XXREAL_1:1,SUBSET_1:def 8;
      hence thesis;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds
      (max (a,b) = 1 implies f1.(a,b) = min (a,b)) &
      (max (a,b) <> 1 implies f1.(a,b) = 0) and
A2: for a,b being Element of [.0,1.] holds
      (max (a,b) = 1 implies f2.(a,b) = min (a,b)) &
      (max (a,b) <> 1 implies f2.(a,b) = 0);
    for a,b being set st a in [.0,1.] & b in [.0,1.] holds
      f1.(a,b) = f2.(a,b)
    proof
      let a,b be set;
      assume a in [.0,1.] & b in [.0,1.]; then
      reconsider aa = a, bb = b as Element of [.0,1.];
      per cases;
      suppose
B0:     max (aa,bb) = 1; then
        f1.(aa,bb) = min (aa,bb) by A1 .= f2.(aa,bb) by A2,B0;
        hence thesis;
      end;
      suppose
B1:     max (aa,bb) <> 1; then
        f1.(aa,bb) = 0 by A1 .= f2.(aa,bb) by A2,B1;
        hence thesis;
      end;
    end;
    hence thesis by BINOP_1:def 21;
  end;
end;

theorem DrasticDef:
  for a,b being Element of [.0,1.] holds
    (a = 1 implies drastic_norm.(a,b) = b) &
    (b = 1 implies drastic_norm.(a,b) = a) &
    (a <> 1 & b <> 1 implies drastic_norm.(a,b) = 0)
  proof
    let a,b be Element of [.0,1.];
A1: b <= 1 & a <= 1 by XXREAL_1:1;
    thus a = 1 implies drastic_norm.(a,b) = b
    proof
      assume
B1:   a = 1; then
      max (a,b) = 1 by A1,XXREAL_0:def 10; then
      drastic_norm.(a,b) = min (a,b) by Drastic2Def
                        .= b by XXREAL_0:def 9,A1,B1;
      hence thesis;
    end;
    thus b = 1 implies drastic_norm.(a,b) = a
    proof
      assume
B1:   b = 1; then
      max (a,b) = 1 by A1,XXREAL_0:def 10; then
      drastic_norm.(a,b) = min (a,b) by Drastic2Def
                        .= a by XXREAL_0:def 9,A1,B1;
      hence thesis;
    end;
    assume a <> 1 & b <> 1; then
    max (a,b) <> 1 by XXREAL_0:16;
    hence thesis by Drastic2Def;
  end;

registration
  cluster drastic_norm -> commutative associative with-1-identity
    monotonic;
  coherence
  proof
    set f = drastic_norm;
FF: for a,b being Element of [.0,1.] holds
      f.(a,b) = f.(b,a)
    proof
      let a,b be Element of [.0,1.];
      per cases;
      suppose
A1:     a = 1; then
        f.(a,b) = b by DrasticDef;
        hence thesis by A1,DrasticDef;
      end;
      suppose
A1:     b = 1; then
        f.(b,a) = a by DrasticDef;
        hence thesis by A1,DrasticDef;
      end;
      suppose a <> 1 & b <> 1; then
        f.(a,b) = 0 & f.(b,a) = 0 by DrasticDef;
        hence thesis;
      end;
    end;
TT: for a being Element of [.0,1.] holds f.(a,1) = a
    proof
      let a be Element of [.0,1.];
      1 in [.0,1.] by XXREAL_1:1;
      hence thesis by DrasticDef;
    end;
D1: for a,b,c,d being Element of [.0,1.] st
      a <= c & b <= d holds f.(a,b) <= f.(c,d)
    proof
      let a,b,c,d be Element of [.0,1.];
B2:   f.(c,d) >= 0 by XXREAL_1:1;
      assume
S1:   a <= c & b <= d;
      per cases;
      suppose
S0:     a = 1;
        c <= 1 by XXREAL_1:1; then
        f.(c,d) = d by DrasticDef,S0,S1,XXREAL_0:1;
        hence thesis by S1,DrasticDef,S0;
      end;
      suppose
S0:     b = 1;
        d <= 1 by XXREAL_1:1; then
        f.(c,d) = c by DrasticDef,S0,S1,XXREAL_0:1;
        hence thesis by S1,DrasticDef,S0;
      end;
      suppose b <> 1 & a <> 1;
        hence thesis by B2,DrasticDef;
      end;
    end;
H1: 0 in [.0,1.] by XXREAL_1:1;
BU: for a being Element of [.0,1.] holds f.(a,0) = 0
    proof
      let a be Element of [.0,1.];
H2:   0 <= a by XXREAL_1:1;
      per cases;
      suppose max (a,0) = 1; then
        f.(a,0) = min (a,0) by Drastic2Def,H1 .= 0 by H2,XXREAL_0:def 9;
        hence thesis;
      end;
      suppose max (a,0) <> 1;
        hence thesis by Drastic2Def,H1;
      end;
    end;
    for a,b,c being Element of [.0,1.] holds
      f.(a,f.(b,c)) = f.(f.(a,b),c)
    proof
      let a,b,c be Element of [.0,1.];
Z4:   min(a,b) in [.0,1.] by MinIn01;
EE:   min(b,c) in [.0,1.] by MinIn01;
      per cases;
      suppose
Z1:     max (a,b) = 1 & max (b,c) = 1; then
K1:     a = 1 or b = 1 by XXREAL_0:16;
        max (a,c) in [.0,1.] by MaxIn01; then
U2:     max (a,c) <= 1 by XXREAL_1:1;
Z2:     f.(b,c) = min (b,c) by Drastic2Def,Z1;
UU:     max (a,min(b,c)) = min (max(a,b),max(a,c)) by XXREAL_0:39
          .= max (a,c) by U2,XXREAL_0:def 9,Z1;
        per cases;
        suppose
HU:       max (a,c) = 1;
U2:       max (min(a,b),c) = min (max(a,c),max(b,c)) by XXREAL_0:39
              .= 1 by Z1,HU;
          f.(a,f.(b,c)) = f.(a,min(b,c)) by Drastic2Def,Z1
                .= min (a,min(b,c)) by Drastic2Def,HU,UU,EE
                .= min (min(a,b),c) by XXREAL_0:33
                .= f.(min(a,b),c) by U2,Drastic2Def,Z4
                .= f.(f.(a,b),c) by Drastic2Def,Z1;
          hence thesis;
        end;
        suppose
HU:       max (a,c) <> 1; then
          a <= b by XXREAL_1:1,K1,DiffMax; then
K3:       min (a,b) = a by XXREAL_0:def 9;
U1:       f.(a,b) = min (a,b) by Drastic2Def,Z1;
          f.(a,f.(b,c)) = 0 by Drastic2Def,HU,UU,Z2
                .= f.(f.(a,b),c) by U1,K3,HU,Drastic2Def;
          hence thesis;
        end;
      end;
      suppose
Z1:     max (a,b) = 1 & max (b,c) <> 1; then
z1:     a = 1 or b = 1 by XXREAL_0:16;
        max (b,c) in [.0,1.] by MaxIn01; then
W1:     max (b,c) <= 1 by XXREAL_1:1;
za:     b <> 1
        proof
          assume b = 1; then
          max (b,c) >= 1 by XXREAL_0:25;
          hence thesis by Z1,XXREAL_0:1,W1;
        end;
        c <= 1 by XXREAL_1:1; then
z3:     max (a,c) = 1 by z1,za,XXREAL_0:def 10;
qq:     max (min(a,b),c) = min (max(a,c),max(b,c)) by XXREAL_0:39
          .= max (b,c) by W1,z3,XXREAL_0:def 9;
        f.(b,c) = 0 by Drastic2Def,Z1; then
        f.(a,f.(b,c)) = 0 by BU
                     .= f.(min(a,b),c) by qq,Z1,Drastic2Def,Z4
                     .= f.(f.(a,b),c) by Drastic2Def,Z1;
        hence thesis;
      end;
      suppose
Z1:     max (a,b) <> 1 & max (b,c) = 1; then
z1:     c = 1 or b = 1 by XXREAL_0:16;
        max (a,b) in [.0,1.] by MaxIn01; then
w1:     max (a,b) <= 1 by XXREAL_1:1;
zz:     b <> 1
        proof
          assume b = 1; then
          max (a,b) >= 1 by XXREAL_0:25;
          hence thesis by Z1,w1,XXREAL_0:1;
        end;
Z2:     f.(b,c) = min (b,c) by Drastic2Def,Z1;
Y1:     f.(a,b) = 0 by Drastic2Def,Z1;
        b <= c by XXREAL_1:1,zz,z1; then
        f.(b,c) = b by Z2,XXREAL_0:def 9; then
        f.(a,f.(b,c)) = 0 by Drastic2Def,Z1
                     .= f.(c,0) by BU
                     .= f.(f.(a,b),c) by Y1,FF;
        hence thesis;
      end;
      suppose
Z1:     max (a,b) <> 1 & max (b,c) <> 1; then
Z2:     f.(b,c) = 0 by Drastic2Def;
Z3:     f.(a,b) = 0 by Drastic2Def,Z1;
        f.(a,f.(b,c)) = 0 by BU,Z2
              .= f.(c,0) by BU
              .= f.(f.(a,b),c) by Z3,FF;
        hence thesis;
      end;
    end;
    hence thesis by FF,TT,D1,BINOP_1:def 3,def 2;
  end;
end;

definition
  func nilmin_norm -> BinOp of [.0,1.] means :NilminDef:
    for a,b being Element of [.0,1.] holds
      (a + b > 1 implies it.(a,b) = min (a,b)) &
      (a + b <= 1 implies it.(a,b) = 0);
  existence
  proof
    set C = [.0,1.];
    defpred P[Real,Real] means $1 + $2 > 1;
    deffunc F(Element of C,Element of C) = In(min ($1,$2),C);
    deffunc G(Element of C,Element of C) = In(0,C);
    ex f being Function of [:C,C:],C st for c be Element of C,
    d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = F(c,d)) &
    (not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then
    consider f being Function of [:C,C:],C such that
A1: for c be Element of C, d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = F(c,d)) &
    (not P [c,d] implies f. [c,d] = G(c,d));
    take f;
A0: dom f = [:C,C:] by FUNCT_2:def 1;
    let a,b be Element of C;
cc: min (a,b) = a or min (a,b) = b by XXREAL_0:15;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
    (a + b > 1 implies f.(a,b) = min (a,b)) &
    (a + b <= 1 implies f.(a,b) = 0)
    proof
      thus a + b > 1 implies f.(a,b) = min (a,b)
      proof
        assume a + b > 1; then
        f. [a,b] = F(a,b) by A1,AA
                .= min (a,b) by SUBSET_1:def 8,cc;
        hence thesis;
      end;
      assume a + b <= 1; then
      f. [a,b] = G(a,b) by A1,AA
                .= 0 by XXREAL_1:1,SUBSET_1:def 8;
      hence thesis;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds
      (a + b > 1 implies f1.(a,b) = min (a,b)) &
      (a + b <= 1 implies f1.(a,b) = 0) and
A2: for a,b being Element of [.0,1.] holds
      (a + b > 1 implies f2.(a,b) = min (a,b)) &
      (a + b <=  1 implies f2.(a,b) = 0);
    for a,b being set st a in [.0,1.] & b in [.0,1.] holds
      f1.(a,b) = f2.(a,b)
    proof
      let a,b be set;
      assume a in [.0,1.] & b in [.0,1.]; then
      reconsider aa = a, bb = b as Element of [.0,1.];
      per cases;
      suppose
B0:     aa + bb > 1; then
        f1.(aa,bb) = min (aa,bb) by A1 .= f2.(aa,bb) by A2,B0;
        hence thesis;
      end;
      suppose
B1:     aa + bb <= 1; then
        f1.(aa,bb) = 0 by A1 .= f2.(aa,bb) by A2,B1;
        hence thesis;
      end;
    end;
    hence thesis by BINOP_1:def 21;
  end;
end;

registration
  cluster nilmin_norm -> commutative associative with-1-identity
    monotonic;
  coherence
  proof
    set f = nilmin_norm;
FF: for a,b being Element of [.0,1.] holds
      f.(a,b) = f.(b,a)
    proof
      let a,b be Element of [.0,1.];
      per cases;
      suppose
A1:     a + b > 1;
        hence f.(a,b) = min (a,b) by NilminDef
               .= f.(b,a) by NilminDef,A1;
      end;
      suppose a + b <= 1; then
        f.(a,b) = 0 & f.(b,a) = 0 by NilminDef;
        hence thesis;
      end;
    end;
U1: 1 in [.0,1.] by XXREAL_1:1;
TT: for a being Element of [.0,1.] holds f.(a,1) = a
    proof
      let a be Element of [.0,1.];
U4:   0 <= a <= 1 by XXREAL_1:1;
      per cases;
      suppose a + 1 > 1; then
        f.(a,1) = min (a,1) by NilminDef,U1
            .= a by U4,XXREAL_0:def 9;
        hence thesis;
      end;
      suppose
U2:     a + 1 <= 1; then
        a <= 1 - 1 by XREAL_1:19; then
        a = 0 by XXREAL_1:1;
        hence thesis by NilminDef,U2,U1;
      end;
    end;
D1: for a,b,c,d being Element of [.0,1.] st
      a <= c & b <= d holds f.(a,b) <= f.(c,d)
    proof
      let a,b,c,d be Element of [.0,1.];
      assume
S1:   a <= c & b <= d;
      per cases;
      suppose
S0:     a + b > 1; then
Sa:     f.(a,b) = min (a,b) by NilminDef;
        a + b <= c + d by S1,XREAL_1:7; then
        c + d > 1 by S0,XXREAL_0:2; then
        f.(c,d) = min (c,d) by NilminDef;
        hence thesis by S1,Sa,XXREAL_0:18;
      end;
      suppose a + b <= 1; then
        f.(a,b) = 0 by NilminDef;
        hence thesis by XXREAL_1:1;
      end;
    end;
H1: 0 in [.0,1.] by XXREAL_1:1;
BU: for a being Element of [.0,1.] holds f.(a,0) = 0
    proof
      let a be Element of [.0,1.];
      per cases;
      suppose a + 0 > 1;
        hence thesis by XXREAL_1:1;
      end;
      suppose a + 0 <= 1;
        hence thesis by NilminDef,H1;
      end;
    end;
    for a,b,c being Element of [.0,1.] holds
      f.(a,f.(b,c)) = f.(f.(a,b),c)
    proof
      let a,b,c be Element of [.0,1.];
EE:   min (b,c) in [.0,1.] by MinIn01;
U3:   min (a,b) in [.0,1.] by MinIn01;
      per cases;
      suppose
Z1:     a + b > 1 & b + c > 1; then
Z2:     f.(b,c) = min (b,c) by NilminDef;
        per cases;
        suppose
HU:       a + c > 1; then
W6:       a + min (b,c) > 1 by Z1,XXREAL_0:15;
W7:       c + min(a,b) > 1 by HU,Z1,XXREAL_0:15;
          f.(a,f.(b,c)) = f.(a,min(b,c)) by Z1,NilminDef
                .= min (a,min(b,c)) by NilminDef,EE,W6
                .= min (min(a,b),c) by XXREAL_0:33
                .= f.(min(a,b),c) by NilminDef,U3,W7
                .= f.(f.(a,b),c) by NilminDef,Z1;
          hence thesis;
        end;
        suppose
HU:       a + c <= 1;
          a + min (b,c) <= a + c by XREAL_1:6,XXREAL_0:17; then
W1:       a + min (b,c) <= 1 by HU,XXREAL_0:2;
          c + min (a,b) <= a + c by XREAL_1:6,XXREAL_0:17; then
W2:       c + min (a,b) <= 1 by HU,XXREAL_0:2;
U1:       f.(a,b) = min (a,b) by NilminDef,Z1;
          f.(a,f.(b,c)) = 0 by W1,NilminDef,Z2
                .= f.(f.(a,b),c) by U1,W2,NilminDef;
          hence thesis;
        end;
      end;
      suppose
Z1:     a + b > 1 & b + c <= 1; then
Z2:     f.(a,b) = min (a,b) by NilminDef;
        per cases;
        suppose
          a + c <= 1; then
G2:       min (a,b) + c <= 1 by Z1,XXREAL_0:15;
          f.(b,c) = 0 by NilminDef,Z1; then
          f.(a,f.(b,c)) = 0 by BU
                     .= f.(f.(a,b),c) by Z2,NilminDef,G2;
          hence thesis;
        end;
        suppose
hh:       a + c > 1;
g4:       min (a,b) + c = min (a+c, b+c) by FUZZY_2:42
            .= b + c by XXREAL_0:def 9,hh,XXREAL_0:2,Z1;
          f.(b,c) = 0 by NilminDef,Z1;
          hence thesis by Z2,g4,BU;
        end;
      end;
      suppose
Z1:     a + b <= 1 & b + c > 1; then
Z2:     f.(b,c) = min (b,c) by NilminDef;
ZZ:     f.(a,b) = 0 by NilminDef,Z1;
        per cases;
        suppose
          a + c <= 1; then
G2:       min (b,c) + a <= 1 by Z1,XXREAL_0:15;
          f.(f.(a,b),c) = f.(0,c) by Z1,NilminDef
                     .= f.(c,0) by FF,H1
                     .= 0 by BU
                     .= f.(a,f.(b,c)) by Z2,NilminDef,G2;
          hence thesis;
        end;
        suppose
g5:       a + c > 1;
g4:       min (c,b) + a = min (c+a, b+a) by FUZZY_2:42
            .= a + b by XXREAL_0:def 9,g5,XXREAL_0:2,Z1;
          f.(a,f.(b,c)) = f.(a,min(b,c)) by NilminDef,Z1
                     .= 0 by NilminDef,g4,Z1
                     .= f.(c,0) by BU
                     .= f.(f.(a,b),c) by ZZ,FF;
          hence thesis;
        end;
      end;
      suppose
Z1:     a + b <= 1 & b + c <= 1; then
Z2:     f.(b,c) = 0 by NilminDef;
Z3:     f.(a,b) = 0 by NilminDef,Z1;
        f.(a,f.(b,c)) = 0 by BU,Z2
              .= f.(c,0) by BU
              .= f.(f.(a,b),c) by Z3,FF;
        hence thesis;
      end;
    end;
    hence thesis by FF,TT,D1,BINOP_1:def 3,def 2;
  end;
end;

definition
  func Hamacher_norm -> BinOp of [.0,1.] means :HamDef:
    for a,b being Element of [.0,1.] holds
      it.(a,b) = (a * b) / (a + b - a * b);
  existence
  proof
    set A = [.0,1.];
    deffunc F(Element of A,Element of A) =
      In(($1 * $2) / ($1 + $2 - $1 * $2),A);
    ex f being Function of [:A,A:], A st
    for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being BinOp of A such that
A1: for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y);
    reconsider ff = f as BinOp of [.0,1.];
    take ff;
    let a,b be Element of [.0,1.];
    reconsider aa = a, bb = b as Element of A;
    ff.(a,b) = F(aa,bb) by A1;
    hence thesis by SUBSET_1:def 8,HamIn01;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds
      f1.(a,b) = (a * b) / (a + b - a * b) and
A2: for a,b being Element of [.0,1.] holds
      f2.(a,b) = (a * b) / (a + b - a * b);
    for a,b being set st a in [.0,1.] & b in [.0,1.] holds
      f1.(a,b) = f2.(a,b)
    proof
      let a,b be set;
      assume a in [.0,1.] & b in [.0,1.]; then
      reconsider aa = a, bb = b as Element of [.0,1.];
      f1.(aa,bb) = (aa * bb) / (aa + bb - aa * bb) by A1
          .= f2.(aa,bb) by A2;
        hence thesis;
    end;
    hence thesis by BINOP_1:def 21;
  end;
end;

registration
  cluster Hamacher_norm -> commutative associative with-1-identity
    monotonic;
  coherence
  proof
    set f = Hamacher_norm;
FF: for a,b being Element of [.0,1.] holds
      f.(a,b) = f.(b,a)
    proof
      let a,b be Element of [.0,1.];
      f.(a,b) = (a * b) / (a + b - a * b) by HamDef
          .= f.(b,a) by HamDef;
      hence thesis;
    end;
TT: for a being Element of [.0,1.] holds f.(a,1) = a
    proof
      let a be Element of [.0,1.];
      1 in [.0,1.] by XXREAL_1:1; then
      f.(a,1) = (a * 1) / (a + 1 - a * 1) by HamDef;
      hence thesis;
    end;
D1: for a,b,c,d being Element of [.0,1.] st
      a <= c & b <= d holds f.(a,b) <= f.(c,d)
    proof
      let a,b,c,d be Element of [.0,1.];
JJ:   0 <= a & 0 <= b & 0 <= c & 0 <= d by XXREAL_1:1;
B2:   f.(c,d) >= 0 by XXREAL_1:1;
      assume
S1:   a <= c & b <= d;
D1:   f.(a,b) = (a * b) / (a + b - a * b) by HamDef;
D2:   f.(c,d) = (c * d) / (c + d - c * d) by HamDef;
d2:   f.(a,d) = (a * d) / (a + d - a * d) by HamDef;
      set A = a + b - a * b, B = c + d - c * d;
      per cases;
      suppose A = 0;
        hence thesis by B2,XCMPLX_1:49,D1;
      end;
      suppose
DD:     B = 0;
        reconsider ad = a + d - a * d, ab = a + b - a * b
          as Element of [.0,1.] by abMinab01;
        reconsider B as Element of [.0,1.] by abMinab01;
        1 - a in [.0,1.] by OpIn01; then
        1 - a >= 0 by XXREAL_1:1; then
        b * (1 - a) <= d * (1 - a) by S1,XREAL_1:64; then
w0:     b * (1 - a) + a <= d * (1 - a) + a by XREAL_1:6;
        1 - d in [.0,1.] by OpIn01; then
        1 - d >= 0 by XXREAL_1:1; then
        a * (1 - d) <= c * (1 - d) by S1,XREAL_1:64; then
WC:     a * (1 - d) + d <= c * (1 - d) + d by XREAL_1:6; then
de:     ab = 0 by XXREAL_1:1,DD,w0;
dg:     ad >= 0 by XXREAL_1:1;
hf:     ad = 0 by DD,WC,XXREAL_1:1;
df:     f.(a,d) - f.(a,b) = (a * d) / ad - 0 by XCMPLX_1:49,de,D1,d2
          .= (a * d) / ad;
WA:     f.(a,b) <= f.(a,d) - 0 by XREAL_1:11,df,dg,JJ;
        f.(c,d) - f.(a,d) = (c * d) / B - 0 by XCMPLX_1:49,hf,d2,D2
          .= 0 by XCMPLX_1:49,DD;
        hence thesis by WA;
      end;
      suppose A <> 0 & B <> 0; then
D8:     f.(c,d) - f.(a,b) =
           (A * (c * d) - B * (a * b)) / (A * B) by XCMPLX_1:130,D1,D2
           .= ((a * c) * (d - b) + (b * d) * (c - a)) / (A * B);
        A in [.0,1.] & B in [.0,1.] by abMinab01; then
d6:     A >= 0 & B >= 0 by XXREAL_1:1;
        b <= d - 0 by S1; then
D3:     d - b >= 0 by XREAL_1:11;
        a <= c - 0 by S1; then
        c - a >= 0 by XREAL_1:11; then
        f.(c,d) - f.(a,b) + f.(a,b) >= 0 + f.(a,b) by XREAL_1:6,d6,D8,JJ,D3;
        hence thesis;
      end;
    end;
H1: 0 in [.0,1.] by XXREAL_1:1;
BU: for a being Element of [.0,1.] holds f.(a,0) = 0
    proof
      let a be Element of [.0,1.];
      f.(a,0) = (a * 0) / (a + 0 - a * 0) by HamDef,H1;
      hence thesis;
    end;
    for a,b,c being Element of [.0,1.] holds
      f.(a,f.(b,c)) = f.(f.(a,b),c)
    proof
      let a,b,c be Element of [.0,1.];
J1:   f.(a,b) = (a * b) / (a + b - a * b) by HamDef;
J2:   f.(b,c) = (b * c) / (b + c - b * c) by HamDef;
      reconsider bc = (b * c) / (b + c - b * c) as Element of [.0,1.]
        by HamIn01;
      set ab = (a * b) / (a + b - a * b);
      set bb = b + c - b * c;
      set AB = a + b - a * b;
      per cases;
      suppose
Z1:     a <> 0 & b <> 0 & c <> 0; then
P1:     a * b <> 0 by XCMPLX_1:6;
j3:     ab in [.0,1.] by HamIn01;
        per cases;
        suppose
          ab = 0; then
          AB = 0 by XCMPLX_1:50,P1;
          hence thesis by Z1,Lemacik;
        end;
        suppose
T1:       bc = 0;
          b * c <> 0 by Z1,XCMPLX_1:6; then
          b + c - b * c = 0 by T1,XCMPLX_1:50;
          hence thesis by Z1,Lemacik;
        end;
        suppose ab <> 0 & bc <> 0; then
f1:       AB <> 0 & bb <> 0 by XCMPLX_1:49;
WA:      (a * bc) * (ab + c - ab * c)
           = ((a * (b * c)) / bb) * (c + (((a * b) / AB) - ((a * b) / AB) * c))
               by XCMPLX_1:74
          .= ((a * (b * c)) / bb) * (c * AB / AB + ((a * b) / AB) * (1 - c))
                by XCMPLX_1:89,f1
          .= ((a * (b * c)) / bb) * (c * AB / AB + (((a * b) * (1-c)) / AB))
                by XCMPLX_1:74
          .= ((a * (b * c)) / bb) * ((c * AB + ((a * b) * (1-c))) / AB)
                by XCMPLX_1:62
          .= ((a * (b * c)) * ((c * AB + ((a * b) * (1-c))))) / (AB * bb)
                by XCMPLX_1:76
          .= ((a*b*c)/AB) * (((a * bb) + ((b*c)*(1-a)))/bb) by XCMPLX_1:76
          .= ((a*b*c)/AB) * (a * bb / bb+ (((b*c)*(1-a))/bb)) by XCMPLX_1:62
          .= ((a*b*c)/AB) * (a * bb / bb + ((b*c)/bb) * (1 - a)) by XCMPLX_1:74
          .= (((a*b)/AB) * c) * (a * bb / bb + ((b*c)/bb) * (1 - a))
            by XCMPLX_1:74
          .= (((a*b)/AB) * c) * (a + ((b*c)/bb) * (1 - a)) by XCMPLX_1:89,f1
          .= (ab * c) * (a + bc - a * bc);
          per cases;
          suppose that
  f2:       a + bc - a * bc <> 0 and
f3:         ab + c - ab * c <> 0;
            f.(a,f.(b,c)) = (a * bc) / (a + bc - a * bc) by HamDef,J2
                .= (ab * c) / (ab + c - ab * c) by WA,XCMPLX_1:94,f2,f3
                .= f.(f.(a,b),c) by J1,HamDef;
            hence thesis;
          end;
          suppose
            a + bc - a * bc = 0;
            hence thesis by Z1,Lemacik;
          end;
          suppose
            ab + c - ab * c = 0;
            hence thesis by Z1,Lemacik,j3;
          end;
        end;
      end;
      suppose
Z1:     a <> 0 & b <> 0 & c = 0; then
        f.(a,f.(b,c)) = f.(a,0) by BU
                .= 0 by BU
                .= f.(f.(a,b),c) by BU,Z1;
        hence thesis;
      end;
      suppose
Z1:     a = 0 & b <> 0;
        f.(a,f.(b,c)) = f.(f.(b,c),a) by FF
                     .= 0 by BU,Z1
                     .= f.(c,0) by BU
                     .= f.(0,c) by FF,H1
                     .= f.(f.(b,a),c) by BU,Z1
                     .= f.(f.(a,b),c) by FF;
        hence thesis;
      end;
      suppose
Z1:     a <> 0 & b = 0; then
z1:     f.(a,b) = 0 by BU;
        f.(b,c) = f.(c,b) by FF .= 0 by Z1,BU; then
        f.(a,f.(b,c)) = 0 by BU
                     .= f.(c,0) by BU
                     .= f.(f.(a,b),c) by FF,z1;
        hence thesis;
      end;
      suppose
Z1:     a = 0 & b = 0; then
Z2:     f.(a,b) = (0 * 0) / (0 + 0 - 0 * 0) by HamDef
           .= 0;
        f.(b,c) = (b * c) / (b + c - b * c) by HamDef;
        hence thesis by Z2,Z1;
      end;
    end;
    hence thesis by FF,TT,D1,BINOP_1:def 3,def 2;
  end;
end;

begin :: Basic Triangular Conorms

definition
  func drastic_conorm -> BinOp of [.0,1.] means :Drastic2CDef:
    for a,b being Element of [.0,1.] holds
      (min (a,b) = 0 implies it.(a,b) = max (a,b)) &
      (min (a,b) <> 0 implies it.(a,b) = 1);
  existence
  proof
    set C = [.0,1.];
    defpred P[set,set] means $1 = 0 or $2 = 0;
    deffunc F(Element of C,Element of C) = In(max ($1,$2),C);
    deffunc G(Element of C,Element of C) = In(1,C);
    ex f being Function of [:C,C:],C st for c be Element of C,
    d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = F(c,d)) &
    (not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then
    consider f being Function of [:C,C:],C such that
A1: for c be Element of C, d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = F(c,d)) &
    (not P [c,d] implies f. [c,d] = G(c,d));
    take f;
A0: dom f = [:C,C:] by FUNCT_2:def 1;
    let a,b be Element of C;
cc: max (a,b) = a or max (a,b) = b by XXREAL_0:16;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
    (min (a,b) = 0 implies f.(a,b) = max (a,b)) &
    (min (a,b) <> 0 implies f.(a,b) = 1)
    proof
      thus min (a,b) = 0 implies f.(a,b) = max (a,b)
      proof
        assume min (a,b) = 0; then
        a = 0 or b = 0 by XXREAL_0:15; then
        f. [a,b] = F(a,b) by A1,AA
                .= max (a,b) by SUBSET_1:def 8,cc;
        hence thesis;
      end;
      assume
B0:   min (a,b) <> 0;
      a <> 0 & b <> 0
      proof
        assume a = 0 or b = 0; then
        per cases;
        suppose
Z1:       a = 0; then
          b >= a by XXREAL_1:1;
          hence thesis by B0,XXREAL_0:def 9,Z1;
        end;
        suppose
Z1:       b = 0; then
          a >= b by XXREAL_1:1;
          hence thesis by B0,XXREAL_0:def 9,Z1;
        end;
      end; then
      f. [a,b] = G(a,b) by A1,AA
              .= 1 by XXREAL_1:1,SUBSET_1:def 8;
      hence thesis;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds
      (min (a,b) = 0 implies f1.(a,b) = max (a,b)) &
      (min (a,b) <> 0 implies f1.(a,b) = 1) and
A2: for a,b being Element of [.0,1.] holds
      (min (a,b) = 0 implies f2.(a,b) = max (a,b)) &
      (min (a,b) <> 0 implies f2.(a,b) = 1);
    for a,b being set st a in [.0,1.] & b in [.0,1.] holds
      f1.(a,b) = f2.(a,b)
    proof
      let a,b be set;
      assume a in [.0,1.] & b in [.0,1.]; then
      reconsider aa = a, bb = b as Element of [.0,1.];
      per cases;
      suppose
B0:     min (aa,bb) = 0; then
        f1.(aa,bb) = max (aa,bb) by A1 .= f2.(aa,bb) by A2,B0;
        hence thesis;
      end;
      suppose
B1:     min (aa,bb) <> 0; then
        f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B1;
        hence thesis;
      end;
    end;
    hence thesis by BINOP_1:def 21;
  end;
end;

begin :: Translating between Triangular Norms and Conorms

definition
  let t be BinOp of [.0,1.];
  func conorm t -> BinOp of [.0,1.] means :CoDef:
    for a,b being Element of [.0,1.] holds
      it.(a,b) = 1 - t.(1 - a,1 - b);
  existence
  proof
    reconsider A = [.0,1.] as non empty real-membered set;
    deffunc F(Element of A, Element of A) = In (1- t.(1-$1,1-$2),A);
    ex f being Function of [:A,A:], A st
    for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being BinOp of A such that
A1: for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y);
    reconsider ff = f as BinOp of [.0,1.];
    take ff;
    let a,b be Element of [.0,1.];
    reconsider aa = a, bb = b as Element of A;
    ff.(a,b) = F(aa,bb) by A1;
    hence thesis by SUBSET_1:def 8,CoIn01;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds f1.(a,b) = 1-t.(1-a,1-b) and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = 1-t.(1-a,1-b);
A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1
          .= dom f2 by FUNCT_2:def 1;
    for x,y being object st
      [x,y] in dom f1 holds f1.(x,y) = f2.(x,y)
    proof
      let x,y be object;
      assume [x,y] in dom f1; then
      reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87;
      f1.(xx,yy) = 1-t.(1-xx,1-yy) by A1
                .= f2.(xx,yy) by A2;
      hence thesis;
    end;
    hence thesis by A3,BINOP_1:20;
  end;
end;

registration let t be t-norm;
  cluster conorm t -> monotonic commutative associative with-0-identity;
  coherence
  proof
    set f = conorm t;
A1: for a,b being Element of [.0,1.] holds
      f.(a,b) = f.(b,a)
    proof
      let a,b be Element of [.0,1.];
A2:   1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01;
      f.(a,b) = 1-t.(1-a,1-b) by CoDef
             .= 1-t.(1-b,1-a) by A2,BINOP_1:def 2
             .= f.(b,a) by CoDef;
      hence thesis;
    end;
C1: for a,b,c being Element of [.0,1.] holds
      f.(f.(a,b),c) = f.(a,f.(b,c))
    proof
      let a,b,c be Element of [.0,1.];
A2:   1-a in [.0,1.] & 1-b in [.0,1.] & 1-c in [.0,1.] by OpIn01;
      set A = 1-t.(1-a,1-b);
H1:   A in [.0,1.] by CoIn01;
      set C = 1-t.(1-b,1-c);
H2:   C in [.0,1.] by CoIn01;
      f.(f.(a,b),c) = f.(1-t.(1-a,1-b),c) by CoDef
      .= 1-t.(1-A,1-c) by CoDef,H1
      .= 1-t.(1-a,1-C) by BINOP_1:def 3,A2
      .= f.(a,C) by CoDef,H2
      .= f.(a,f.(b,c)) by CoDef;
      hence thesis;
    end;
D1: for a,b,c,d being Element of [.0,1.] st
      a <= c & b <= d holds f.(a,b) <= f.(c,d)
    proof
      let a,b,c,d be Element of [.0,1.];
A2:   1-a in [.0,1.] & 1-b in [.0,1.] & 1-c in [.0,1.] & 1-d in [.0,1.]
        by OpIn01;
      assume a <= c & b <= d; then
      1 - c <= 1 - a & 1 - d <= 1 - b by XREAL_1:10; then
      t.(1-a,1-b) >= t.(1-c,1-d) by A2,MonDef; then
      1-t.(1-a,1-b) <= 1-t.(1-c,1-d) by XREAL_1:10; then
      f.(a,b) <= 1-t.(1-c,1-d) by CoDef;
      hence thesis by CoDef;
    end;
    for a being Element of [.0,1.] holds f.(a,0) = a
    proof
      let a be Element of [.0,1.];
T1:   0 in [.0,1.] by XXREAL_1:1;
      1-a in [.0,1.] by OpIn01; then
      t.(1-a,1) = 1 - a by IdDef; then
      1-t.(1-a,1-0) = a;
      hence thesis by CoDef,T1;
    end;
    hence thesis by A1,BINOP_1:def 2,def 3,D1,C1;
  end;
end;

theorem
  maxnorm = conorm minnorm
  proof
    for a,b being Element of [.0,1.] holds
      maxnorm.(a,b) = 1 - minnorm.(1 - a, 1 - b)
    proof
      let a,b be Element of [.0,1.];
A1:   1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01;
      set e1 = -1;
A2:   - max(e1 * -a, e1 * -b) = - (e1 * min (-a,-b)) by MES57
         .= min (-a,-b);
A3:   min (1 +- a, 1 +- b) = 1 + min (-a, -b) by FUZZY_2:42
           .= 1 - max(a, b) by A2;
      maxnorm.(a,b) = 1 - min(1 - a, 1 - b) by A3,MaxDef
       .= 1 - minnorm.(1 - a, 1 - b) by A1,MinDef;
      hence thesis;
    end;
    hence thesis by CoDef;
  end;

theorem
  for t being BinOp of [.0,1.] holds
    conorm conorm t = t
  proof
    let t be BinOp of [.0,1.];
    set tt = conorm conorm t;
    for a,b being Element of [.0,1.] holds
      t.(a,b) = tt.(a,b)
    proof
      let a, b be Element of [.0,1.];
A1:   1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01;
      tt.(a,b) = 1 - (conorm t).(1-a,1-b) by CoDef
         .= 1 - (1 - t.(1-(1-a),1-(1-b))) by CoDef,A1;
      hence thesis;
    end;
    hence thesis by BINOP_1:2;
  end;

:::theorem ::: obvious
:::  for t being t-norm holds conorm t is t-conorm;

begin :: The Ordering of Triangular Norms (and Conorms)

definition let f1, f2 be BinOp of [.0,1.];
  pred f1 <= f2 means
    for a,b being Element of [.0,1.] holds
      f1.(a,b) <= f2.(a,b);
end;

theorem
  for t being t-norm holds
    drastic_norm <= t
  proof
    let t be t-norm;
    set f1 = drastic_norm;
    for a,b being Element of [.0,1.] holds
      f1.(a,b) <= t.(a,b)
    proof
      let a,b be Element of [.0,1.];
      per cases;
      suppose
A2:     a = 1;
        reconsider aa = 1, bb = b as Element of [.0,1.] by XXREAL_1:1;
        t.(aa,bb) = t.(bb,aa) by BINOP_1:def 2
                 .= b by IdDef;
        hence thesis by DrasticDef,A2;
      end;
      suppose
A2:     b = 1;
        reconsider aa = a, bb = 1 as Element of [.0,1.] by XXREAL_1:1;
        f1.(aa,bb) = aa by DrasticDef;
        hence thesis by A2,IdDef;
      end;
      suppose
A2:     a <> 1 & b <> 1;
        reconsider aa = a, bb = b as Element of [.0,1.];
        f1.(aa,bb) = 0 by DrasticDef,A2;
        hence thesis by XXREAL_1:1;
      end;
    end;
    hence thesis;
  end;

theorem
  for t being t-norm holds
    t <= minnorm
  proof
    let t be t-norm;
    set f1 = minnorm;
    for a,b being Element of [.0,1.] holds
      t.(a,b) <= f1.(a,b)
    proof
      let a,b be Element of [.0,1.];
      reconsider aa = a, bb = b as Element of [.0,1.];
A1:   f1.(a,b) = min (aa,bb) by MinDef;
      reconsider cc = 1 as Element of [.0,1.] by XXREAL_1:1;
      aa <= 1 by XXREAL_1:1; then
      t.(aa,bb) <= t.(cc,bb) by MonDef; then
      t.(aa,bb) <= t.(bb,cc) by BINOP_1:def 2; then
A3:   t.(aa,bb) <= bb by IdDef;
      bb <= 1 by XXREAL_1:1; then
      t.(aa,bb) <= t.(aa,cc) by MonDef; then
      t.(aa,bb) <= aa by IdDef;
      hence thesis by A1,XXREAL_0:20,A3;
    end;
    hence thesis;
  end;

theorem
  for t1, t2 being t-norm st t1 <= t2 holds
    conorm t2 <= conorm t1
  proof
    let t1, t2 be t-norm;
    set c1 = conorm t1, c2 = conorm t2;
    assume
A1: t1 <= t2;
    for a,b being Element of [.0,1.] holds
      c2.(a,b) <= c1.(a,b)
    proof
      let a,b be Element of [.0,1.];
      1-a in [.0,1.] & 1-b in [.0,1.] by OpIn01; then
      1 - t2.(1-a,1-b) <= 1 - t1.(1-a,1-b) by A1,XREAL_1:10; then
      1 - t2.(1-a,1-b) <= c1.(a,b) by CoDef;
      hence thesis by CoDef;
    end;
    hence thesis;
  end;

begin :: The Rest of Triangular Conorms

definition
  func Hamacher_conorm -> BinOp of [.0,1.] means :HamCoDef:
    for a,b being Element of [.0,1.] holds
      (a = b = 1 implies it.(a,b) = 1) &
      (a <> 1 or b <> 1 implies it.(a,b) = (a + b - 2 * a * b) / (1 - a * b));
  existence
  proof
    set C = [.0,1.];
    deffunc F(Element of C, Element of C) =
      In (($1 + $2 - 2 * $1 * $2) / (1 - $1 * $2),C);
    defpred P[set,set] means $1 = 1 & $2 = 1;
    deffunc G(Element of C,Element of C) = In(1,C);
    ex f being Function of [:C,C:],C st for c be Element of C,
       d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = G(c,d)) &
    (not P [c,d] implies f. [c,d] = F(c,d)) from SCHEME1:sch 21; then
    consider f being Function of [:C,C:],C such that
A1: for c be Element of C, d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = G(c,d)) &
    (not P [c,d] implies f. [c,d] = F(c,d));
    take f;
A0: dom f = [:C,C:] by FUNCT_2:def 1;
    let a,b be Element of C;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
    (a = b = 1 implies f.(a,b) = 1) &
    (a <> 1 or b <> 1 implies f.(a,b) = (a + b - 2 * a * b) / (1 - a * b))
    proof
      thus a = b = 1 implies f.(a,b) = 1
      proof
        assume a = b = 1; then
        f. [a,b] = G(a,b) by A1,AA
                .= 1 by SUBSET_1:def 8,XXREAL_1:1;
        hence thesis;
      end;
      assume a <> 1 or b <> 1; then
      f. [a,b] = F(a,b) by A1,AA
                .= (a + b - 2 * a * b) / (1 - a * b)
                by SUBSET_1:def 8,HamCoIn01;
      hence thesis;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds
      (a = b = 1 implies f1.(a,b) = 1) &
      (a <> 1 or b <> 1 implies f1.(a,b) = (a + b - 2 * a * b) / (1 - a * b))
      and
A2: for a,b being Element of [.0,1.] holds
      (a = b = 1 implies f2.(a,b) = 1) &
      (a <> 1 or b <> 1 implies
        f2.(a,b) = (a + b - 2 * a * b) / (1 - a * b));
    for a,b being set st a in [.0,1.] & b in [.0,1.] holds
      f1.(a,b) = f2.(a,b)
    proof
      let a,b be set;
      assume a in [.0,1.] & b in [.0,1.]; then
      reconsider aa = a, bb = b as Element of [.0,1.];
      per cases;
      suppose
B0:     aa = bb = 1; then
        f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B0;
        hence thesis;
      end;
      suppose
B1:     aa <> 1 or bb <> 1; then
        f1.(aa,bb) = (aa + bb - 2 * aa * bb) / (1 - aa * bb) by A1
                  .= f2.(aa,bb) by A2,B1;
        hence thesis;
      end;
    end;
    hence thesis by BINOP_1:def 21;
  end;
end;

theorem CoHam:
  conorm Hamacher_norm = Hamacher_conorm
  proof
    set dn = conorm Hamacher_norm;
    set dc = Hamacher_conorm;
    for a,b being Element of [.0,1.] holds
      dc.(a,b) = 1 - (Hamacher_norm).(1-a,1-b)
    proof
      let a,b be Element of [.0,1.];
AB:   0 in [.0,1.] by XXREAL_1:1;
A3:   1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01;
WE:   0 <= a <= 1 & 0 <= b <= 1 by XXREAL_1:1;
      per cases;
      suppose
Aa:     a <> 1 or b <> 1; then
AA:     1 - a * b <> 0 by WE,XREAL_1:150;
        dc.(a,b) = (a + b - 2 * a * b) / (1 - a * b) by HamCoDef,Aa
        .= ((1 * ((1 - a) + (1 - b) - (1 - a) * (1 - b))) -
           ((1 - a) * (1 - b)))
           / ((1 - a) + (1 - b) - (1 - a) * (1 - b))
        .= 1 - ((1 - a) * (1 - b)) / ((1 - a) + (1 - b) - (1 - a) * (1 - b))
           by XCMPLX_1:127,AA
        .= 1 - (Hamacher_norm).(1-a,1-b) by HamDef,A3;
        hence thesis;
      end;
      suppose
T1:     a = b = 1; then
        Hamacher_norm.(1-a,1-b) = (0 * 0) / (0 + 0 - 0 * 0) by HamDef,AB
          .= 0;
        hence thesis by T1,HamCoDef;
      end;
    end;
    hence thesis by CoDef;
  end;

registration
  cluster Hamacher_conorm -> commutative associative with-0-identity
    monotonic;
  coherence by CoHam;
end;

theorem
  conorm drastic_norm = drastic_conorm
  proof
    set dn = conorm drastic_norm;
    set dc = drastic_conorm;
    for a,b being Element of [.0,1.] holds
      dc.(a,b) = 1 - (drastic_norm).(1-a,1-b)
    proof
      let a,b be Element of [.0,1.];
A3:   1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01; then
we:   1 - a <= 1 & 1 - b <= 1 by XXREAL_1:1;
WE:   0 <= a & 0 <= b by XXREAL_1:1;
      per cases;
      suppose A0: a = 0 & b = 0; then
A1:     min (a,b) = 0;
A2:     max (1-a,1-b) = 1 by A0;
        dc.(a,b) = max (a,b) by Drastic2CDef,A1
             .= 1 - min (1-a,1-b) by A0
             .= 1 - (drastic_norm).(1-a,1-b) by Drastic2Def,A2,A3;
        hence thesis;
      end;
      suppose
BB:     a <> 0 & b <> 0; then
B0:     min (a,b) <> 0 by XXREAL_0:15;
        1 - a <> 1 & 1 - b <> 1 by BB; then
B1:     max (1-a,1-b) <> 1 by XXREAL_0:16;
        dc.(a,b) = 1 - 0 by Drastic2CDef,B0
          .= 1 - (drastic_norm).(1-a,1-b) by Drastic2Def,B1,A3;
        hence thesis;
      end;
      suppose
BB:     b <> 0 & a = 0; then
B0:     min (a,b) = 0 by WE,XXREAL_0:def 9;
B1:     min (1-a,1-b) = 1 - b by we,XXREAL_0:def 9,BB;
B8:     max (1-a,1-b) = 1 by XXREAL_0:def 10,we,BB;
        dc.(a,b) = max (a,b) by Drastic2CDef,B0
          .= 1 - min (1-a,1-b) by B1,BB,XXREAL_0:def 10,WE
          .= 1 - (drastic_norm).(1-a,1-b) by Drastic2Def,A3,B8;
        hence thesis;
      end;
      suppose
BB:     a <> 0 & b = 0; then
B0:     min (a,b) = 0 by WE,XXREAL_0:def 9;
B1:     min (1-a,1-b) = 1 - a by we,XXREAL_0:def 9,BB;
B8:     max (1-a,1-b) = 1 by XXREAL_0:def 10,we,BB;
        dc.(a,b) = max (a,b) by Drastic2CDef,B0
          .= 1 - min (1-a,1-b) by B1,BB,XXREAL_0:def 10,WE
          .= 1 - (drastic_norm).(1-a,1-b) by Drastic2Def,A3,B8;
        hence thesis;
      end;
    end;
    hence thesis by CoDef;
  end;

theorem ConormProd:
  conorm prodnorm = probsum_conorm
  proof
    set dn = conorm prodnorm;
    set dc = probsum_conorm;
    for a,b being Element of [.0,1.] holds
      dc.(a,b) = 1 - (prodnorm).(1-a,1-b)
    proof
      let a,b be Element of [.0,1.];
A3:   1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01;
      dc.(a,b) = a + b - a*b by ProbSumDef
             .= 1 - (1-a) * (1-b)
             .= 1 - (prodnorm).(1-a,1-b) by ProdDef,A3;
      hence thesis;
    end;
    hence thesis by CoDef;
  end;

registration
  cluster probsum_conorm -> commutative associative with-0-identity monotonic;
  coherence by ConormProd;
end;

definition
  func nilmax_conorm -> BinOp of [.0,1.] means :NilmaxDef:
    for a,b being Element of [.0,1.] holds
      (a + b < 1 implies it.(a,b) = max (a,b)) &
      (a + b >= 1 implies it.(a,b) = 1);
  existence
  proof
    set C = [.0,1.];
    defpred P[Real,Real] means $1 + $2 < 1;
    deffunc F(Element of C,Element of C) = In(max ($1,$2),C);
    deffunc G(Element of C,Element of C) = In(1,C);
    ex f being Function of [:C,C:],C st for c be Element of C,
    d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = F(c,d)) &
    (not P [c,d] implies f. [c,d] = G(c,d)) from SCHEME1:sch 21; then
    consider f being Function of [:C,C:],C such that
A1: for c be Element of C, d be Element of C st [c,d] in dom f holds
    (P[c,d] implies f. [c,d] = F(c,d)) &
    (not P [c,d] implies f. [c,d] = G(c,d));
    take f;
A0: dom f = [:C,C:] by FUNCT_2:def 1;
    let a,b be Element of C;
cc: max (a,b) = a or max (a,b) = b by XXREAL_0:16;
AA: [a,b] in dom f by A0,ZFMISC_1:87;
    (a + b < 1 implies f.(a,b) = max (a,b)) &
    (a + b >= 1 implies f.(a,b) = 1)
    proof
      thus a + b < 1 implies f.(a,b) = max (a,b)
      proof
        assume a + b < 1; then
        f. [a,b] = F(a,b) by A1,AA
                .= max (a,b) by SUBSET_1:def 8,cc;
        hence thesis;
      end;
      assume a + b >= 1; then
      f. [a,b] = G(a,b) by A1,AA
                .= 1 by XXREAL_1:1,SUBSET_1:def 8;
      hence thesis;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds
      (a + b < 1 implies f1.(a,b) = max (a,b)) &
      (a + b >= 1 implies f1.(a,b) = 1) and
A2: for a,b being Element of [.0,1.] holds
      (a + b < 1 implies f2.(a,b) = max (a,b)) &
      (a + b >= 1 implies f2.(a,b) = 1);
    for a,b being set st a in [.0,1.] & b in [.0,1.] holds
      f1.(a,b) = f2.(a,b)
    proof
      let a,b be set;
      assume a in [.0,1.] & b in [.0,1.]; then
      reconsider aa = a, bb = b as Element of [.0,1.];
      per cases;
      suppose
B0:     aa + bb < 1; then
        f1.(aa,bb) = max (aa,bb) by A1 .= f2.(aa,bb) by A2,B0;
        hence thesis;
      end;
      suppose
B1:     aa + bb >= 1; then
        f1.(aa,bb) = 1 by A1 .= f2.(aa,bb) by A2,B1;
        hence thesis;
      end;
    end;
    hence thesis by BINOP_1:def 21;
  end;
end;

theorem ConormNilmin:
  conorm nilmin_norm = nilmax_conorm
  proof
    set dn = conorm nilmin_norm;
    set dc = nilmax_conorm;
    for a,b being Element of [.0,1.] holds
      dc.(a,b) = 1 - (nilmin_norm).(1-a,1-b)
    proof
      let a,b be Element of [.0,1.];
A3:   1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01;
      per cases;
      suppose
W0:     a + b < 1; then
        2 - (a + b) > 2 - 1 by XREAL_1:10; then
W1:     1 - a + (1 - b) > 1;
        dc.(a,b) = max (a,b) by NilmaxDef,W0
             .= 1 - min (1-a,1-b) by MaxMin
             .= 1 - (nilmin_norm).(1-a,1-b) by NilminDef,A3,W1;
        hence thesis;
      end;
      suppose
W0:     a + b >= 1; then
        2 - (a + b) <= 2 - 1 by XREAL_1:10; then
W1:     1 - a + (1 - b) <= 1;
        dc.(a,b) = 1 - 0 by NilmaxDef,W0
             .= 1 - (nilmin_norm).(1-a,1-b) by NilminDef,A3,W1;
        hence thesis;
      end;
    end;
    hence thesis by CoDef;
  end;

registration
  cluster nilmax_conorm -> commutative associative with-0-identity monotonic;
  coherence by ConormNilmin;
end;

definition
  func BoundedSum_conorm -> BinOp of [.0,1.] means :LukConorm:
    for a,b being Element of [.0,1.] holds
      it.(a,b) = min (a + b,1);
  existence
  proof
    reconsider A = [.0,1.] as non empty real-membered set;
    deffunc F(Element of A, Element of A) = In (min ($1 + $2,1),A);
    ex f being Function of [:A,A:], A st
    for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y) from BINOP_1:sch 4; then
    consider f being BinOp of A such that
A1: for x being Element of A for y being Element of A holds
      f.(x,y) = F(x,y);
    reconsider ff = f as BinOp of [.0,1.];
    take ff;
    let a,b be Element of [.0,1.];
    reconsider aa = a, bb = b as Element of A;
    ff.(a,b) = F(aa,bb) by A1;
    hence thesis by SUBSET_1:def 8,Lemma2a;
  end;
  uniqueness
  proof
    let f1,f2 be BinOp of [.0,1.] such that
A1: for a,b being Element of [.0,1.] holds f1.(a,b) = min (a + b, 1) and
A2: for a,b being Element of [.0,1.] holds f2.(a,b) = min (a + b, 1);
A3: dom f1 = [:[.0,1.],[.0,1.]:] by FUNCT_2:def 1
          .= dom f2 by FUNCT_2:def 1;
    for x,y being object st
      [x,y] in dom f1 holds f1.(x,y) = f2.(x,y)
    proof
      let x,y be object;
      assume [x,y] in dom f1; then
      reconsider xx = x, yy = y as Element of [.0,1.] by ZFMISC_1:87;
      f1.(xx,yy) = min (xx + yy, 1) by A1
                .= f2.(xx,yy) by A2;
      hence thesis;
    end;
    hence thesis by A3,BINOP_1:20;
  end;
end;

theorem ConormLukasiewicz:
  conorm Lukasiewicz_norm = BoundedSum_conorm
  proof
    set dn = conorm Lukasiewicz_norm;
    set dc = BoundedSum_conorm;
    for a,b being Element of [.0,1.] holds
      dc.(a,b) = 1 - (Lukasiewicz_norm).(1-a,1-b)
    proof
      let a,b be Element of [.0,1.];
A3:   1 - a in [.0,1.] & 1 - b in [.0,1.] by OpIn01;
      dc.(a,b) = min (a+b,1) by LukConorm
             .= 1 - max (0,1-a+(1-b)-1) by LukasiDual
             .= 1 - (Lukasiewicz_norm).(1-a,1-b) by LukNorm,A3;
      hence thesis;
    end;
    hence thesis by CoDef;
  end;

registration
  cluster BoundedSum_conorm -> commutative associative with-0-identity
    monotonic;
  coherence by ConormLukasiewicz;
end;

theorem
  for t being t-conorm holds maxnorm <= t
  proof
    let t be t-conorm;
    set f1 = maxnorm;
    for a,b being Element of [.0,1.] holds
      f1.(a,b) <= t.(a,b)
    proof
      let a,b be Element of [.0,1.];
      reconsider aa = a, bb = b as Element of [.0,1.];
A1:   f1.(a,b) = max (aa,bb) by MaxDef;
      reconsider cc = 0 as Element of [.0,1.] by XXREAL_1:1;
      aa >= 0 by XXREAL_1:1; then
      t.(aa,bb) >= t.(cc,bb) by MonDef; then
      t.(aa,bb) >= t.(bb,cc) by BINOP_1:def 2; then
A3:   t.(aa,bb) >= bb by ZeroDef;
      bb >= 0 by XXREAL_1:1; then
      t.(aa,bb) >= t.(aa,cc) by MonDef; then
      t.(aa,bb) >= aa by ZeroDef;
      hence thesis by A1,XXREAL_0:28,A3;
    end;
    hence thesis;
  end;

theorem
  for t being t-conorm holds t <= drastic_conorm
  proof
    let t be t-conorm;
    set f1 = drastic_conorm;
    for a,b being Element of [.0,1.] holds
      f1.(a,b) >= t.(a,b)
    proof
      let a,b be Element of [.0,1.];
      per cases by XXREAL_0:15;
      suppose
A2:     a = 0; then
        reconsider aa = 0, bb = b as Element of [.0,1.];
        aa <= bb by XXREAL_1:1; then
        min (aa,bb) = 0 by XXREAL_0:def 9; then
A3:     f1.(aa,bb) = max(aa,bb) by Drastic2CDef;
        t.(aa,bb) = t.(bb,aa) by BINOP_1:def 2
                 .= b by ZeroDef;
        hence thesis by A2,A3,XXREAL_0:25;
      end;
      suppose
A2:     b = 0; then
        reconsider aa = a, bb = 0 as Element of [.0,1.];
        aa >= bb by XXREAL_1:1; then
        min (aa,bb) = 0 by XXREAL_0:def 9; then
A3:     f1.(aa,bb) = max(aa,bb) by Drastic2CDef;
        t.(aa,bb) = a by ZeroDef;
        hence thesis by A2,A3,XXREAL_0:25;
      end;
      suppose
aa:     min (a,b) <> 0;
        reconsider aa = a, bb = b as Element of [.0,1.];
        f1.(aa,bb) = 1 by Drastic2CDef,aa;
        hence thesis by XXREAL_1:1;
      end;
    end;
    hence thesis;
  end;