The Mizar article:

Basic Properties of Fuzzy Set Operation and Membership Function

by
Takashi Mitsuishi,
Katsumi Wasaki, and
Yasunari Shidama

Received May 22, 2000

Copyright (c) 2000 Association of Mizar Users

MML identifier: FUZZY_2
[ MML identifier index ]


environ

 vocabulary FUZZY_1, FUNCT_1, FUNCT_3, BOOLE, SQUARE_1, RELAT_1, SUBSET_1,
      ARYTM_1, PARTFUN1, RCOMP_1, INTEGRA1, ORDINAL2, FUZZY_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, SQUARE_1,
      REAL_1, RELSET_1, PARTFUN1, RFUNCT_1, INTEGRA1, SEQ_1, RCOMP_1, PSCOMP_1,
      FUZZY_1;
 constructors FUZZY_1, SQUARE_1, INTEGRA2, RFUNCT_1, REAL_1, PSCOMP_1;
 clusters RELSET_1, INTEGRA1, MEMBERED;
 requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
 theorems TARSKI, AXIOMS, FUNCT_1, FUNCT_3, REAL_1, REAL_2, SQUARE_1, PARTFUN1,
      RFUNCT_3, INTEGRA1, INTEGRA2, FUZZY_1, XBOOLE_0, XCMPLX_0, XCMPLX_1;
 schemes PARTFUN1;

begin

reserve x,y,y1,y2 for set;
reserve C for non empty set;
reserve c for Element of C;
reserve f,h,g,h1 for Membership_Func of C;
reserve A for FuzzySet of C,f;
reserve B for FuzzySet of C,g;
reserve D for FuzzySet of C,h;
reserve D1 for FuzzySet of C,h1;
reserve X for Universal_FuzzySet of C;
reserve E for Empty_FuzzySet of C;

:::::Basic Properties of Membership Function and Difference Set:::::

theorem Th1:
for x be Element of C,h be Membership_Func of C holds
0 <= h.x & h.x <= 1
proof
 let x be Element of C,h be Membership_Func of C;
A1:0 <= h.x
 proof
    chi({},C) = EMF(C) by FUZZY_1:def 13;
  then (EMF(C)).x = 0 by FUNCT_3:def 3;
  hence thesis by FUZZY_1:31;
 end;
   h.x <= 1
 proof
    chi(C,C) = UMF(C) by FUZZY_1:def 14;
  then (UMF(C)).x = 1 by FUNCT_3:def 3;
  hence thesis by FUZZY_1:31;
 end;
 hence thesis by A1;
end;

theorem Th2:
for x be Element of C holds (EMF(C)).x = 0 & (UMF(C)).x = 1
proof
 let x be Element of C;
   chi({},C) = EMF(C) & chi(C,C) = UMF(C) by FUZZY_1:def 13,def 14;
 hence thesis by FUNCT_3:def 3;
end;

theorem Th3:
for c holds f.c <= h.c implies max(f,min(g,h)).c = min(max(f,g),h).c
proof
 let c;
 assume A1:f.c <= h.c;
      max(f,min(g,h)).c = min(max(f,g),max(f,h)).c by FUZZY_1:16
 .= min(max(f,g).c,max(f,h).c) by FUZZY_1:6
 .= min(max(f,g).c,max(f.c,h.c)) by FUZZY_1:6
 .= min(max(f,g).c,h.c) by A1,SQUARE_1:def 2;
 hence thesis by FUZZY_1:6;
end;

theorem
  A c= D implies A \/ (B /\ D) = (A \/ B) /\ D
proof
 assume A1:A c= D;
   A \/ (B /\ D) = (A \/ B) /\ D
 proof
    max(f,min(g,h)) = min(max(f,g),h)
  proof
A2:C = dom max(f,min(g,h)) & C = dom min(max(f,g),h) by FUZZY_1:def 1;
     for x being Element of C st x in C holds
              max(f,min(g,h)).x = min(max(f,g),h).x
   proof
    let x be Element of C;
      f.x <= h.x by A1,FUZZY_1:def 4;
    hence thesis by Th3;
   end;
   hence thesis by A2,PARTFUN1:34;
  end;
  hence thesis by FUZZY_1:def 3;
 end;
 hence thesis;
end;


definition
let C be non empty set;
let f,g be Membership_Func of C;
let A be FuzzySet of C,f;
let B be FuzzySet of C,g;
func A\B ->
FuzzySet of C,min(f,1_minus g) equals
   [:C,min(f,1_minus g).:C:];
 correctness by FUZZY_1:def 2;
end;

canceled;

theorem Th6:
1_minus min(f,1_minus g) = max(1_minus f,g)
proof
   1_minus min(f,1_minus g) = max(1_minus f,1_minus(1_minus g)) by FUZZY_1:20;
 hence thesis by FUZZY_1:18;
end;

theorem
  (A\B)` = A` \/ B
proof
   1_minus min(f,1_minus g) = max(1_minus f,g) by Th6;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th8:
for c holds f.c <= g.c implies
min(f,1_minus h).c <= min(g,1_minus h).c
proof
 let c;
 assume f.c <= g.c;
 then min(f.c,(1_minus h).c) <= min(g.c,(1_minus h).c) by FUZZY_1:45;
 then min(f,1_minus h).c <= min(g.c,(1_minus h).c) by FUZZY_1:6;
 hence thesis by FUZZY_1:6;
end;

theorem
  A c= B implies A\D c= B\D
proof
 assume A1:A c= B;
   A\D c= B\D
 proof
    for c holds min(f,1_minus h).c <= min(g,1_minus h).c
  proof
   let c;
     f.c <= g.c by A1,FUZZY_1:def 4;
   hence thesis by Th8;
  end;
  hence thesis by FUZZY_1:def 4;
 end;
 hence thesis;
end;

theorem Th10:
for c holds f.c <= g.c implies
min(h,1_minus g).c <= min(h,1_minus f).c
proof
 let c;
 assume f.c <= g.c;
 then 1 - f.c >= 1 - g.c by REAL_2:106;
 then (1_minus g).c <= 1- f.c by FUZZY_1:def 7;
 then (1_minus g).c <= (1_minus f).c by FUZZY_1:def 7;
 then min((1_minus g).c,h.c) <= min((1_minus f).c,h.c) by FUZZY_1:45;
 then min(h,1_minus g).c <= min((1_minus f).c,h.c) by FUZZY_1:6;
 hence thesis by FUZZY_1:6;
end;

theorem
  A c= B implies D\B c= D\A
proof
 assume A1:A c= B;
   D\B c= D\A
 proof
    for c holds min(h,1_minus g).c <= min(h,1_minus f).c
  proof
   let c;
     f.c <= g.c by A1,FUZZY_1:def 4;
   hence thesis by Th10;
  end;
  hence thesis by FUZZY_1:def 4;
 end;
 hence thesis;
end;

theorem Th12:
for c holds f.c <= g.c & h.c <= h1.c implies
min(f,1_minus h1).c <= min(g,1_minus h).c
proof
 let c;
 assume f.c <= g.c & h.c <= h1.c;
 then f.c <= g.c & 1-h.c >= 1-h1.c by REAL_2:106;
 then min(f.c,1-h1.c) <= min(g.c,1- h.c) by FUZZY_1:44;
 then min(f.c,(1_minus h1).c) <= min(g.c,1- h.c) by FUZZY_1:def 7;
 then min(f.c,(1_minus h1).c) <= min(g.c,(1_minus h).c) by FUZZY_1:def 7;
 then min(f,1_minus h1).c <= min(g.c,(1_minus h).c) by FUZZY_1:6;
 hence thesis by FUZZY_1:6;
end;

theorem
  A c= B & D c= D1 implies A\D1 c= B\D
proof
 assume A1:A c= B & D c= D1;
   A\D1 c= B\D
 proof
    for c holds min(f,1_minus h1).c <= min(g,1_minus h).c
  proof
   let c;
     f.c <= g.c & h.c <= h1.c by A1,FUZZY_1:def 4;
   hence thesis by Th12;
  end;
  hence thesis by FUZZY_1:def 4;
 end;
 hence thesis;
end;

theorem Th14:
for c holds min(f,1_minus g).c <= f.c
proof
 let c;
   min(f.c,(1_minus g).c) <= f.c by SQUARE_1:35;
 hence thesis by FUZZY_1:6;
end;

theorem
  A\B c= A
proof
   for c holds min(f,1_minus g).c <= f.c by Th14;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th16:
for c holds min(f,1_minus g).c <= max(min(f,1_minus(g)),min(1_minus(f),g)).c
proof
 let c;
   max(min(f,1_minus(g)),min(1_minus(f),g)).c
 =max(min(f,1_minus(g)).c,min(1_minus(f),g).c) by FUZZY_1:6;
 hence thesis by SQUARE_1:46;
end;

theorem
  A\B c= A \+\ B
proof
   for c holds min(f,1_minus g).c <= max(min(f,1_minus(g)),min(1_minus(f),g)).c
    by Th16;
 hence thesis by FUZZY_1:def 4;
end;

theorem
  A\E = A
proof
   min(f,1_minus EMF(C)) = min(f,UMF(C)) by FUZZY_1:62
 .= f by FUZZY_1:32;
 hence thesis by FUZZY_1:def 3;
end;

theorem
  E\A = E
proof
   min(EMF(C),1_minus f) = min(1_minus f,EMF(C)) by FUZZY_1:7
 .= EMF(C) by FUZZY_1:32;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th20:
for c holds min(f,1_minus g).c <= min(f,1_minus min(f,g)).c
proof
 let c;
   min(f,1_minus min(f,g)).c = min(f,max(1_minus f,1_minus g)).c by FUZZY_1:20
 .=max(min(f,1_minus f),min(f,1_minus g)).c by FUZZY_1:16
 .=max(min(f,1_minus f).c,min(f,1_minus g).c) by FUZZY_1:6;
 hence thesis by SQUARE_1:46;
end;

theorem
  A\B c= A\(A /\ B)
proof
   for c holds min(f,1_minus g).c <= min(f,1_minus min(f,g)).c by Th20;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th22:
for c holds max(min(f,g),min(f,1_minus g)).c <= f.c
proof
 let c;
     max(min(f,g),min(f,1_minus g)).c
  =min(max(min(f,g),f),max(min(f,g),1_minus g)).c by FUZZY_1:16
 .=min(max(f,min(f,g)),max(min(f,g),1_minus g)).c by FUZZY_1:7
 .=min(f,max(min(f,g),1_minus g)).c by FUZZY_1:14
 .=min(f.c,max(min(f,g),1_minus g).c) by FUZZY_1:6;
 hence thesis by SQUARE_1:35;
end;

theorem Th23:
for c holds max(f,min(g,1_minus f)).c <= max(f,g).c
proof
 let c;
   max(f,min(g,1_minus f)).c = min(max(f,g),max(f,1_minus f)).c by FUZZY_1:16
 .= min(max(f,g).c,max(f,1_minus f).c) by FUZZY_1:6;
 hence thesis by SQUARE_1:35;
end;

theorem
  A \/ (B\A) c= A \/ B
proof
   for c holds max(f,min(g,1_minus f)).c <= max(f,g).c by Th23;
 hence thesis by FUZZY_1:def 4;
end;

theorem
  (A /\ B) \/ (A\B) c= A
proof
   for c holds max(min(f,g),min(f,1_minus g)).c <= f.c by Th22;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th26:
min(f,1_minus min(g,1_minus h)) = max(min(f,1_minus g),min(f,h))
proof
      min(f,1_minus min(g,1_minus h))
  = min(f,max(1_minus g,1_minus(1_minus h))) by FUZZY_1:20
 .= min(f,max(1_minus g,h)) by FUZZY_1:18;
 hence thesis by FUZZY_1:16;
end;

theorem
  A\(B\D) = (A\B) \/ (A /\ D)
proof
   min(f,1_minus min(g,1_minus h)) = max(min(f,1_minus g),min(f,h)) by Th26;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th28:
for c holds min(f,g).c <= min(f,1_minus(min(f,1_minus g))).c
proof
 let c;
      min(f,1_minus(min(f,1_minus g))).c
  = min(f,max(1_minus f,1_minus(1_minus g))).c by FUZZY_1:20
 .= min(f,max(1_minus f,g)).c by FUZZY_1:18
 .= max(min(f,1_minus f),min(f,g)).c by FUZZY_1:16
 .= max(min(f,1_minus f).c,min(f,g).c) by FUZZY_1:6;
 hence thesis by SQUARE_1:46;
end;

theorem
  A /\ B c= A\(A\B)
proof
   for c holds min(f,g).c <= min(f,1_minus(min(f,1_minus g))).c by Th28;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th30:
for c holds min(f,1_minus g).c <= min(max(f,g),1_minus g).c
proof
 let c;
      min(max(f,g),1_minus g).c = min(1_minus g,max(f,g)).c by FUZZY_1:7
 .= max(min(1_minus g,f),min(1_minus g,g)).c by FUZZY_1:16
 .= max(min(f,1_minus g),min(1_minus g,g)).c by FUZZY_1:7
 .= max(min(f,1_minus g).c,min(1_minus g,g).c) by FUZZY_1:6;
 hence thesis by SQUARE_1:46;
end;

theorem
  A\B c= (A \/ B)\B
proof
   for c holds min(f,1_minus g).c <= min(max(f,g),1_minus g).c by Th30;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th32:
min(f,1_minus max(g,h)) = min(min(f,1_minus g),min(f,1_minus h))
proof
     min(f,1_minus max(g,h)) = min(f,min(1_minus g,1_minus h)) by FUZZY_1:20
 .=min(min(f,f),min(1_minus g,1_minus h)) by FUZZY_1:7
 .=min(f,min(f,min(1_minus g,1_minus h))) by FUZZY_1:11
 .=min(f,min(min(f,1_minus g),1_minus h)) by FUZZY_1:11
 .=min(f,min(1_minus h,min(f,1_minus g))) by FUZZY_1:7
 .=min(min(f,1_minus h),min(f,1_minus g)) by FUZZY_1:11
 .=min(min(f,1_minus g),min(f,1_minus h)) by FUZZY_1:7;
 hence thesis;
end;

theorem
  A\(B \/ D) = (A\B) /\ (A\D)
proof
   min(f,1_minus max(g,h)) = min(min(f,1_minus g),min(f,1_minus h)) by Th32;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th34:
min(f,1_minus min(g,h)) = max(min(f,1_minus g),min(f,1_minus h))
proof
   min(f,1_minus min(g,h)) = min(f,max(1_minus g,1_minus h)) by FUZZY_1:20;
 hence thesis by FUZZY_1:16;
end;

theorem
  A\(B /\ D) = (A\B) \/ (A\D)
proof
   min(f,1_minus min(g,h)) = max(min(f,1_minus g),min(f,1_minus h)) by Th34;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th36:
min(min(f,1_minus g),1_minus h) = min(f,1_minus max(g,h))
proof
     min(min(f,1_minus g),1_minus h)
 = min(f,min(1_minus g,1_minus h)) by FUZZY_1:11;
 hence thesis by FUZZY_1:20;
end;

theorem
  (A\B)\D = A\(B \/ D)
proof
   min(min(f,1_minus g),1_minus h) = min(f,1_minus max(g,h)) by Th36;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th38:
for c holds
min(max(f,g),1_minus min(f,g)).c >= max(min(f,1_minus g),min(g,1_minus f)).c
proof
 let c;
      min(max(f,g),1_minus min(f,g)).c
  = min(max(f,g),max(1_minus(f),1_minus(g))).c by FUZZY_1:20
 .= max(min(max(f,g),1_minus f),min(max(f,g),1_minus g)).c by FUZZY_1:16
 .= max(min(1_minus f,max(f,g)),min(max(f,g),1_minus g)).c by FUZZY_1:7
 .= max(min(1_minus f,max(f,g)),min(1_minus g,max(f,g))).c by FUZZY_1:7
 .= max(max(min(1_minus f,f),min(1_minus f,g)),min(1_minus g,max(f,g))).c
                 by FUZZY_1:16
 .= max(max(min(1_minus f,f),min(1_minus f,g))
       ,max(min(1_minus g,f),min(1_minus g,g))).c by FUZZY_1:16
 .= max(max(max(min(1_minus f,f),min(1_minus f,g)),min(1_minus g,f)),
            min(1_minus g,g)).c by FUZZY_1:11
 .= max(max(min(1_minus f,f),max(min(1_minus f,g),min(1_minus g,f))),
               min(1_minus g,g)).c by FUZZY_1:11
 .= max(max(max(min(1_minus f,g),min(1_minus g,f)),min(1_minus f,f)),
               min(1_minus g,g)).c by FUZZY_1:7
 .= max(max(min(1_minus f,g),min(1_minus g,f)),
       max(min(1_minus f,f),min(1_minus g,g))).c by FUZZY_1:11
 .= max(max(min(1_minus g,f),min(1_minus f,g)),
       max(min(1_minus f,f),min(1_minus g,g))).c by FUZZY_1:7
 .= max(max(min(f,1_minus g),min(1_minus f,g)),
       max(min(1_minus f,f),min(1_minus g,g))).c by FUZZY_1:7
 .= max(max(min(f,1_minus g),min(g,1_minus f)),
       max(min(1_minus f,f),min(1_minus g,g))).c by FUZZY_1:7
 .= max(max(min(f,1_minus g),min(g,1_minus f)).c,
       max(min(1_minus f,f),min(1_minus g,g)).c) by FUZZY_1:6;
 hence thesis by SQUARE_1:46;
end;

theorem
  (A\B) \/ (B\A) c= (A \/ B)\(A /\ B)
proof
   for c holds
 min(max(f,g),1_minus min(f,g)).c
 >= max(min(f,1_minus g),min(g,1_minus f)).c by Th38;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th40:
min(max(f,g),1_minus h) = max(min(f,1_minus h),min(g,1_minus h))
proof
   min(max(f,g),1_minus h) = min(1_minus h,max(f,g)) by FUZZY_1:7
 .=max(min(1_minus h,f),min(1_minus h,g)) by FUZZY_1:16
 .=max(min(f,1_minus h),min(1_minus h,g)) by FUZZY_1:7;
 hence thesis by FUZZY_1:7;
end;

theorem
  (A \/ B)\D = (A\D) \/ (B\D)
proof
   min(max(f,g),1_minus h) = max(min(f,1_minus h),min(g,1_minus h)) by Th40;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th42:
for c holds min(f,1_minus g).c <= h.c & min(g,1_minus f).c <= h.c
implies max(min(f,1_minus g),min(1_minus f,g)).c <= h.c
proof
 let c;
 assume min(f,1_minus g).c <= h.c & min(g,1_minus f).c <= h.c;
 then max(min(f,1_minus g).c,min(g,1_minus f).c) <= max(h.c,h.c) by RFUNCT_3:7
;
 then max(min(f,1_minus g).c,min(1_minus f,g).c) <= max(h.c,h.c) by FUZZY_1:7;
 hence thesis by FUZZY_1:6;
end;

theorem
  A\B c= D & B\A c= D implies A \+\ B c= D
proof
 assume A1:A\B c= D & B\A c= D;
   A \+\ B c= D
 proof
    for c holds max(min(f,1_minus g),min(1_minus f,g)).c <= h.c
  proof
   let c;
     min(f,1_minus g).c <= h.c & min(g,1_minus f).c <= h.c by A1,FUZZY_1:def 4;
   hence thesis by Th42;
  end;
  hence thesis by FUZZY_1:def 4;
 end;
 hence thesis;
end;

theorem
  A /\ (B\D) = (A /\ B)\D
proof
   min(f,min(g,1_minus h)) = min(min(f,g),1_minus h) by FUZZY_1:11;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th45:
for c holds min(f,min(g,1_minus h)).c <= min(min(f,g),1_minus min(f,h)).c
proof
 let c;
A1: min(f,min(g,1_minus h)).c = min(min(f,g),1_minus h).c by FUZZY_1:11
 .= min(min(f,g).c,(1_minus h).c) by FUZZY_1:6;
   (1_minus h).c <= max((1_minus f).c,(1_minus h).c) by SQUARE_1:46;
 then min(min(f,g).c,(1_minus h).c)
 <= min(min(f,g).c,max((1_minus f).c,(1_minus h).c)) by FUZZY_1:44;
 then min(min(f,g).c,(1_minus h).c)
 <= min(min(f,g).c,max(1_minus f,1_minus h).c) by FUZZY_1:6;
 then min(min(f,g).c,(1_minus h).c)
 <= min(min(f,g),max(1_minus f,1_minus h)).c by FUZZY_1:6;
 hence thesis by A1,FUZZY_1:20;
end;

theorem
  A /\ (B\D) c= (A /\ B)\(A /\ D)
proof
   for c holds
 min(f,min(g,1_minus h)).c <= min(min(f,g),1_minus min(f,h)).c by Th45;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th47:
for c holds
min(max(f,g),1_minus min(f,g)).c >= max(min(f,1_minus g),min(1_minus f,g)).c
proof
 let c;
      min(max(f,g),1_minus min(f,g)).c
  = min(max(f,g),max(1_minus f,1_minus g)).c by FUZZY_1:20
 .= max(min(max(f,g),1_minus f),min(max(f,g),1_minus g)).c by FUZZY_1:16
 .= max(min(1_minus f,max(f,g)),min(max(f,g),1_minus g)).c by FUZZY_1:7
 .= max(min(1_minus f,max(f,g)),min(1_minus g,max(f,g))).c by FUZZY_1:7
 .= max(max(min(1_minus f,f),min(1_minus f,g)),min(1_minus g,max(f,g))).c
         by FUZZY_1:16
 .= max(max(min(1_minus f,f),min(1_minus f,g)),
        max(min(1_minus g,f),min(1_minus g,g))).c by FUZZY_1:16
 .= max(max(min(1_minus f,f),min(1_minus f,g)),
         max(min(1_minus g,g),min(1_minus g,f))).c by FUZZY_1:7
  .= max(max(max(min(1_minus f,f),min(1_minus f,g)),min(1_minus g,g))
                ,min(1_minus g,f)).c by FUZZY_1:11
 .= max(max(min(1_minus f,f),max(min(1_minus f,g),min(1_minus g,g)))
                ,min(1_minus g,f)).c by FUZZY_1:11
 .= max(max(min(1_minus f,f),max(min(1_minus g,g),min(1_minus f,g)))
                ,min(1_minus g,f)).c by FUZZY_1:7
 .= max(max(max(min(1_minus f,f),min(1_minus g,g)),min(1_minus f,g))
                ,min(1_minus g,f)).c by FUZZY_1:11
 .= max(max(min(1_minus f,f),min(1_minus g,g)),max(min(1_minus f,g)
                 ,min(1_minus g,f))).c by FUZZY_1:11
 .= max(max(min(1_minus f,f),min(1_minus g,g)),max(min(1_minus g,f)
                 ,min(1_minus f,g))).c by FUZZY_1:7
 .= max(max(min(1_minus f,f),min(1_minus g,g)),max(min(f,1_minus g)
                ,min(1_minus f,g))).c by FUZZY_1:7
 .= max(max(min(1_minus f,f),min(1_minus g,g)).c,
        max(min(f,1_minus g),min(1_minus f,g)).c) by FUZZY_1:6;
 hence thesis by SQUARE_1:46;
end;

theorem
  A \+\ B c= (A \/ B)\(A /\ B)
proof
   for c holds
 min(max(f,g),1_minus min(f,g)).c >= max(min(f,1_minus g),min(1_minus f,g)).c
  by Th47;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th49:
for c holds
max(min(f,g),1_minus max(f,g)).c
<= (1_minus max(min(f,1_minus g),min(1_minus f,g))).c
proof
 let c;
      min(max(f,g),1_minus min(f,g)).c
 >= max(min(f,1_minus g),min(1_minus f,g)).c by Th47;
 then 1-min(max(f,g),1_minus min(f,g)).c
 <= 1-max(min(f,1_minus g),min(1_minus f,g)).c by REAL_2:106;
 then (1_minus min(max(f,g),1_minus min(f,g))).c
 <= 1-max(min(f,1_minus g),min(1_minus f,g)).c by FUZZY_1:def 7;
 then (1_minus min(max(f,g),1_minus min(f,g))).c
 <= (1_minus max(min(f,1_minus g),min(1_minus f,g))).c by FUZZY_1:def 7;
 then (max(1_minus max(f,g),1_minus(1_minus min(f,g)))).c
 <= (1_minus max(min(f,1_minus g),min(1_minus f,g))).c by FUZZY_1:20;
 then (max(1_minus max(f,g),min(f,g))).c
 <= (1_minus max(min(f,1_minus g),min(1_minus f,g))).c by FUZZY_1:18;
 hence thesis by FUZZY_1:7;
end;

theorem
  (A /\ B) \/ (A \/ B)` c= (A \+\ B)`
proof
  for c holds
max(min(f,g),1_minus max(f,g)).c
<= (1_minus max(min(f,1_minus g),min(1_minus f,g))).c by Th49;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th51:
min(max(min(f,1_minus g),min(1_minus f,g)),1_minus h)
=max(min(f,1_minus max(g,h)),min(g,1_minus max(f,h)))
proof
 set f1 = 1_minus f, g1 = 1_minus g, h1 = 1_minus h;
      min(max(min(f,g1),min(f1,g)),h1)
  = min(h1,max(min(f,g1),min(f1,g))) by FUZZY_1:7
 .= max(min(h1,min(f,g1)),min(h1,min(f1,g))) by FUZZY_1:16
 .= max(min(h1,min(g1,f)),min(h1,min(f1,g))) by FUZZY_1:7
 .= max(min(min(h1,g1),f),min(h1,min(f1,g))) by FUZZY_1:11
 .= max(min(min(h1,g1),f),min(min(h1,f1),g)) by FUZZY_1:11
 .= max(min(f,min(h1,g1)),min(min(h1,f1),g)) by FUZZY_1:7
 .= max(min(f,min(h1,g1)),min(g,min(h1,f1))) by FUZZY_1:7
 .= max(min(f,1_minus max(h,g)),min(g,min(h1,f1))) by FUZZY_1:20
 .= max(min(f,1_minus max(h,g)),min(g,1_minus max(h,f))) by FUZZY_1:20
 .= max(min(f,1_minus max(h,g)),min(g,1_minus max(f,h))) by FUZZY_1:7;
 hence thesis by FUZZY_1:7;
end;

theorem
  (A \+\ B)\D = (A\(B \/ D)) \/ (B\(A \/ D))
proof
   min(max(min(f,1_minus g),min(1_minus f,g)),1_minus h)
 =max(min(f,1_minus max(g,h)),min(g,1_minus max(f,h))) by Th51;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th53:
for c holds
min(f,1_minus max(min(g,1_minus h),min(1_minus g,h))).c
>= max(min(f,1_minus max(g,h)),min(min(f,g),h)).c
proof
 let c;
A1: max(min(f,1_minus max(g,h)),min(min(f,g),h)).c
  = max(min(f,1_minus max(g,h)),min(f,min(g,h))).c by FUZZY_1:11
 .= min(f,max(1_minus max(g,h),min(g,h))).c by FUZZY_1:16
 .= min(f,max(min(g,h),1_minus max(g,h))).c by FUZZY_1:7
 .= min(f.c,max(min(g,h),1_minus max(g,h)).c) by FUZZY_1:6;
      max(min(g,h),1_minus max(g,h)).c
 <= (1_minus max(min(g,1_minus h),min(1_minus g,h))).c by Th49;
 then min(f.c,max(min(g,h),1_minus max(g,h)).c)
 <= min(f.c,(1_minus max(min(g,1_minus h),min(1_minus g,h))).c) by FUZZY_1:44;
 hence thesis by A1,FUZZY_1:6;
end;

theorem
  (A\(B \/ D)) \/ ((A /\ B) /\ D) c= A\(B \+\ D)
proof
   for c holds
 min(f,1_minus max(min(g,1_minus h),min(1_minus g,h))).c
 >= max(min(f,1_minus max(g,h)),min(min(f,g),h)).c by Th53;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th55:
for c holds f.c <= g.c implies g.c >= max(f,min(g,1_minus f)).c
proof
 let c;
 assume A1:f.c <= g.c;
      max(f,min(g,1_minus f)).c = min(max(f,g),max(f,1_minus f)).c by FUZZY_1:
16
 .= min(max(f,g).c,max(f,1_minus f).c) by FUZZY_1:6
 .= min(max(f.c,g.c),max(f,1_minus f).c) by FUZZY_1:6
 .= min(g.c,max(f,1_minus f).c) by A1,SQUARE_1:def 2;
 hence thesis by SQUARE_1:35;
end;

theorem
  A c= B implies A \/ (B\A) c= B
proof
 assume A1:A c= B;
   A \/ (B\A) c= B
 proof
    for c holds g.c >= max(f,min(g,1_minus f)).c
  proof
   let c;
     f.c <= g.c by A1,FUZZY_1:def 4;
   hence thesis by Th55;
  end;
  hence thesis by FUZZY_1:def 4;
 end;
 hence thesis;
end;

theorem
  for c holds
max(f,g).c >= max(max(min(f,1_minus g),min(1_minus f,g)),min(f,g)).c
proof
 set f1 = 1_minus f, g1 = 1_minus g;
 let c;
      max(max(min(f,1_minus g),min(1_minus f,g)),min(f,g)).c
  = max(min(f,g1),max(min(f1,g),min(f,g))).c by FUZZY_1:11
 .= max(min(f,g1),min(max(min(f1,g),f),max(min(f1,g),g))).c by FUZZY_1:16
 .= max(min(f,g1),min(max(min(f1,g),f),max(g,min(f1,g)))).c by FUZZY_1:7
 .= max(min(f,g1),min(max(min(f1,g),f),max(g,min(g,f1)))).c by FUZZY_1:7
 .= max(min(f,g1),min(max(min(f1,g),f),g)).c by FUZZY_1:14
 .= min(max(min(f,g1),max(min(f1,g),f)),max(min(f,g1),g)).c by FUZZY_1:16
 .= min(max(min(f,g1),max(min(f1,g),f)).c,max(min(f,g1),g).c) by FUZZY_1:6;
 then A1:max(max(min(f,1_minus g),min(1_minus f,g)),min(f,g)).c <= max(min(f,g1
),g).c
            by SQUARE_1:35;
      max(min(f,g1),g).c = max(g,min(f,g1)).c by FUZZY_1:7
 .= min(max(g,f),max(g,g1)).c by FUZZY_1:16
 .= min(max(f,g),max(g,g1)).c by FUZZY_1:7
 .= min(max(f,g).c,max(g,g1).c) by FUZZY_1:6;
 then max(min(f,g1),g).c <= max(f,g).c by SQUARE_1:35;
 hence thesis by A1,AXIOMS:22;
end;

canceled;

theorem Th59:
min(f,1_minus g) = EMF(C) implies for c holds f.c <= g.c
proof
 assume A1:min(f,1_minus g) = EMF(C);
   for c holds f.c <= g.c
 proof
  let c;
A2:min(f.c,(1_minus g).c) = (EMF(C)).c by A1,FUZZY_1:6;
    now per cases by A2,SQUARE_1:38;
   suppose f.c = (EMF(C)).c;
   hence f.c <= g.c by FUZZY_1:31;
   suppose A3:(1_minus g).c = (EMF(C)).c;
     f.c <= g.c
   proof
      g.c = (1_minus (1_minus g)).c by FUZZY_1:18
       .= 1 - (1_minus g).c by FUZZY_1:def 7
       .= (1_minus EMF(C)).c by A3,FUZZY_1:def 7
       .= (UMF(C)).c by FUZZY_1:62;
    hence thesis by FUZZY_1:31;
   end;
   hence thesis;
  end;
  hence thesis;
 end;
 hence thesis;
end;

theorem
  A\B = E implies A c= B
proof
 assume A1:A\B = E;
   A c= B
 proof
    for c holds f . c <= g . c
  proof
   let c;
     min(f,1_minus g) = EMF(C) by A1,FUZZY_1:def 3;
   hence thesis by Th59;
  end;
  hence thesis by FUZZY_1:def 4;
 end;
 hence thesis;
end;

theorem Th61:
min(f,g) = EMF(C) implies min(f,1_minus g) = f
proof
 assume A1:min(f,g) = EMF(C);
   min(f,1_minus g) = f
 proof
A2:C = dom min(f,1_minus g) & C = dom f by FUZZY_1:def 1;
    for x being Element of C st x in C holds min(f,1_minus g).x = f.x
  proof
   let x be Element of C;
A3:(EMF(C)).x = min(f.x,g.x) by A1,FUZZY_1:6;
     now per cases by A3,SQUARE_1:38;
    suppose A4:f.x = (EMF(C)).x;
      min(f,1_minus g).x = f.x
    proof
       min(f,1_minus g).x = min(f.x,(1_minus g).x) by FUZZY_1:6
                       .= min(1_minus g,EMF(C)).x by A4,FUZZY_1:6
                       .= (EMF(C)).x by FUZZY_1:32;
     hence thesis by A4;
    end;
    hence thesis;
    suppose A5:g.x = (EMF(C)).x;
      min(f,1_minus g).x = f.x
    proof
       min(f,1_minus g).x = min(f.x,(1_minus g).x) by FUZZY_1:6
                       .= min(f.x,1 - (EMF(C)).x) by A5,FUZZY_1:def 7
                       .= min(f.x,(1_minus EMF(C)).x) by FUZZY_1:def 7
                       .= min(f.x,(UMF(C)).x) by FUZZY_1:62
                       .= min(f,UMF(C)).x by FUZZY_1:6;
     hence thesis by FUZZY_1:32;
    end;
    hence thesis;
   end;
   hence thesis;
   end;
  hence thesis by A2,PARTFUN1:34;
 end;
 hence thesis;
end;

theorem
  A /\ B = E implies A\B = A
proof
 assume A /\ B = E;
 then min(f,g) = EMF(C) by FUZZY_1:def 3;
 then min(f,1_minus g) = f by Th61;
 hence thesis by FUZZY_1:def 3;
end;

begin
:::::Algebraic Product and Algebraic Sum:::::

definition
let C be non empty set;
let h,g be Membership_Func of C;
func h*g -> Membership_Func of C means :Def2:
for c being Element of C holds it.c = (h.c)*(g.c);
existence
proof
 defpred P[set,set] means $2 = (h.$1)*(g.$1);
 A1:for x,y st x in C & P[x,y] holds y in REAL;
 A2:for x,y1,y2 st x in C & P[x,y1] & P[x,y2] holds y1=y2;
  consider IT being PartFunc of C,REAL such that
 A3:(for x holds x in dom IT iff x in C & ex y st P[x,y]) &
    (for x st x in dom IT holds P[x,IT.x]) from PartFuncEx(A1,A2);
 A4:dom IT = C & rng IT c= [.0,1.]
  proof
  A5:dom IT = C
   proof
     C c= dom IT
    proof
       for x being set st x in C holds x in dom IT
     proof
      let x be set;
      assume A6:x in C;
        ex y st y = (h.x)*(g.x);
      hence thesis by A3,A6;
     end;
     hence thesis by TARSKI:def 3;
    end;
    hence thesis by XBOOLE_0:def 10;::a7,
   end;
    rng IT c= [.0,1.]
  proof
A7:rng h c= [.0,1.] & rng g c= [.0,1.] by FUZZY_1:def 1;
     for y being set st y in rng IT holds y in [.0,1.]
   proof
    let y be set; assume y in rng IT;
    then consider x being Element of C such that
A8:x in dom IT & y = IT.x by PARTFUN1:26;
    reconsider A=[.0,1.] as closed-interval Subset of REAL by INTEGRA1:def 1;
      A = [. inf A, sup A .] by INTEGRA1:5;
then A9:0=inf A & 1=sup A by INTEGRA1:6;
      x in C;
    then x in dom h & x in dom g by FUZZY_1:def 1;
    then h.x in rng h & g.x in rng g by FUNCT_1:def 5;
    then 0 <= h.x & h.x <= 1 & 0 <= g.x & g.x <= 1 by A7,A9,INTEGRA2:1;
    then 0 <= (h.x)*(g.x) & (h.x)*(g.x) <= 1 by REAL_2:140,SQUARE_1:19;
    then 0 <= IT.x & IT.x <= 1 by A3,A8;
    hence thesis by A8,A9,INTEGRA2:1;
   end;
   hence thesis by TARSKI:def 3;
  end;
  hence thesis by A5;
  end;
 then A10:IT is Membership_Func of C by FUZZY_1:def 1;
   for c being Element of C holds IT.c = (h.c)*(g.c) by A3,A4;
 hence thesis by A10;
 end;
uniqueness
proof
  let F,G be Membership_Func of C;
  assume that
A11:for c being Element of C holds F.c = (h.c)*(g.c)
  and
A12:for c being Element of C holds G.c = (h.c)*(g.c);
A13:C = dom F & C = dom G by FUZZY_1:def 1;
    for c being Element of C st c in C holds F.c = G.c
  proof
   let c be Element of C;
     F.c = (h.c)*(g.c) & G.c = (h.c)*(g.c) by A11,A12;
   hence thesis;
  end;
 hence thesis by A13,PARTFUN1:34;
 end;
end;

definition
let C be non empty set;
let h,g be Membership_Func of C;
func h ++ g -> Membership_Func of C means :Def3:
for c being Element of C holds it.c = h.c + g.c -(h.c)*(g.c);
existence
proof
 defpred P[set,set] means $2 = h.$1 + g.$1 -(h.$1)*(g.$1);
 A1:for x,y st x in C & P[x,y] holds y in REAL;
 A2:for x,y1,y2 st x in C & P[x,y1] & P[x,y2] holds y1=y2;
  consider IT being PartFunc of C,REAL such that
 A3:(for x holds x in dom IT iff x in C & ex y st P[x,y]) &
    (for x st x in dom IT holds P[x,IT.x]) from PartFuncEx(A1,A2);
 A4:dom IT = C & rng IT c= [.0,1.]
  proof
  A5:dom IT = C
   proof
     C c= dom IT
    proof
       for x being set st x in C holds x in dom IT
     proof
      let x be set;
      assume A6:x in C;
        ex y st y = h.x + g.x -(h.x)*(g.x);
      hence thesis by A3,A6;
     end;
     hence thesis by TARSKI:def 3;
    end;
    hence thesis by XBOOLE_0:def 10;
   end;
    rng IT c= [.0,1.]
  proof
     for y being set st y in rng IT holds y in [.0,1.]
   proof
    let y be set; assume y in rng IT;
    then consider x being Element of C such that
A7:x in dom IT & y = IT.x by PARTFUN1:26;
    reconsider A=[.0,1.] as closed-interval Subset of REAL by INTEGRA1:def 1;
      A = [. inf A, sup A .] by INTEGRA1:5;
then A8:0=inf A & 1=sup A by INTEGRA1:6;
      0 <= h.x + g.x -(h.x)*(g.x) & h.x + g.x -(h.x)*(g.x) <= 1
    proof
       0 <= (1_minus h).x & (1_minus h).x <= 1 &
     0 <= (1_minus g).x & (1_minus g).x <= 1 by Th1;
     then 0 <= 1-h.x & 1-h.x <= 1 & 0 <= 1- g.x & 1-g.x <= 1 by FUZZY_1:def 7;
     then 0 <= (1-h.x)*(1-g.x) & (1-h.x)*(1-g.x) <= 1 by REAL_2:140,SQUARE_1:19
;
     then A9: 1 - (1-h.x)*(1-g.x) >= 1 - 1 & 1-0 >= 1 -(1-h.x)*(1-g.x) by
REAL_2:106;
          1 - (1-h.x)*(1-g.x) = 1-(1*1-1*g.x-h.x*1+ (h.x)*(g.x)) by XCMPLX_1:47
     .= 1-(1-g.x-h.x) - (h.x)*(g.x) by XCMPLX_1:36
     .= 1-(1-g.x) + h.x - (h.x)*(g.x) by XCMPLX_1:37
     .= 1-1 + g.x + h.x - (h.x)*(g.x) by XCMPLX_1:37
     .= h.x + g.x -(h.x)*(g.x);
     hence thesis by A9;
    end;
    then 0 <= IT.x & IT.x <= 1 by A3,A7;
    hence thesis by A7,A8,INTEGRA2:1;::
   end;
   hence thesis by TARSKI:def 3;
  end;
  hence thesis by A5;
  end;
 then A10:IT is Membership_Func of C by FUZZY_1:def 1;
   for c being Element of C holds IT.c = h.c + g.c -(h.c)*(g.c) by A3,A4;
 hence thesis by A10;
 end;
uniqueness
proof
  let F,G be Membership_Func of C;
  assume that
A11:for c being Element of C holds F.c = h.c + g.c -(h.c)*(g.c)
  and
A12:for c being Element of C holds G.c = h.c + g.c -(h.c)*(g.c);
A13:C = dom F & C = dom G by FUZZY_1:def 1;
    for c being Element of C st c in C holds F.c = G.c
  proof
   let c be Element of C;
     F.c = h.c + g.c -(h.c)*(g.c) & G.c = h.c + g.c -(h.c)*(g.c) by A11,A12;
   hence thesis;
  end;
 hence thesis by A13,PARTFUN1:34;
 end;
end;


definition
let C be non empty set;
let h,g be Membership_Func of C;
let A be FuzzySet of C,h;
let B be FuzzySet of C,g;
func A * B -> FuzzySet of C,h*g equals
   [:C,(h*g).:C:];
 correctness by FUZZY_1:def 2;
end;


definition
let C be non empty set;
let h,g be Membership_Func of C;
let A be FuzzySet of C,h;
let B be FuzzySet of C,g;
func A ++ B -> FuzzySet of C,(h ++ g) equals
   [:C,(h ++ g).:C:];
 correctness by FUZZY_1:def 2;
end;

theorem Th63:
for c holds (f*f).c <= f.c & (f ++ f).c >= f.c
proof
 let c;
A1:(f*f).c <= f.c
 proof
    f.c <= 1 & 0 <= f.c by Th1;
  then (f.c)*(f.c) <= 1*(f.c) by AXIOMS:25;
  hence thesis by Def2;
 end;
   (f ++ f).c >= f.c
 proof
    0 <= (1_minus f).c & 0 <= f.c by Th1;
  then 0*(f.c) <= (f.c)*((1_minus f).c) by AXIOMS:25;
  then 0 <= (f.c)*(1 - f.c) by FUZZY_1:def 7;
  then 0 <= (f.c)*1 - (f.c)*(f.c) by XCMPLX_1:40;
  then 0 + f.c <= f.c - (f.c)*(f.c) + f.c by AXIOMS:24;
  then f.c <= f.c + f.c - (f.c)*(f.c) by XCMPLX_1:29;
  hence thesis by Def3;
 end;
 hence thesis by A1;
end;

theorem
  A*A c= A & A c= A ++ A
proof
   for c holds (f*f).c <= f.c & (f ++ f).c >= f.c by Th63;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th65:
f*g = g*f & f ++ g = g ++ f
proof
A1: C = dom (f*g) & C = dom (g*f) &
 C = dom (f ++ g) & C = dom (g ++ f) by FUZZY_1:def 1;
A2:f*g = g*f
 proof
    for c being Element of C st c in C holds
  (f*g).c = (g*f).c
  proof
   let c be Element of C;
     (f*g).c = (g.c)*(f.c) by Def2;
   hence thesis by Def2;
  end;
  hence thesis by A1,PARTFUN1:34;
 end;
   f ++ g = g ++ f
 proof
    for c being Element of C st c in C holds (f ++ g).c = (g ++ f).c
  proof
   let c be Element of C;
     (f ++ g).c = g.c + f.c - (g.c)*(f.c) by Def3;
   hence thesis by Def3;
  end;
  hence thesis by A1,PARTFUN1:34;
 end;
 hence thesis by A2;
end;

theorem
  A*B = B*A & A ++ B = B ++ A
proof
   f*g = g*f & f ++ g = g ++ f by Th65;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th67:
(f*g)*h = f*(g*h)
proof
A1:C = dom ((f*g)*h) & C = dom (f*(g*h)) by FUZZY_1:def 1;
   for c being Element of C st c in C holds ((f*g)*h).c = (f*(g*h)).c
 proof
  let c;
    ((f*g)*h).c = ((f*g).c)*(h.c) by Def2
             .= ((f.c)*(g.c))*(h.c) by Def2
             .= (f.c)*((g.c)*(h.c)) by XCMPLX_1:4
             .= (f.c)*((g*h).c) by Def2;
  hence thesis by Def2;
 end;
 hence thesis by A1,PARTFUN1:34;
end;

theorem
  (A*B)*D = A*(B*D)
proof
   (f*g)*h = f*(g*h) by Th67;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th69:
(f ++ g) ++ h = f ++ (g ++ h)
proof
A1:C = dom((f ++ g) ++ h) & C = dom(f ++ (g ++ h)) by FUZZY_1:def 1;
   for c being Element of C st c in C holds ((f ++ g) ++ h).c = (f ++ (g ++ h))
.
c
 proof
  let c;
  set x = f.c, y = g.c, z = h.c;
A2:  ((f ++ g) ++ h).c = (f ++ g).c + h.c - ((f ++ g).c)*(h.c) by Def3
  .= f.c + g.c -(f.c)*(g.c) + h.c - ((f ++ g).c)*(h.c) by Def3
  .= ((f.c + g.c) -(f.c)*(g.c) + h.c) - (f.c + g.c -(f.c)*(g.c))*(h.c) by Def3
  .= (-x*y + (x + y)) + z - (x + y -x*y)*z by XCMPLX_0:def 8
  .= -x*y + ((x + y) + z) - (x + y -x*y)*z by XCMPLX_1:1
  .= -x*y - (x + y -x*y)*z + (x + y + z) by XCMPLX_1:29
  .= -x*y - (x*z + y*z -x*y*z) + (x + y + z) by XCMPLX_1:43
  .= -x*y - (x*z + y*z) +x*y*z + (x + y + z) by XCMPLX_1:37
  .= -x*y - x*z - y*z +x*y*z + (x + y + z) by XCMPLX_1:36;
       (f ++ (g ++ h)).c = x + (g ++ h).c -x*((g ++ h).c) by Def3
  .= x + (y + z -y*z) -x*((g ++ h).c) by Def3
  .= x + (y + z -y*z) -x*(y + z -y*z) by Def3
  .= x + (y + z) -y*z -x*(y + z -y*z) by XCMPLX_1:29
  .= -y*z -x*(y + z -y*z) + (x + (y + z)) by XCMPLX_1:158
  .= -y*z -(y*x + z*x -y*z*x) + (x + (y + z)) by XCMPLX_1:43
  .= -y*z -(x*y + x*z) +x*(y*z) + (x + (y + z)) by XCMPLX_1:37
  .= -y*z -x*y - x*z +x*(y*z) + (x + (y + z)) by XCMPLX_1:36
  .= -y*z -x*y - x*z +x*(y*z) + (x + y + z) by XCMPLX_1:1
  .= -y*z -x*y - x*z +x*y*z + (x + y + z) by XCMPLX_1:4;
  hence thesis by A2,XCMPLX_1:147;
 end;
 hence thesis by A1,PARTFUN1:34;
end;

theorem
  (A ++ B) ++ D = A ++ (B ++ D)
proof
   (f ++ g) ++ h = f ++ (g ++ h) by Th69;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th71:
for c holds (f*(f ++ g)).c <= f.c & (f ++ (f*g)).c >= f.c
proof
 let c;
A1:(f*(f ++ g)).c <= f.c
 proof
    0 <= f.c & (f ++ g).c <= 1 by Th1;
  then ((f ++ g).c)*(f.c) <= 1*(f.c) by AXIOMS:25;
  hence thesis by Def2;
 end;
   (f ++ (f*g)).c >= f.c
 proof
    (f*g).c >= 0 & (1_minus f).c >= 0 by Th1;
  then 0*((f*g).c) <= ((1_minus f).c)*((f*g).c) by AXIOMS:25;
  then 0 <= (1 - f.c)*((f*g).c) by FUZZY_1:def 7;
  then 0 <= 1*((f*g).c) - (f.c)*((f*g).c) by XCMPLX_1:40;
  then 0+f.c <= (f*g).c - (f.c)*((f*g).c) + f.c by AXIOMS:24;
  then f.c <= f.c + (f*g).c - (f.c)*((f*g).c) by XCMPLX_1:29;
  hence thesis by Def3;
 end;
 hence thesis by A1;
end;

theorem
  A*(A ++ B) c= A & A c= A ++ (A*B)
proof
   for c holds (f*(f ++ g)).c <= f.c & (f ++ (f*g)).c >= f.c by Th71;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th73:
for c holds (f*(g ++ h)).c <= ((f*g) ++ (f*h)).c
proof
 let c;
 set x = f.c, y = g.c, z = h.c;
   (f*f).c <= f.c & (g*h).c >= 0 by Th1,Th63;
 then ((f*f).c)*((g*h).c) <= (f.c)*((g*h).c) by AXIOMS:25;
 then ((f*g).c + (f*h).c ) - ((f*f).c)*((g*h).c) >=
 ((f*g).c + (f*h).c) - (f.c)*((g*h).c) by REAL_2:106;
 then ((f*g).c + (f*h).c ) - ((f*f)*(g*h)).c >=
 ((f*g).c + (f*h).c) - (f.c)*((g*h).c) by Def2;
 then ((f*g).c + (f*h).c ) - ((f*f)*(g*h)).c >=
 (x*y + (f*h).c) - (f.c)*((g*h).c) by Def2;
 then ((f*g).c + (f*h).c ) - ((f*f)*(g*h)).c >= x*y+x*z - (f.c)*((g*h).c) by
Def2;
 then (f*g).c + (f*h).c - ((f* (f*(g*h)))).c >= x*y+x*z - (f.c)*((g*h).c) by
Th67;
 then (f*g).c + (f*h).c - ((f*((f*g)*h))).c >= x*y + x*z - x*((g*h).c) by Th67
;
 then (f*g).c + (f*h).c - ((f*((f*g)*h))).c >= (y + z - (g*h).c)*x by XCMPLX_1:
43;
 then (f*g).c + (f*h).c - ((f*((g*f)*h))).c >= (y + z - (g*h).c)*x by Th65;
 then (f*g).c + (f*h).c - ((f*(g*(f*h)))).c >= (y + z - (g*h).c)*x by Th67;
 then (f*g).c + (f*h).c - (((f*g)*(f*h))).c >= (y + z - (g*h).c)*x by Th67;
 then (f*g).c + (f*h).c - (((f*g)*(f*h))).c >= x*(y + z - y*z) by Def2;
 then (f*g).c + (f*h).c - ((f*g).c)*((f*h).c) >= x*(y + z - y*z) by Def2;
 then ((f*g) ++(f*h)).c >= x*(y + z - y*z) by Def3;
 then ((f*g) ++(f*h)).c >= x*((g ++ h).c) by Def3;
 hence thesis by Def2;
end;

theorem
  A*(B ++ D) c= (A*B) ++ (A*D)
proof
   for c holds (f*(g ++ h)).c <= ((f*g) ++ (f*h)).c by Th73;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th75:
for c holds ((f ++ g)*(f ++ h)).c <= (f ++ (g*h)).c
proof
 let c;
 set x = f.c, y = g.c, z = h.c;
A1: ((f ++ g)*(f ++ h)).c - (f ++ (g*h)).c
  = ((f ++ g).c)*((f ++ h).c) - (f ++ (g*h)).c by Def2
 .= (x + y - x*y)*((f ++ h).c) - (f ++ (g*h)).c by Def3
 .= (x + y - x*y)*(x + z - x*z) - (f ++ (g*h)).c by Def3
 .= (x + y - x*y)*(x + z - x*z) - (x + (g*h).c - x*((g*h).c)) by Def3
 .= (x + y - x*y)*(x + z - x*z) - (x + y*z - x*((g*h).c)) by Def2
 .= (x + y - x*y)*(x + z - x*z) - (x + y*z - x*(y*z)) by Def2
 .= (x - x*y + y)*(x + z - x*z) - (x + y*z - (y*z)*x) by XCMPLX_1:29
 .= (x - x*y + y)*(x + z - x*z) - (x + y*z - y*(z*x)) by XCMPLX_1:4
 .= (x - x*y + y)*(x + (z - x*z)) - (x + y*z - y*(x*z)) by XCMPLX_1:29
 .= (x - x*y + y)*(x + (z - x*z)) - (x + (y*z - y*(x*z))) by XCMPLX_1:29
 .= (x - x*y + y)*(x + (z - x*z)) - (x + y*(z - x*z)) by XCMPLX_1:40
 .= (x-x*y)*x+(x-x*y)*(z-x*z)+y*x+y*(z-x*z)- (x + y*(z - x*z)) by XCMPLX_1:10

 .= (x - x*y)*x+(x-x*y)*(z-x*z)+y*x+y*(z - x*z) - x - y*(z - x*z) by XCMPLX_1:
36
 .= -y*(z-x*z)+(y*(z-x*z)+((x-x*y)*x+(x-x*y)*(z - x*z) + y*x))-x by XCMPLX_1:
159
 .= -y*(z-x*z)+y*(z-x*z)+((x-x*y)*x+ (x - x*y)*(z - x*z) + y*x)-x by XCMPLX_1:1
 .= 0 + ((x - x*y)*x + (x - x*y)*(z - x*z) + y*x)-x by XCMPLX_0:def 6
 .= (x - x*y)*x + (-x*y + x)*(z - x*z) + x*y-x*1 by XCMPLX_0:def 8
 .= (x - x*y)*x + ((z - x*z)*(-x*y) + (z - x*z)*x) + x*y-x*1 by XCMPLX_1:8
 .= (x*1 - x*y)*x + (z - x*z)*(-(x*y)) + (z - x*z)*x + x*y-x*1 by XCMPLX_1:1
 .= x*(1 - y)*x + ((z - x*z)*(-(x*y))) + (z - x*z)*x + x*y-x*1 by XCMPLX_1:40
 .= x*(1 - y)*x + -((z - x*z)*(x*y)) + (z - x*z)*x + x*y-x*1 by XCMPLX_1:175

 .= x*(1 - y)*x + -((z - x*z)*(x*y)) + (z*x - x*z*x) + x*y-x*1 by XCMPLX_1:40
 .= x*(1 - y)*x + -(z*(x*y) - x*z*(x*y)) + (z*x - x*z*x) + x*y-x*1 by XCMPLX_1:
40
 .= x*(1 - y)*x -(z*(x*y) - x*z*(x*y)) + (z*x - x*z*x) + x*y-x*1 by XCMPLX_0:
def 8
 .= (x*(1 - y)*x-(z*(x*y))+ (x*z*(x*y))) + (z*x - x*z*x) + x*y-x*1 by XCMPLX_1:
37
 .= ((1 - y)*x*x -(z*(x*y)) +(z*x*(x*y))) +z*x -x*z*x + x*y-x*1 by XCMPLX_1:29
 .= ((1 - y)*x*x -(z*(x*y)) +(z*x*(x*y))) -x*z*x +z*x+ x*y-x*1 by XCMPLX_1:29

 .= (-(z*(x*y))+(1 - y)*x*x +(z*x*(x*y))) -x*z*x+z*x+x*y-x*1 by XCMPLX_0:def 8
 .= (-(z*(x*y))+((1 - y)*x*x +(z*x*(x*y)))) -x*z*x +z*x+ x*y-x*1 by XCMPLX_1:1
 .= (-(z*(x*y))+((1 - y)*(x*x) +(z*x*(x*y)))) -x*z*x+z*x+ x*y-x*1 by XCMPLX_1:4
 .= (-(z*(x*y))+((1 - y)*(x*x) +z*x*x*y )) -x*z*x +z*x+ x*y-x*1 by XCMPLX_1:4
 .= (-(z*(x*y))+((1 - y)*(x*x)+y*(z*(x*x)))) -x*z*x+z*x+ x*y-x*1 by XCMPLX_1:4
 .= (-(z*(x*y))+((1 - y)*(x*x)+y*z*(x*x))) -x*z*x+z*x+ x*y-x*1 by XCMPLX_1:4
 .= (-(z*(x*y))+(1 - y+y*z)*(x*x) ) -x*z*x +z*x+ x*y-x*1 by XCMPLX_1:8
 .= (1 - y+y*z)*(x*x) -(z*x*x) -(x*y*z) +(z*x)+ (x*y)-x*1 by XCMPLX_1:159

 .= (1 - y+y*z)*(x*x) -z*(x*x) -(x*y*z) +(z*x)+ (x*y)-x*1 by XCMPLX_1:4
 .= (1 - y+y*z -z)*(x*x) -(x*y*z) +(z*x)+ (x*y)-x*1 by XCMPLX_1:40
 .= (z*x) -(x*y*z) +(1 - y+y*z -z)*(x*x)+ (x*y)-x*1 by XCMPLX_1:30
 .= (z*x) -x*(y*z) +(1 - y+y*z -z)*(x*x)+ (x*y)-x*1 by XCMPLX_1:4
 .= (z -y*z)*x +(1 - y+y*z -z)*(x*x)+ (x*y)-x*1 by XCMPLX_1:40
 .= x*(z -y*z) +(x*y)+(1 - y+y*z -z)*(x*x) -x*1 by XCMPLX_1:1
 .= x*(z -y*z +y)+(1 - y+y*z -z)*(x*x) -x*1 by XCMPLX_1:8
 .= x*(z -y*z +y)-x*1+(1 - y+y*z -z)*(x*x) by XCMPLX_1:29
 .= x*(z -y*z +y-1)+(1 - y+y*z -z)*(x*x) by XCMPLX_1:40
 .= x*(z -y*z +y-1)+( - y+y*z +1-z)*(x*x) by XCMPLX_1:156
 .= x*(z -y*z +y-1)+( - y+y*z -z +1)*(x*x) by XCMPLX_1:29
 .= x*(y +z -y*z -1)+( - y+y*z -z +1)*(x*x) by XCMPLX_1:29
 .= x*((g++h).c -1)+( - y+y*z -z +1)*(x*x) by Def3
 .= x*((g++h).c -1)+( - (y-y*z+z) +1)*(x*x) by XCMPLX_1:169
 .= x*((g++h).c -1)+( - (y+z-y*z) +1)*(x*x) by XCMPLX_1:29
 .= x*((g++h).c -1)+( - (g++h).c +1)*(x*x) by Def3
 .= x*(-(-(g++h).c +1))+( - (g++h).c +1)*(x*x) by XCMPLX_1:163
 .= (-(g++h).c +1)*(-x)+( - (g++h).c +1)*(x*x) by XCMPLX_1:176
 .= (-(g++h).c +1)*(-x+ x*x) by XCMPLX_1:8
 .= (1-(g++h).c)*(-x+ x*x) by XCMPLX_0:def 8
 .=((1_minus (g++h)).c)*(-x+ x*x) by FUZZY_1:def 7;
   (f*f).c <= f.c by Th63;
 then x*x <= x by Def2;
then A2:-x+ x*x <= 0 by REAL_2:106;
   0<=(1_minus (g++h)).c by Th1;
 then ((1_minus (g++h)).c)*(-x+ x*x) <= 0*(-x+ x*x) by A2,REAL_1:52;
 hence thesis by A1,SQUARE_1:11;
end;

theorem
  (A ++ B)*(A ++ D) c= A ++ (B*D)
proof
   for c holds ((f ++ g)*(f ++ h)).c <= (f ++ (g*h)).c by Th75;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th77:
1_minus (f*g) = (1_minus f) ++ (1_minus g)
proof
A1:C = dom 1_minus (f*g) &
   C = dom ((1_minus f) ++ (1_minus g)) by FUZZY_1:def 1;
   for c being Element of C st c in C holds
 (1_minus (f*g)).c = ((1_minus f) ++ (1_minus g)).c
 proof
  let c;
       ((1_minus f) ++ (1_minus g)).c
   = (1_minus f).c + (1_minus g).c - ((1_minus f).c)*((1_minus g).c) by Def3
  .= 1 - f.c + (1_minus g).c - ((1_minus f).c)*((1_minus g).c) by FUZZY_1:def 7
  .= 1 - f.c + (1- g.c) - ((1_minus f).c)*((1_minus g).c) by FUZZY_1:def 7
  .= 1 - f.c + (1- g.c) - (1 - f.c)*((1_minus g).c) by FUZZY_1:def 7
  .= 1 - f.c + (1- g.c) - (1 - f.c)*(1- g.c) by FUZZY_1:def 7
  .= 1 - f.c - (1- g.c)*(1 - f.c)+ (1- g.c) by XCMPLX_1:29
  .= 1 - f.c - ((1- f.c)*1 - (1- f.c)*g.c)+ (1- g.c) by XCMPLX_1:40
  .= (1- f.c)*g.c+ (1- g.c) by XCMPLX_1:18
  .= 1*g.c- f.c*g.c+ (1- g.c) by XCMPLX_1:40
  .= 1- g.c + g.c - f.c*g.c by XCMPLX_1:29
  .= g.c- g.c + 1 - f.c*g.c by XCMPLX_1:30
  .= 0 + 1 - f.c*g.c by XCMPLX_1:14
  .= 1 - (f*g).c by Def2;
  hence thesis by FUZZY_1:def 7;
 end;
 hence thesis by A1,PARTFUN1:34;
end;

theorem
  (A*B)` = A` ++ B`
proof
   1_minus (f*g) = (1_minus f) ++ (1_minus g) by Th77;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th79:
1_minus(f ++ g) = (1_minus f)*(1_minus g)
proof
A1:C = dom 1_minus(f ++ g) &
   C = dom ((1_minus f)*(1_minus g)) by FUZZY_1:def 1;
   for c being Element of C st c in C holds
 (1_minus(f ++ g)).c = ((1_minus f)*(1_minus g)).c
 proof
  let c;
       ((1_minus f)*(1_minus g)).c
   = ((1_minus f).c)*((1_minus g).c) by Def2
  .= (1 - f.c)*((1_minus g).c) by FUZZY_1:def 7
  .= (1 - f.c)*(1- g.c) by FUZZY_1:def 7
  .= (1 - f.c)*1- (1 - f.c)*g.c by XCMPLX_1:40
  .= 1 - f.c- (1*g.c - f.c*g.c) by XCMPLX_1:40
  .= 1 - (f.c+ (1*g.c - f.c*g.c)) by XCMPLX_1:36
  .= 1 - (f.c+ g.c - f.c*g.c) by XCMPLX_1:29
  .= 1 - (f ++ g).c by Def3;
  hence thesis by FUZZY_1:def 7;
 end;
 hence thesis by A1,PARTFUN1:34;
end;

theorem
  (A ++B)` = (A`)*(B`)
proof
   1_minus(f ++ g) = (1_minus f)*(1_minus g) by Th79;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th81:
f ++ g = 1_minus((1_minus f)*(1_minus g))
proof
A1:C = dom (f ++ g) &
   C = dom 1_minus((1_minus f)*(1_minus g)) by FUZZY_1:def 1;
   for c being Element of C st c in C holds
 (f ++ g).c = (1_minus((1_minus f)*(1_minus g))).c
 proof
  let c;
       (1_minus((1_minus f)*(1_minus g))).c
   = 1 - ((1_minus f)*(1_minus g)).c by FUZZY_1:def 7
  .= 1 - ((1_minus f).c)*((1_minus g).c) by Def2
  .= 1 - (1 - f.c)*((1_minus g).c) by FUZZY_1:def 7
  .= 1 - (1 - f.c)*(1 - g.c) by FUZZY_1:def 7
  .= 1 - ((1 - f.c)*1 - (1 - f.c)*g.c) by XCMPLX_1:40
  .= 1 - ((1 - f.c) - (1*g.c - f.c*g.c)) by XCMPLX_1:40
  .= 1 - (1 - f.c) + (1*g.c - f.c*g.c) by XCMPLX_1:37
  .= 1 - 1 + f.c + (1*g.c - f.c*g.c) by XCMPLX_1:37
  .= f.c + g.c - f.c*g.c by XCMPLX_1:29;
  hence thesis by Def3;
 end;
 hence thesis by A1,PARTFUN1:34;
end;

theorem
  A ++ B = (A`*B`)`
proof
   f ++ g = 1_minus((1_minus f)*(1_minus g)) by Th81;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th83:
f*(EMF(C)) = EMF(C) & f*(UMF(C)) = f
proof
A1:f*(EMF(C)) = EMF(C)
 proof
  A2:C = dom EMF(C) & C = dom (f*EMF(C)) by FUZZY_1:def 1;
    for c being Element of C st c in C holds (f*(EMF(C))).c = (EMF(C)).c
  proof
   let c;
     (f*EMF(C)).c = (f.c)*((EMF(C)).c) by Def2
               .= (f.c)*0 by Th2;
   hence thesis by Th2;
  end;
 hence thesis by A2,PARTFUN1:34;
 end;
   f*(UMF(C)) = f
 proof
A3:C = dom f & C = dom (f*UMF(C)) by FUZZY_1:def 1;
    for c being Element of C st c in C holds (f*(UMF(C))).c = f.c
  proof
   let c;
     (f*(UMF(C))).c = (f.c)*((UMF(C)).c) by Def2
                 .= (f.c)*1 by Th2;
   hence thesis;
  end;
  hence thesis by A3,PARTFUN1:34;
 end;
 hence thesis by A1;
end;

theorem
  A*E = E & A*X = A
proof
   f*(EMF(C)) = EMF(C) & f*(UMF(C)) = f by Th83;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th85:
f ++ EMF(C) = f & f ++ UMF(C) = UMF(C)
proof
A1:f ++ EMF(C) = f
 proof
  A2:C = dom f & C = dom (f ++ EMF(C)) by FUZZY_1:def 1;
    for c being Element of C st c in C holds (f ++ EMF(C)).c = f.c
  proof
   let c;
     (f ++ EMF(C)).c = f.c + (EMF(C)).c - (f.c)*((EMF(C)).c) by Def3
                  .= f.c + 0 - (f.c)*((EMF(C)).c) by Th2
                  .= f.c - (f.c)*0 by Th2;
   hence thesis;
  end;
 hence thesis by A2,PARTFUN1:34;
 end;
   f ++ UMF(C) = UMF(C)
 proof
A3:C = dom UMF(C) & C = dom (f ++ UMF(C)) by FUZZY_1:def 1;
    for c being Element of C st c in C holds (f ++ UMF(C)).c = (UMF(C)).c
  proof
   let c;
     (f ++ UMF(C)).c = f.c + (UMF(C)).c - (f.c)*((UMF(C)).c) by Def3
                  .= (UMF(C)).c+f.c - (f.c)*1 by Th2
                  .= (UMF(C)).c + (f.c - f.c) by XCMPLX_1:29;
   hence thesis by XCMPLX_1:25;
  end;
  hence thesis by A3,PARTFUN1:34;
 end;
 hence thesis by A1;
end;

theorem
  A ++ E = A & A ++ X = X
proof
   f ++ EMF(C) = f & f ++ UMF(C) = UMF(C) by Th85;
 hence thesis by FUZZY_1:def 3;
end;

canceled 2;

theorem
  E c= A*A` & A ++ A` c= X
proof
   (for c holds (EMF(C)).c <= (f*(1_minus f)).c) &
 (for c holds (UMF(C)).c >= (f ++ (1_minus f)).c) by FUZZY_1:31;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th90:
for c holds (f*g).c <= min(f,g).c
proof
 let c;
A1:min(f,g).c = min(f.c,g.c) by FUZZY_1:6;
   now per cases by A1,SQUARE_1:38;
  suppose A2:min(f,g).c = f.c;
    (f*g).c <= min(f,g).c
  proof
     g.c <= 1 & f.c >= 0 by Th1;
   then (g.c)*(f.c) <= 1*(f.c) by AXIOMS:25;
   hence thesis by A2,Def2;
  end;
  hence thesis;
  suppose A3:min(f,g).c = g.c;
    (f*g).c <= min(f,g).c
  proof
     f.c <= 1 & g.c >= 0 by Th1;
   then (f.c)*(g.c) <= 1*(g.c) by AXIOMS:25;
   hence thesis by A3,Def2;
  end;
  hence thesis;
 end;
 hence thesis;
end;

theorem
  A*B c= A /\ B
proof
   for c holds (f*g).c <= min(f,g).c by Th90;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th92:
for c holds max(f,g).c <= (f ++ g).c
proof
 let c;
A1:max(f,g).c = max(f.c,g.c) by FUZZY_1:6;
   now per cases by A1,SQUARE_1:49;
  suppose A2:max(f,g).c = f.c;
    (f ++ g).c >= max(f,g).c
  proof
     g.c >= 0 & (1_minus f).c >= 0 by Th1;
   then 0*(g.c) <= (g.c)*((1_minus f).c) by AXIOMS:25;
   then 0 <= (g.c)*(1 - f.c) by FUZZY_1:def 7;
   then 0 <= (g.c)*1 - (g.c)*(f.c) by XCMPLX_1:40;
   then 0 + f.c <= g.c - (f.c)*(g.c) + f.c by AXIOMS:24;
   then f.c <= f.c + g.c - (f.c)*(g.c) by XCMPLX_1:29;
   hence thesis by A2,Def3;
  end;
  hence thesis;
  suppose A3:max(f,g).c = g.c;
    (f ++ g).c >= max(f,g).c
  proof
     f.c >= 0 & (1_minus g).c >= 0 by Th1;
   then 0*(f.c) <= (f.c)*((1_minus g).c) by AXIOMS:25;
   then 0 <= (f.c)*(1 - g.c) by FUZZY_1:def 7;
   then 0 <= (f.c)*1 - (f.c)*(g.c) by XCMPLX_1:40;
   then 0 + g.c <= f.c - (f.c)*(g.c) + g.c by AXIOMS:24;
   then g.c <= f.c + g.c - (f.c)*(g.c) by XCMPLX_1:29;
   hence thesis by A3,Def3;
  end;
  hence thesis;
 end;
 hence thesis;
end;

theorem
  A \/ B c= A ++ B
proof
   for c holds max(f,g).c <= (f ++ g).c by Th92;
 hence thesis by FUZZY_1:def 4;
end;

Lm1:
for a,b,c be Real st 0 <= c holds c*min(a,b) = min(c*a,c*b)
proof
 let a,b,c be Element of REAL;
 assume A1:0 <= c;
   now per cases by SQUARE_1:38;
  suppose A2:min(a,b) = a;
    c*min(a,b) = min(c*a,c*b)
  proof
     a <= b by A2,SQUARE_1:def 1;
   then a*c <= b*c by A1,AXIOMS:25;
   hence thesis by A2,SQUARE_1:def 1;
  end;
  hence thesis;
  suppose A3:min(a,b) = b;
    c*min(a,b) = min(c*a,c*b)
  proof
     a >= b by A3,SQUARE_1:def 1;
   then a*c >= b*c by A1,AXIOMS:25;
   hence thesis by A3,SQUARE_1:def 1;
  end;
  hence thesis;
 end;
 hence thesis;
end;

Lm2:
for a,b,c be Real st 0 <= c holds c*max(a,b) = max(c*a,c*b)
proof
 let a,b,c be Element of REAL;
 assume A1:0 <= c;
   now per cases by SQUARE_1:49;
  suppose A2:max(a,b) = b;
    c*max(a,b) = max(c*a,c*b)
  proof
     a <= b by A2,SQUARE_1:def 2;
   then a*c <= c*b by A1,AXIOMS:25;
   hence thesis by A2,SQUARE_1:def 2;
  end;
  hence thesis;
  suppose A3:max(a,b) = a;
    c*max(a,b) = max(c*a,c*b)
  proof
     a >= b by A3,SQUARE_1:def 2;
   then a*c >= b*c by A1,AXIOMS:25;
   hence thesis by A3,SQUARE_1:def 2;
  end;
  hence thesis;
 end;
 hence thesis;
end;

theorem
  for a,b,c be Real st 0 <= c holds
c*max(a,b) = max(c*a,c*b) & c*min(a,b) = min(c*a,c*b) by Lm1,Lm2;

theorem
  for a,b,c be Real holds
c + max(a,b) = max(c+a,c+b) & c + min(a,b) = min(c+a,c+b)
proof
 let a,b,c be Element of REAL;
A1: c + max(a,b) = max(c+a,c+b)
 proof
    now per cases by SQUARE_1:49;
   suppose A2:max(a,b) = b;
     c + max(a,b) = max(c+a,c+b)
   proof
      a <= b by A2,SQUARE_1:def 2;
    then c+a <= c+b by AXIOMS:24;
    hence thesis by A2,SQUARE_1:def 2;
   end;
   hence thesis;
   suppose A3:max(a,b) = a;
     c + max(a,b) = max(c+a,c+b)
   proof
      a >= b by A3,SQUARE_1:def 2;
    then a+c >= b+c by AXIOMS:24;
    hence thesis by A3,SQUARE_1:def 2;
   end;
   hence thesis;
  end;
  hence thesis;
 end;
   c + min(a,b) = min(c+a,c+b)
 proof
    now per cases by SQUARE_1:38;
   suppose A4:min(a,b) = a;
     c + min(a,b) = min(c+a,c+b)
   proof
      a <= b by A4,SQUARE_1:def 1;
    then a+c <= c+b by AXIOMS:24;
    hence thesis by A4,SQUARE_1:def 1;
   end;
   hence thesis;
   suppose A5:min(a,b) = b;
     c + min(a,b) = min(c+a,c+b)
   proof
      a >= b by A5,SQUARE_1:def 1;
    then a+c >= b+c by AXIOMS:24;
    hence thesis by A5,SQUARE_1:def 1;
   end;
   hence thesis;
  end;
  hence thesis;
 end;
 hence thesis by A1;
end;

theorem Th96:
f*max(g,h) = max(f*g,f*h)
proof
A1:C = dom (f*max(g,h)) & C = dom max(f*g,f*h) by FUZZY_1:def 1;
   for c being Element of C st c in C holds (f*max(g,h)).c = max(f*g,f*h).c
 proof
  let c;
A2:f.c >= 0 by Th1;
    (f*max(g,h)).c = (f.c)*(max(g,h).c) by Def2
                .= (f.c)*max(g.c,h.c) by FUZZY_1:6
                .= max((f.c)*g.c,(f.c)*(h.c)) by A2,Lm2
                .= max((f*g).c,(f.c)*(h.c)) by Def2
                .= max((f*g).c,(f*h).c) by Def2;
  hence thesis by FUZZY_1:6;
 end;
 hence thesis by A1,PARTFUN1:34;
end;

theorem Th97:
f*min(g,h) = min(f*g,f*h)
proof
A1:C = dom (f*min(g,h)) & C = dom min(f*g,f*h) by FUZZY_1:def 1;
   for c being Element of C st c in C holds (f*min(g,h)).c = min(f*g,f*h).c
 proof
  let c;
A2:f.c >= 0 by Th1;
    (f*min(g,h)).c = (f.c)*(min(g,h).c) by Def2
                .= (f.c)*min(g.c,h.c) by FUZZY_1:6
                .= min((f.c)*g.c,(f.c)*(h.c)) by A2,Lm1
                .= min((f*g).c,(f.c)*(h.c)) by Def2
                .= min((f*g).c,(f*h).c) by Def2;
  hence thesis by FUZZY_1:6;
 end;
 hence thesis by A1,PARTFUN1:34;
end;

theorem
  A*(B /\ D) = (A*B) /\ (A*D) & A*(B \/ D) = (A*B) \/ (A*D)
proof
   f*max(g,h) = max(f*g,f*h) & f*min(g,h) = min(f*g,f*h) by Th96,Th97;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th99:
f ++ max(g,h) = max((f ++ g),(f ++ h))
proof
A1:C = dom (f ++ max(g,h)) & C = dom max((f ++ g),(f ++ h)) by FUZZY_1:def 1;
   for c being Element of C st c in C holds
 (f ++ max(g,h)).c = (max((f ++ g),(f ++ h))).c
 proof
  let c;
A2:(f ++ max(g,h)).c = f.c + max(g,h).c - (f.c)*(max(g,h).c) by Def3
                    .= f.c + max(g.c,h.c) - (f.c)*(max(g,h).c) by FUZZY_1:6;
    now per cases by SQUARE_1:49;
   suppose A3:max(g.c,h.c) = g.c;
     (f ++ max(g,h)).c = (max((f ++ g),(f ++ h))).c
   proof
      g.c >= h.c & (1_minus f).c >= 0 by A3,Th1,SQUARE_1:def 2;
    then (g.c)*((1_minus f).c) >= (h.c)*((1_minus f).c) by AXIOMS:25;
    then (g.c)*(1- f.c) >= (h.c)*((1_minus f).c) by FUZZY_1:def 7;
    then (g.c)*(1- f.c) >= (h.c)*(1- f.c) by FUZZY_1:def 7;
    then (g.c)*(1- f.c) + f.c >= (h.c)*(1- f.c) + f.c by AXIOMS:24;
    then (g.c)*1- (g.c)*f.c + f.c >= (h.c)*(1- f.c) + f.c by XCMPLX_1:40;
    then (g.c)- (g.c)*f.c + f.c >= (h.c)*1- (h.c)*(f.c) + f.c by XCMPLX_1:40;
    then f.c + g.c - (g.c)*f.c >= (h.c)*1- (h.c)*(f.c) + f.c by XCMPLX_1:29
;
then A4: f.c + g.c - (g.c)*f.c >= f.c + h.c - (h.c)*(f.c) by XCMPLX_1:29;
A5: (f ++ max(g,h)).c = f.c + g.c - (f.c)*g.c by A2,A3,FUZZY_1:6;

         f.c + g.c - (f.c)*g.c
     = max((f.c + g.c - (f.c)*g.c),(f.c + h.c - (f.c)*(h.c)))
                                                       by A4,SQUARE_1:def 2
    .= max((f ++ g).c,(f.c + h.c - (f.c)*(h.c))) by Def3
    .= max((f ++ g).c,(f ++ h).c) by Def3;
    hence thesis by A5,FUZZY_1:6;
   end;
   hence thesis;
   suppose A6:max(g.c,h.c) = h.c;
     (f ++ max(g,h)).c = (max((f ++ g),(f ++ h))).c
   proof
      h.c >= g.c & (1_minus f).c >= 0 by A6,Th1,SQUARE_1:def 2;
    then (h.c)*((1_minus f).c) >= (g.c)*((1_minus f).c) by AXIOMS:25;
    then (h.c)*(1- f.c) >= (g.c)*((1_minus f).c) by FUZZY_1:def 7;
    then (h.c)*(1- f.c) >= (g.c)*(1- f.c) by FUZZY_1:def 7;
    then (h.c)*(1- f.c) + f.c >= (g.c)*(1- f.c) + f.c by AXIOMS:24;
    then (h.c)*1- (h.c)*f.c + f.c >= (g.c)*(1- f.c) + f.c by XCMPLX_1:40;
    then (h.c)- (h.c)*f.c + f.c >= (g.c)*1- (g.c)*(f.c) + f.c by XCMPLX_1:40;
    then f.c + h.c - (h.c)*f.c >= (g.c)*1- (g.c)*(f.c) + f.c by XCMPLX_1:29
;
then A7: f.c + h.c - (h.c)*f.c >= f.c + g.c - (g.c)*(f.c) by XCMPLX_1:29;
A8: (f ++ max(g,h)).c = f.c + h.c - (f.c)*h.c by A2,A6,FUZZY_1:6;
         f.c + h.c - (f.c)*h.c
     = max((f.c + g.c - (f.c)*g.c),(f.c + h.c - (f.c)*(h.c)))
                                                       by A7,SQUARE_1:def 2
    .= max((f ++ g).c,(f.c + h.c - (f.c)*(h.c))) by Def3
    .= max((f ++ g).c,(f ++ h).c) by Def3;
    hence thesis by A8,FUZZY_1:6;
   end;
   hence thesis;
  end;
  hence thesis;
 end;
 hence thesis by A1,PARTFUN1:34;
end;

theorem Th100:
f ++ min(g,h) = min((f ++ g),(f ++ h))
proof
A1:C = dom (f ++ min(g,h)) & C = dom min((f ++ g),(f ++ h)) by FUZZY_1:def 1;
   for c being Element of C st c in C holds
 (f ++ min(g,h)).c = (min((f ++ g),(f ++ h))).c
 proof
  let c;
A2:(f ++ min(g,h)).c = f.c + min(g,h).c - (f.c)*(min(g,h).c) by Def3
                    .= f.c + min(g.c,h.c) - (f.c)*(min(g,h).c) by FUZZY_1:6;
    now per cases by SQUARE_1:38;
   suppose A3:min(g.c,h.c) = g.c;
     (f ++ min(g,h)).c = (min((f ++ g),(f ++ h))).c
   proof
      g.c <= h.c & (1_minus f).c >= 0 by A3,Th1,SQUARE_1:def 1;
    then (g.c)*((1_minus f).c) <= (h.c)*((1_minus f).c) by AXIOMS:25;
    then (g.c)*(1- f.c) <= (h.c)*((1_minus f).c) by FUZZY_1:def 7;
    then (g.c)*(1- f.c) <= (h.c)*(1- f.c) by FUZZY_1:def 7;
    then (g.c)*(1- f.c) + f.c <= (h.c)*(1- f.c) + f.c by AXIOMS:24;
    then (g.c)*1- (g.c)*f.c + f.c <= (h.c)*(1- f.c) + f.c by XCMPLX_1:40;
    then (g.c)- (g.c)*f.c + f.c <= (h.c)*1- (h.c)*(f.c) + f.c by XCMPLX_1:40;
    then f.c + g.c - (g.c)*f.c <= (h.c)*1- (h.c)*(f.c) + f.c by XCMPLX_1:29
;
then A4:f.c + g.c - (g.c)*f.c <= f.c + h.c - (h.c)*(f.c) by XCMPLX_1:29;
A5:(f ++ min(g,h)).c = f.c + g.c - (f.c)*g.c by A2,A3,FUZZY_1:6;
         f.c + g.c - (f.c)*g.c
    = min((f.c + g.c - (f.c)*g.c),(f.c + h.c - (f.c)*(h.c)))
                                                       by A4,SQUARE_1:def 1
    .= min((f ++ g).c,(f.c + h.c - (f.c)*(h.c))) by Def3
    .= min((f ++ g).c,(f ++ h).c) by Def3;
    hence thesis by A5,FUZZY_1:6;
   end;
   hence thesis;
   suppose A6:min(g.c,h.c) = h.c;
     (f ++ min(g,h)).c = (min((f ++ g),(f ++ h))).c
   proof
      h.c <= g.c & (1_minus f).c >= 0 by A6,Th1,SQUARE_1:def 1;
    then (h.c)*((1_minus f).c) <= (g.c)*((1_minus f).c) by AXIOMS:25;
    then (h.c)*(1- f.c) <= (g.c)*((1_minus f).c) by FUZZY_1:def 7;
    then (h.c)*(1- f.c) <= (g.c)*(1- f.c) by FUZZY_1:def 7;
    then (h.c)*(1- f.c) + f.c <= (g.c)*(1- f.c) + f.c by AXIOMS:24;
    then (h.c)*1- (h.c)*f.c + f.c <= (g.c)*(1- f.c) + f.c by XCMPLX_1:40;
    then (h.c)- (h.c)*f.c + f.c <= (g.c)*1- (g.c)*(f.c) + f.c by XCMPLX_1:40;
    then f.c + h.c - (h.c)*f.c <= (g.c)*1- (g.c)*(f.c) + f.c by XCMPLX_1:29
;
then A7:f.c + h.c - (h.c)*f.c <= f.c + g.c - (g.c)*(f.c) by XCMPLX_1:29;
A8:(f ++ min(g,h)).c = f.c + h.c - (f.c)*h.c by A2,A6,FUZZY_1:6;
         f.c + h.c - (f.c)*h.c
     = min((f.c + g.c - (f.c)*g.c),(f.c + h.c - (f.c)*(h.c)))
                                                       by A7,SQUARE_1:def 1
    .= min((f ++ g).c,(f.c + h.c - (f.c)*(h.c))) by Def3
    .= min((f ++ g).c,(f ++ h).c) by Def3;
    hence thesis by A8,FUZZY_1:6;
   end;
   hence thesis;
  end;
  hence thesis;
 end;
 hence thesis by A1,PARTFUN1:34;
end;

theorem
  A ++ (B \/ D) = (A ++ B) \/ (A ++ D) & A ++ (B /\ D) = (A ++ B) /\ (A ++ D)
proof
   f ++ max(g,h) = max((f ++ g),(f ++ h)) &
 f ++ min(g,h) = min((f ++ g),(f ++ h)) by Th99,Th100;
 hence thesis by FUZZY_1:def 3;
end;

theorem Th102:
for c holds (max(f,g)*max(f,h)).c <= max(f,(g*h)).c
proof
 let c;
A1:(max(f,g)*max(f,h)).c = (max(f,g).c)*(max(f,h).c) by Def2
                      .= max(f.c,g.c)*(max(f,h).c) by FUZZY_1:6
                      .= max(f.c,g.c)*max(f.c,h.c) by FUZZY_1:6;
   max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
 proof
   now per cases by SQUARE_1:49;
  suppose A2:max(f.c,g.c) = f.c;
    max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
  proof
     now per cases by SQUARE_1:49;
    suppose A3:max(f.c,h.c) = f.c;
      max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
    proof
       max(f,(g*h)).c = max(f.c,(g*h).c) by FUZZY_1:6;
then A4:  max(f,(g*h)).c >= f.c by SQUARE_1:46;
       (f*f).c <= f.c by Th63;
     then (f*f).c <= max(f,(g*h)).c by A4,AXIOMS:22;
     hence thesis by A2,A3,Def2;
    end;
    hence thesis;
    suppose A5:max(f.c,h.c) = h.c;
      max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
    proof
       f.c >= 0 & 1 >= h.c by Th1;
then A6:  (f.c)*(h.c) <= (f.c)*1 by AXIOMS:25;
       f.c <= max(f.c,(g*h).c) by SQUARE_1:46;
     then f.c <= max(f,(g*h)).c by FUZZY_1:6;
     hence thesis by A2,A5,A6,AXIOMS:22;
    end;
    hence thesis;
   end;
   hence thesis;
  end;
  hence thesis;
  suppose A7:max(f.c,g.c) = g.c;
    max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
  proof
     now per cases by SQUARE_1:49;
    suppose A8:max(f.c,h.c) = f.c;
      max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
    proof
       f.c >= 0 & 1 >= g.c by Th1;
then A9:  (f.c)*(g.c) <= (f.c)*1 by AXIOMS:25;
       f.c <= max(f.c,(g*h).c) by SQUARE_1:46;
     then f.c <= max(f,(g*h)).c by FUZZY_1:6;
     hence thesis by A7,A8,A9,AXIOMS:22;
    end;
    hence thesis;
    suppose A10:max(f.c,h.c) = h.c;
      max(f.c,g.c)*max(f.c,h.c) <= max(f,(g*h)).c
    proof
       max(f,(g*h)).c = max(f.c,(g*h).c) by FUZZY_1:6;
     then max(f,(g*h)).c >= (g*h).c by SQUARE_1:46;
     hence thesis by A7,A10,Def2;
    end;
    hence thesis;
   end;
   hence thesis;
  end;
  hence thesis;
 end;
 hence thesis;
 end;
 hence thesis by A1;
end;

theorem Th103:
for c holds (min(f,g)*min(f,h)).c <= min(f,(g*h)).c
proof
 let c;
A1:(min(f,g)*min(f,h)).c = (min(f,g).c)*(min(f,h).c) by Def2
                      .= min(f.c,g.c)*(min(f,h).c) by FUZZY_1:6
                      .= min(f.c,g.c)*min(f.c,h.c) by FUZZY_1:6;
   min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
 proof
   now per cases by SQUARE_1:38;
  suppose A2:min(f.c,g.c) = f.c;
    min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
  proof
     now per cases by SQUARE_1:38;
    suppose A3:min(f.c,h.c) = f.c;
      min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
    proof
A4:  f.c <= g.c & f.c <= h.c by A2,A3,SQUARE_1:def 1;
       0 <= g.c & 0 <= f.c by Th1;
     then (f.c)*(f.c) <= (g.c)*(f.c) & (g.c)*(f.c) <= (h.c)*(g.c) by A4,AXIOMS:
25;
     then A5:(f.c)*(f.c) <= (g.c)*(h.c) by AXIOMS:22;
       (f*f).c <= f.c by Th63;
     then min((f*f).c,(f.c)*(f.c)) <= min(f.c,(g.c)*(h.c)) by A5,FUZZY_1:44;
     then min((f.c)*(f.c),(f.c)*(f.c)) <= min(f.c,(g.c)*(h.c)) by Def2;
     then (f.c)*(f.c) <= min(f.c,(g*h).c) by Def2;
     hence thesis by A2,A3,FUZZY_1:6;
    end;
    hence thesis;
    suppose A6:min(f.c,h.c) = h.c;
      min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
    proof
       f.c >= 0 & 1 >= h.c & f.c <= g.c & h.c >= 0 by A2,Th1,SQUARE_1:def 1;
     then (f.c)*(h.c) <= (f.c)*1 & (f.c)*(h.c) <= (g.c)*(h.c) by AXIOMS:25;
     then (f.c)*(h.c) <= min((f.c),(g.c)*(h.c)) by SQUARE_1:39;
     then (f.c)*(h.c) <= min(f.c,(g*h).c) by Def2;
     hence thesis by A2,A6,FUZZY_1:6;
    end;
    hence thesis;
   end;
   hence thesis;
  end;
  hence thesis;
  suppose A7:min(f.c,g.c) = g.c;
    min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
  proof
     now per cases by SQUARE_1:38;
    suppose A8:min(f.c,h.c) = f.c;
      min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
    proof
       f.c >= 0 & 1 >= g.c & f.c <= h.c & g.c >= 0 by A8,Th1,SQUARE_1:def 1;
     then (g.c)*(f.c) <= (f.c)*1 & (f.c)*(g.c) <= (h.c)*(g.c) by AXIOMS:25;
     then (f.c)*(g.c) <= min((f.c),(h.c)*(g.c)) by SQUARE_1:39;
     then (f.c)*(g.c) <= min(f.c,(g*h).c) by Def2;
     hence thesis by A7,A8,FUZZY_1:6;
    end;
    hence thesis;
    suppose A9:min(f.c,h.c) = h.c;
      min(f.c,g.c)*min(f.c,h.c) <= min(f,(g*h)).c
    proof
       g.c >= 0 & h.c <= f.c & f.c >= 0 & g.c <= f.c & (f*f).c <= f.c
                                        by A7,A9,Th1,Th63,SQUARE_1:def 1;
     then (h.c)*(g.c) <= (f.c)*(g.c) & (g.c)*(f.c) <= (f.c)*(f.c) &
     (f.c)*(f.c) <= f.c by Def2,AXIOMS:25;
     then (h.c)*(g.c) <= (f.c)*(f.c) & (f.c)*(f.c) <= f.c by AXIOMS:22;
     then (h.c)*(g.c) <= f.c by AXIOMS:22;
     then (h.c)*(g.c) <= min(f.c,(h.c)*(g.c)) by SQUARE_1:39;
     then (g.c)*(h.c) <= min(f.c,(g*h).c) by Def2;
     hence thesis by A7,A9,FUZZY_1:6;
    end;
    hence thesis;
   end;
   hence thesis;
  end;
  hence thesis;
 end;
 hence thesis;
 end;
 hence thesis by A1;
end;

theorem
  (A \/ B)*(A \/ D) c= A \/ (B*D) & (A /\ B)*(A /\ D) c= A /\ (B*D)
proof
   (for c holds (min(f,g)*min(f,h)).c <= min(f,(g*h)).c) &
 (for c holds (max(f,g)*max(f,h)).c <= max(f,(g*h)).c) by Th102,Th103;
 hence thesis by FUZZY_1:def 4;
end;

theorem Th105:
for c be Element of C,f,g be Membership_Func of C holds
(f ++ g).c = 1 - ((1 - f.c)*(1 - g.c))
proof
 let c;
 let g,h be Membership_Func of C;
      (g ++ h).c = (1_minus((1_minus g)*(1_minus h))).c by Th81
 .= 1-((1_minus g)*(1_minus h)).c by FUZZY_1:def 7
 .= 1-((1_minus g).c)*((1_minus h).c) by Def2
 .= 1-((1-g.c)*((1_minus h).c)) by FUZZY_1:def 7;
 hence thesis by FUZZY_1:def 7;
end;

theorem Th106:
for c holds max(f,g ++ h).c <= (max(f,g) ++ max(f,h)).c
proof
 let c;
A1: max(f,g ++ h).c = max(f.c,(g ++ h).c) by FUZZY_1:6
 .= max(f.c,1 - ((1 - g.c)*(1 - h.c))) by Th105;
A2: (max(f,g) ++ max(f,h)).c
  = max(f,g).c + max(f,h).c - (max(f,g).c)*(max(f,h).c) by Def3
 .= max(f.c,g.c) + max(f,h).c - (max(f,g).c)*(max(f,h).c) by FUZZY_1:6
 .= max(f.c,g.c) + max(f.c,h.c) - (max(f,g).c)*(max(f,h).c) by FUZZY_1:6
 .= max(f.c,g.c) + max(f.c,h.c) - (max(f.c,g.c))*(max(f,h).c) by FUZZY_1:6
 .= max(f.c,g.c) + max(f.c,h.c) - (max(f.c,g.c))*(max(f.c,h.c)) by FUZZY_1:6;
   max(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
 max(f.c,g.c) + max(f.c,h.c) - (max(f.c,g.c))*(max(f.c,h.c))
 proof
    now per cases by SQUARE_1:49;
   suppose A3:max(f.c,g.c) = f.c & max(f.c,h.c) = f.c;
     max(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
   max(f.c,g.c) + max(f.c,h.c) - (max(f.c,g.c))*(max(f.c,h.c))
   proof
      g.c <= f.c & h.c <= f.c &
    (1_minus f).c >= 0 & (1_minus g).c >= 0 by A3,Th1,SQUARE_1:def 2;
    then 1 - g.c >= 1 - f.c & 1 - h.c >= 1 - f.c &
    1-f.c >= 0 & 1-g.c >= 0 by FUZZY_1:def 7,REAL_2:106;
    then (1 - f.c)*(1 - f.c) <= (1 - g.c)*(1 - f.c) &
    (1 - g.c)*(1 - f.c) <= (1 - g.c)*(1 - h.c) by AXIOMS:25;
    then (1 - f.c)*(1 - f.c) <= (1 - g.c)*(1 - h.c) by AXIOMS:22;
    then 1 - (1 - f.c)*(1 - f.c) >= 1 - (1 - g.c)*(1 - h.c) by REAL_2:106;
    then (f ++ f).c >= 1 - (1 - g.c)*(1 - h.c) by Th105;
then A4:f.c + f.c - (f.c)*(f.c) >= 1 - (1 - g.c)*(1 - h.c) by Def3;
      (f ++ f).c >= f.c by Th63;
    then f.c + f.c - (f.c)*(f.c) >= f.c by Def3;
    hence thesis by A3,A4,SQUARE_1:50;
   end;
   hence thesis;
   suppose A5:max(f.c,g.c) = f.c & max(f.c,h.c) = h.c;
     max(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
   max(f.c,g.c) + max(f.c,h.c) - (max(f.c,g.c))*(max(f.c,h.c))
   proof
      g.c <= f.c & (1_minus h).c >= 0 & (1_minus f).c >= 0 & h.c >= 0
                                         by A5,Th1,SQUARE_1:def 2;
    then 1 - f.c <= 1 - g.c & 1 - h.c >= 0 & 1 - f.c >= 0 & h.c >= 0
    by FUZZY_1:def 7,REAL_2:106;
    then (1 - f.c)*(1 -h.c) <= (1 - g.c)*(1 -h.c) & 0*(h.c) <= (h.c)*(1-f.c)
    by AXIOMS:25;
    then 1-(1 - f.c)*(1 -h.c) >= 1-(1 - g.c)*(1 -h.c) &
    0 + f.c <= (h.c)*(1-f.c) + f.c by AXIOMS:24,REAL_2:106;
    then (f ++ h).c >= 1-(1 - g.c)*(1 -h.c) & f.c <= (h.c)*1-(h.c)*(f.c) + f.c
    by Th105,XCMPLX_1:40;
    then f.c + h.c -(f.c)*(h.c) >= 1-(1 - g.c)*(1 -h.c) &
    f.c <= f.c + h.c -(h.c)*(f.c) by Def3,XCMPLX_1:29;
    hence thesis by A5,SQUARE_1:50;
   end;
   hence thesis;
   suppose A6:max(f.c,g.c) = g.c & max(f.c,h.c) = f.c;
     max(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
   max(f.c,g.c) + max(f.c,h.c) - (max(f.c,g.c))*(max(f.c,h.c))
   proof
      h.c <= f.c & (1_minus g).c >= 0 & (1_minus f).c >= 0 & g.c >= 0
                                         by A6,Th1,SQUARE_1:def 2;
    then 1 - f.c <= 1 - h.c & 1 - g.c >= 0 & 1 - f.c >= 0 & g.c >= 0
    by FUZZY_1:def 7,REAL_2:106;
    then (1 - f.c)*(1 -g.c) <= (1 - h.c)*(1 -g.c) & 0*(g.c) <= (g.c)*(1-f.c)
    by AXIOMS:25;
    then 1-(1 - f.c)*(1 -g.c) >= 1-(1 - h.c)*(1 - g.c) &
    0 + f.c <= (g.c)*(1-f.c) + f.c by AXIOMS:24,REAL_2:106;
    then (f ++ g).c >= 1-(1 - h.c)*(1 -g.c) & f.c <= (g.c)*1-(g.c)*(f.c) + f.c
    by Th105,XCMPLX_1:40;
    then f.c + g.c -(f.c)*(g.c) >= 1-(1 - h.c)*(1 -g.c) &
    f.c <= f.c + g.c -(g.c)*(f.c) by Def3,XCMPLX_1:29;
    hence thesis by A6,SQUARE_1:50;
   end;
   hence thesis;
   suppose A7:max(f.c,g.c) = g.c & max(f.c,h.c) = h.c;
     max(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
   max(f.c,g.c) + max(f.c,h.c) - (max(f.c,g.c))*(max(f.c,h.c))
   proof
      g.c >= f.c & h.c >= f.c &
    (1_minus f).c >= 0 & (1_minus g).c >= 0 by A7,Th1,SQUARE_1:def 2;
    then 1 - g.c <= 1 - f.c & 1 - h.c <= 1 - f.c &
    1-f.c >= 0 & 1-g.c >= 0 by FUZZY_1:def 7,REAL_2:106;
    then (1 - f.c)*(1 - f.c) >= (1 - g.c)*(1 - f.c) &
    (1 - g.c)*(1 - f.c) >= (1 - g.c)*(1 - h.c) by AXIOMS:25;
    then (1 - f.c)*(1 - f.c) >= (1 - g.c)*(1 - h.c) by AXIOMS:22;
    then 1 - ((1 - f.c)*(1 - f.c)) <= 1 - (1 - g.c)*(1 - h.c) by REAL_2:106;
then A8:(f ++ f).c <= 1 - (1 - g.c)*(1 - h.c) by Th105;
      (f ++ f).c >= f.c by Th63;
    then f.c <= 1 - (1 - g.c)*(1 - h.c) by A8,AXIOMS:22;
    then f.c <= (g ++ h).c by Th105;
then A9:f.c <= g.c + h.c - (g.c)*(h.c) by Def3;
      1 - ((1 - g.c)*(1 - h.c)) = (g ++ h).c by Th105;
    then 1 - ((1 - g.c)*(1 - h.c)) <= g.c + h.c - (g.c)*(h.c) by Def3;
    hence thesis by A7,A9,SQUARE_1:50;
   end;
   hence thesis;
  end;
  hence thesis;
 end;
 hence thesis by A1,A2;
end;

theorem Th107:
for c holds min(f,g ++ h).c <= (min(f,g) ++ min(f,h)).c
proof
 let c;
A1: min(f,g ++ h).c = min(f.c,(g ++ h).c) by FUZZY_1:6
 .= min(f.c,1 - ((1 - g.c)*(1 - h.c))) by Th105;
A2: (min(f,g) ++ min(f,h)).c
  = min(f,g).c + min(f,h).c - (min(f,g).c)*(min(f,h).c) by Def3
 .= min(f.c,g.c) + min(f,h).c - (min(f,g).c)*(min(f,h).c) by FUZZY_1:6
 .= min(f.c,g.c) + min(f.c,h.c) - (min(f,g).c)*(min(f,h).c) by FUZZY_1:6
 .= min(f.c,g.c) + min(f.c,h.c) - (min(f.c,g.c))*(min(f,h).c) by FUZZY_1:6
 .= min(f.c,g.c) + min(f.c,h.c) - (min(f.c,g.c))*(min(f.c,h.c)) by FUZZY_1:6;
   min(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
 min(f.c,g.c) + min(f.c,h.c) - (min(f.c,g.c))*(min(f.c,h.c))
 proof
    now per cases by SQUARE_1:38;
   suppose A3:min(f.c,g.c) = f.c & min(f.c,h.c) = f.c;
     min(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
   min(f.c,g.c) + min(f.c,h.c) - (min(f.c,g.c))*(min(f.c,h.c))
   proof
      min(f.c,1 - ((1 - g.c)*(1 - h.c))) <= f.c & (f ++ f).c >= f.c
    by Th63,SQUARE_1:35;
    then min(f.c,1 - ((1 - g.c)*(1 - h.c))) <= (f ++ f).c by AXIOMS:22;
    hence thesis by A3,Def3;
   end;
   hence thesis;
   suppose A4:min(f.c,g.c) = f.c & min(f.c,h.c) = h.c;
     min(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
   min(f.c,g.c) + min(f.c,h.c) - (min(f.c,g.c))*(min(f.c,h.c))
   proof
      (1_minus f).c >= 0 & h.c >= 0 by Th1;
    then 1 - f.c >= 0 & h.c >= 0 by FUZZY_1:def 7;
    then 0*(h.c) <= (h.c)*(1-f.c) by AXIOMS:25;
    then 0 + f.c <= (h.c)*(1-f.c) + f.c by AXIOMS:24;
    then f.c <= (h.c)*1-(h.c)*(f.c) + f.c by XCMPLX_1:40;
    then f.c <= f.c + h.c -(h.c)*(f.c) & min(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
f.c
    by SQUARE_1:35,XCMPLX_1:29;
    hence thesis by A4,AXIOMS:22;
   end;
   hence thesis;
   suppose A5:min(f.c,g.c) = g.c & min(f.c,h.c) = f.c;
     min(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
   min(f.c,g.c) + min(f.c,h.c) - (min(f.c,g.c))*(min(f.c,h.c))
   proof
      (1_minus f).c >= 0 & g.c >= 0 by Th1;
    then 1 - f.c >= 0 & g.c >= 0 by FUZZY_1:def 7;
    then 0*(g.c) <= (g.c)*(1-f.c) by AXIOMS:25;
    then 0 + f.c <= (g.c)*(1-f.c) + f.c by AXIOMS:24;
    then f.c <= (g.c)*1-(g.c)*(f.c) + f.c by XCMPLX_1:40;
    then f.c <= f.c + g.c -(g.c)*(f.c) & min(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
f.c
    by SQUARE_1:35,XCMPLX_1:29;
    hence thesis by A5,AXIOMS:22;
   end;
   hence thesis;
   suppose A6:min(f.c,g.c) = g.c & min(f.c,h.c) = h.c;
     min(f.c,1 - ((1 - g.c)*(1 - h.c))) <=
   min(f.c,g.c) + min(f.c,h.c) - (min(f.c,g.c))*(min(f.c,h.c))
   proof
      min(f.c,1-((1-g.c)*(1-h.c))) <= 1-((1 - g.c)*(1 - h.c)) by SQUARE_1:35;
    then min(f.c,1-((1-g.c)*(1-h.c))) <= (g ++ h).c by Th105;
    hence thesis by A6,Def3;
   end;
   hence thesis;
  end;
  hence thesis;
 end;
 hence thesis by A1,A2;
end;

theorem
  A \/ (B ++ D) c= (A \/ B) ++ (A \/ D) & A /\ (B ++ D) c= (A /\ B) ++ (A /\ D)
proof
   (for c holds min(f,g ++ h).c <= (min(f,g) ++ min(f,h)).c) &
 (for c holds max(f,g ++ h).c <= (max(f,g) ++ max(f,h)).c) by Th106,Th107;
 hence thesis by FUZZY_1:def 4;
end;

Back to top