### The Concept of Fuzzy Set and Membership Function and Basic Properties of Fuzzy Set Operation

by
Takashi Mitsuishi,
Noboru Endou, and
Yasunari Shidama

Copyright (c) 2000 Association of Mizar Users

MML identifier: FUZZY_1
[ MML identifier index ]

```environ

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

begin

reserve x,y,y1,y2 for set;
reserve C for non empty set;
reserve c for Element of C;

::::::Definition of Membership Function and Fuzzy Set

theorem Th1:
rng chi(x,y) c= [.0,1.]
proof
A1: rng chi(x,y) c= {0,1} by FUNCT_3:48;
{0,1} c= [.0,1.]
proof
1 in [.0,1.] & 0 in [.0,1.] by TOPREAL5:1;
hence thesis by ZFMISC_1:38;
end;
hence thesis by A1,XBOOLE_1:1;
end;

definition let C;
mode Membership_Func of C -> PartFunc of C,REAL means :Def1:
dom it = C & rng it c= [.0,1.];
existence
proof
take chi(C,C);
thus thesis by Th1,FUNCT_3:def 3;
end;
end;

theorem Th2:
chi(C,C) is Membership_Func of C
proof
A1:rng chi(C,C) c= [.0,1.] by Th1;
dom chi(C,C) =C by FUNCT_3:def 3;
hence thesis by A1,Def1;
end;

reserve f,h,g,h1 for Membership_Func of C;

definition let C be non empty set;
let h be Membership_Func of C;
mode FuzzySet of C,h-> set means :Def2:
it = [:C,h.:C:];
existence;
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;
pred A=B means :Def3:
h = g;
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;
pred A c= B means :Def4:
for c being Element of C holds h.c <= g.c;
end;

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;

Lm1:
A c= B & B c= A implies A = B
proof
assume A1:A c= B & B c= A;
A2:C = dom f & C = dom g by Def1;
for c being Element of C st c in C holds f.c = g.c
proof
let c be Element of C;
f.c <= g.c & g.c <= f.c by A1,Def4;
hence thesis by AXIOMS:21;
end;
then f = g by A2,PARTFUN1:34;
hence thesis by Def3;
end;

Lm2:
A = B implies A c= B & B c= A
proof
assume A=B;
then for x being Element of C holds f.x <= g.x & g.x <= f.x by Def3;
hence thesis by Def4;
end;

theorem
A = B iff A c= B & B c= A by Lm1,Lm2;

theorem
A c= A
proof
for c being Element of C holds f.c <= f.c;
hence thesis by Def4;
end;

theorem Th5:
A c= B & B c= D implies A c= D
proof
assume A1:A c= B & B c= D;
for c being Element of C
holds f.c <= h.c
proof
let c be Element of C;
f.c <= g.c & g.c <= h.c by A1,Def4;
hence thesis by AXIOMS:22;
end;
hence thesis by Def4;
end;

begin
::::::Intersection,Union and Complement

definition
let C be non empty set;
let h,g be Membership_Func of C;
func min(h,g) -> Membership_Func of C means :Def5:
for c being Element of C holds it.c = min(h.c,g.c);
existence
proof
defpred P[set,set] means \$2 = min(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 = min(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
A7:rng h c= [.0,1.] & rng g c= [.0,1.] by Def1;
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 Def1;
then h.x in rng h & g.x in rng g by FUNCT_1:def 5;
then A10:0 <= h.x & h.x <= 1 & 0 <= g.x & g.x <= 1 by A7,A9,INTEGRA2:1;
(h.x >= min(h.x,g.x) & g.x >= min(h.x,g.x)) by SQUARE_1:35;
then 0 <= min(h.x,g.x) & min(h.x,g.x) <= 1 by A10,AXIOMS:22,SQUARE_1:39;
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 A11:IT is Membership_Func of C by Def1;
for c being Element of C holds IT.c = min(h.c,g.c) by A3,A4;
hence thesis by A11;
end;
uniqueness
proof
let F,G be Membership_Func of C;
assume that
A12:for c being Element of C holds F.c = min(h.c,g.c)
and
A13:for c being Element of C holds G.c = min(h.c,g.c);
A14:C = dom F & C = dom G by Def1;
for c being Element of C st c in C holds F.c = G.c
proof
let c be Element of C;
F.c = min(h.c,g.c) & G.c = min(h.c,g.c) by A12,A13;
hence thesis;
end;
hence thesis by A14,PARTFUN1:34;
end;
end;

definition
let C be non empty set;
let h,g be Membership_Func of C;
func max(h,g) -> Membership_Func of C means :Def6:
for c being Element of C holds it.c = max(h.c,g.c);
existence
proof
defpred P[set,set] means \$2 = max(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 = max(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
A7:rng h c= [.0,1.] & rng g c= [.0,1.] by Def1;
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 Def1;
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 <= max(h.x,g.x) & max(h.x,g.x) <= 1 by SQUARE_1:50;
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 Def1;
for c being Element of C holds IT.c = max(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 = max(h.c,g.c)
and
A12:for c being Element of C holds G.c = max(h.c,g.c);
A13:C = dom F & C = dom G by Def1;
for c being Element of C st c in C holds F.c = G.c
proof
let c be Element of C;
F.c = max(h.c,g.c) & G.c = max(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 be Membership_Func of C;
func 1_minus h -> Membership_Func of C means :Def7:
for c being Element of C holds it.c = 1-h.c;
existence
proof
defpred P[set] means \$1 in dom h;
deffunc F(set) = 1 - h.\$1;
consider IT being PartFunc of C,REAL such that
A1:(for x be Element of C holds x in dom IT iff P[x]) &
(for x be Element of C st x in dom IT holds IT.x = F(x)) from LambdaPFD';
A2:dom IT = C & rng IT c= [.0,1.]
proof
A3: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 A4:x in C;
dom h = C by Def1;
hence thesis by A1,A4;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by XBOOLE_0:def 10;
end;
rng IT c= [.0,1.]
proof
A5:rng h c= [.0,1.] by Def1;
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
A6: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 A7:0=inf A & 1=sup A by INTEGRA1:6;
x in C;
then x in dom h by Def1;
then h.x in rng h by FUNCT_1:def 5;
then A8:0 <= h.x & h.x <= 1 by A5,A7,INTEGRA2:1;
then 0+1 <= 1+h.x by AXIOMS:24;
then 1-h.x <= 1 & 0 <= 1- h.x by A8,REAL_1:86,SQUARE_1:12;
then 0 <= IT.x & IT.x <= 1 by A1,A6;
hence thesis by A6,A7,INTEGRA2:1;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by A3;
end;
then A9:IT is Membership_Func of C by Def1;
for c being Element of C holds IT.c = 1 - h.c by A1,A2;
hence thesis by A9;
end;
uniqueness
proof
let F,G be Membership_Func of C;
assume that
A10:for c being Element of C holds F.c = 1-h.c
and
A11:for c being Element of C holds G.c = 1-h.c;
A12:C = dom F & C = dom G by Def1;
for c being Element of C st c in C holds F.c = G.c
proof
let c be Element of C;
F.c = 1-h.c & G.c = 1-h.c by A10,A11;
hence thesis;
end;
hence thesis by A12,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,min(h,g) equals
[:C,min(h,g).:C:];
correctness by Def2;
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,max(h,g) equals
[:C,max(h,g).:C:];
correctness by Def2;
end;

definition
let C be non empty set;
let h be Membership_Func of C;
let A be FuzzySet of C,h;
func A` -> FuzzySet of C,(1_minus h) equals
[:C,(1_minus h).:C:];
correctness by Def2;
end;

theorem
min(h.c,g.c) = min(h,g).c & max(h.c,g.c) = max(h,g).c by Def5,Def6;

theorem Th7:
max(h,h) = h & min(h,h) = h & max(h,h) = min(h,h) &
min(f,g) = min(g,f) & max(f,g) = max(g,f)
proof
A1:C = dom max(h,h) & C = dom min(h,h) & C = dom h &
C = dom min(f,g) & C = dom min(g,f) &
C = dom max(f,g) & C = dom max(g,f) by Def1;
A2:for x being Element of C st x in C holds min(h,h).x = h.x
proof
let x be Element of C;
min(h,h).x = min(h.x,h.x) by Def5
.= h.x;
hence thesis;
end;
A3:for x being Element of C st x in C holds max(h,h).x = h.x
proof
let x be Element of C;
max(h,h).x = max(h.x,h.x) by Def6
.= h.x;
hence thesis;
end;
A4:for x being Element of C st x in C holds max(h,h).x = min(h,h).x
proof
let x be Element of C;
A5:max(h,h).x = max(h.x,h.x) by Def6
.= h.x;
min(h,h).x = min(h.x,h.x) by Def5
.= h.x;
hence thesis by A5;
end;
A6:for x being Element of C st x in C holds min(f,g).x = min(g,f).x
proof
let x be Element of C;
min(f,g).x = min(f.x,g.x) by Def5
.= min(g,f).x by Def5;
hence thesis;
end;
for x being Element of C st x in C holds max(f,g).x = max(g,f).x
proof
let x be Element of C;
max(f,g).x = max(f.x,g.x) by Def6
.= max(g,f).x by Def6;
hence thesis;
end;
hence thesis by A1,A2,A3,A4,A6,PARTFUN1:34;
end;

canceled;

theorem
A /\ A = A & A \/ A = A
proof
min(f,f) = f by Th7;
hence A /\ A = A by Def3;
max(f,f) = f by Th7;
hence A \/ A = A by Def3;
end;

theorem Th10:
A /\ B = B /\ A & A \/ B = B \/ A
proof
min(f,g) = min(g,f) & max(f,g) = max(g,f) by Th7;
hence thesis by Def3;
end;

theorem Th11:
max(max(f,g),h) = max(f,max(g,h)) &
min(min(f,g),h) = min(f,min(g,h))
proof
A1:C = dom max(max(f,g),h) & C = dom max(f,max(g,h)) &
C = dom min(min(f,g),h) & C = dom min(f,min(g,h)) by Def1;
A2:for x being Element of C st x in C holds
max(max(f,g),h).x = max(f,max(g,h)).x
proof
let x be Element of C;
max(max(f,g),h).x = max(max(f,g).x,h.x) by Def6
.= max(max(f.x,g.x),h.x) by Def6
.= max(f.x,max(g.x,h.x)) by SQUARE_1:51
.= max(f.x,max(g,h).x) by Def6
.= max(f,max(g,h)).x by Def6;
hence thesis;
end;
for x being Element of C st x in C holds
min(min(f,g),h).x = min(f,min(g,h)).x
proof
let x be Element of C;
min(min(f,g),h).x = min(min(f,g).x,h.x) by Def5
.= min(min(f.x,g.x),h.x) by Def5
.= min(f.x,min(g.x,h.x)) by SQUARE_1:40
.= min(f.x,min(g,h).x) by Def5
.= min(f,min(g,h)).x by Def5;
hence thesis;
end;
hence thesis by A1,A2,PARTFUN1:34;
end;

theorem
(A \/ B) \/ D = A \/ (B \/ D)
proof
max(max(f,g),h) = max(f,max(g,h)) by Th11;
hence thesis by Def3;
end;

theorem
(A /\ B) /\ D = A /\ (B /\ D)
proof
min(min(f,g),h) = min(f,min(g,h)) by Th11;
hence thesis by Def3;
end;

theorem Th14:
max(f,min(f,g)) = f & min(f,max(f,g)) = f
proof
A1:C = dom max(f,min(f,g)) & C = dom f & C = dom min(f,max(f,g)) by Def1;
A2:for x being Element of C st x in C holds
max(f,min(f,g)).x = f.x
proof
let x be Element of C;
max(f,min(f,g)).x = max(f.x,min(f,g).x) by Def6
.= max(f.x,min(f.x,g.x)) by Def5
.= f.x by SQUARE_1:54;
hence thesis;
end;
for x being Element of C st x in C holds
min(f,max(f,g)).x = f.x
proof
let x be Element of C;
min(f,max(f,g)).x = min(f.x,max(f,g).x) by Def5
.= min(f.x,max(f.x,g.x)) by Def6
.= f.x by SQUARE_1:55;
hence thesis;
end;
hence thesis by A1,A2,PARTFUN1:34;
end;

theorem
A \/ (A /\ B) = A & A /\ (A \/ B) = A
proof
max(f,min(f,g)) = f & min(f,max(f,g)) = f by Th14;
hence thesis by Def3;
end;

theorem Th16:
min(f,max(g,h)) = max(min(f,g),min(f,h)) &
max(f,min(g,h)) = min(max(f,g),max(f,h))
proof
A1:C = dom min(f,max(g,h)) & C = dom max(min(f,g),min(f,h)) &
C = dom max(f,min(g,h)) & C = dom min(max(f,g),max(f,h)) by Def1;
A2:for x being Element of C st x in C holds
min(f,max(g,h)).x = max(min(f,g),min(f,h)).x
proof
let x be Element of C;
min(f,max(g,h)).x = min(f.x,max(g,h).x) by Def5
.= min(f.x,max(g.x,h.x)) by Def6
.= max(min(f.x,g.x),min(f.x,h.x)) by SQUARE_1:56
.= max(min(f,g).x,min(f.x,h.x)) by Def5
.= max(min(f,g).x,min(f,h).x) by Def5
.= max(min(f,g),min(f,h)).x by Def6;
hence thesis;
end;
for x being Element of C st x in C holds
max(f,min(g,h)).x = min(max(f,g),max(f,h)).x
proof
let x be Element of C;
max(f,min(g,h)).x = max(f.x,min(g,h).x) by Def6
.= max(f.x,min(g.x,h.x)) by Def5
.= min(max(f.x,g.x),max(f.x,h.x)) by SQUARE_1:57
.= min(max(f,g).x,max(f.x,h.x)) by Def6
.= min(max(f,g).x,max(f,h).x) by Def6
.= min(max(f,g),max(f,h)).x by Def5;
hence thesis;
end;
hence thesis by A1,A2,PARTFUN1:34;
end;

theorem Th17:
A \/ (B /\ D) = (A \/ B) /\ (A \/ D) &
A /\ (B \/ D) = (A /\ B) \/ (A /\ D)
proof
min(f,max(g,h)) = max(min(f,g),min(f,h)) &
max(f,min(g,h)) = min(max(f,g),max(f,h)) by Th16;
hence thesis by Def3;
end;

theorem Th18:
1_minus(1_minus(h)) = h
proof
A1:C = dom 1_minus(1_minus(h)) & C = dom h by Def1;
for x being Element of C st x in C holds
(1_minus(1_minus(h))).x = h.x
proof
let x be Element of C;
(1_minus(1_minus(h))).x = 1 - ((1_minus(h)).x) by Def7
.= 1 - (1 - h.x) by Def7
.= h.x by XCMPLX_1:18;
hence thesis;
end;
hence thesis by A1,PARTFUN1:34;
end;

theorem Th19:
(A`)` = A
proof
1_minus(1_minus(f)) = f by Th18;
hence thesis by Def3;
end;

theorem Th20:
1_minus(max(f,g)) = min(1_minus(f),1_minus(g)) &
1_minus(min(f,g)) = max(1_minus(f),1_minus(g))
proof
A1:C = dom 1_minus(max(f,g)) & C = dom min(1_minus(f),1_minus(g)) &
C = dom 1_minus(min(f,g)) & C = dom max(1_minus(f),1_minus(g)) by Def1;
A2:for x being Element of C st x in C holds
(1_minus(max(f,g))).x = min(1_minus(f),1_minus(g)).x
proof
let x be Element of C;
A3: (1_minus(max(f,g))).x
=1 - max(f,g).x by Def7
.=1 - max(f.x,g.x) by Def6
.=1 - (f.x + g.x + abs(f.x - g.x))/2 by SQUARE_1:45;
min(1_minus(f),1_minus(g)).x
=min((1_minus(f)).x,(1_minus(g)).x) by Def5
.=min((1 - f.x),(1_minus(g)).x) by Def7
.=min((1 - f.x),(1- g.x)) by Def7
.=((1-f.x) + (1-g.x) - abs((1-f.x) - (1-g.x)))/2 by SQUARE_1:34
.=((1-f.x) + 1-g.x- abs((1-f.x) - (1-g.x)))/2 by XCMPLX_1:29
.=(1+1-f.x -g.x- abs((1-f.x) - (1-g.x)))/2 by XCMPLX_1:29
.=(2-f.x -g.x- abs((1+-f.x) - (1-g.x)))/2 by XCMPLX_0:def 8
.=(2-f.x -g.x- abs(-f.x+g.x))/2 by XCMPLX_1:31
.=(2-f.x -g.x- abs(-(f.x-g.x)))/2 by XCMPLX_1:162
.=(2-f.x -g.x- abs(f.x-g.x))/2 by ABSVALUE:17
.=(2-(f.x + g.x) - abs(f.x-g.x))/2 by XCMPLX_1:36
.=((1+1)-((f.x + g.x) + abs(f.x-g.x)))/2 by XCMPLX_1:36
.=(1+1)/2 - ((f.x + g.x) + abs(f.x-g.x))/2 by XCMPLX_1:121
.=1 - ((f.x + g.x) + abs(f.x-g.x))/2;
hence thesis by A3;
end;
for x being Element of C st x in C holds
(1_minus(min(f,g))).x = max(1_minus(f),1_minus(g)).x
proof
let x be Element of C;
A4: (1_minus(min(f,g))).x
=1 - min(f,g).x by Def7
.=1 - min(f.x,g.x) by Def5
.=1 - (f.x + g.x - abs(f.x - g.x))/2 by SQUARE_1:34;
max(1_minus(f),1_minus(g)).x
=max((1_minus(f)).x,(1_minus(g)).x) by Def6
.=max((1 - f.x),(1_minus(g)).x) by Def7
.=max((1 - f.x),(1- g.x)) by Def7
.=((1-f.x) + (1-g.x) + abs((1-f.x) - (1-g.x)))/2 by SQUARE_1:45
.=((1-f.x) + 1-g.x + abs((1-f.x) - (1-g.x)))/2 by XCMPLX_1:29
.=(1+1-f.x -g.x +abs((1-f.x) - (1-g.x)))/2 by XCMPLX_1:29
.=(2-f.x -g.x + abs((1+-f.x) - (1-g.x)))/2 by XCMPLX_0:def 8
.=(2-f.x -g.x + abs(-f.x+g.x))/2 by XCMPLX_1:31
.=(2-f.x -g.x + abs(-(f.x-g.x)))/2 by XCMPLX_1:162
.=(2-f.x -g.x + abs(f.x-g.x))/2 by ABSVALUE:17
.=(2-(f.x + g.x) + abs(f.x-g.x))/2 by XCMPLX_1:36
.=((1+1)-((f.x + g.x) - abs(f.x-g.x)))/2 by XCMPLX_1:37
.=(1+1)/2 - ((f.x + g.x) - abs(f.x-g.x))/2 by XCMPLX_1:121
.=1 - ((f.x + g.x) - abs(f.x-g.x))/2;
hence thesis by A4;
end;
hence thesis by A1,A2,PARTFUN1:34;
end;

theorem ::DE MORGAN::
(A \/ B)` = A` /\ B` &
(A /\ B)` = A` \/ B`
proof
1_minus(max(f,g)) = min(1_minus(f),1_minus(g)) &
1_minus(min(f,g)) = max(1_minus(f),1_minus(g)) by Th20;
hence thesis by Def3;
end;

begin
::::::Empty Fuzzy Set and Universal Fuzzy Set

definition let C be non empty set;
mode Empty_FuzzySet of C -> set means :Def11:
it = [:C,chi({},C).:C:];
existence;

mode Universal_FuzzySet of C -> set means :Def12:
it = [:C,chi(C,C).:C:];
existence;
end;

reserve X for Universal_FuzzySet of C;
reserve E for Empty_FuzzySet of C;

canceled;

theorem Th23:
chi({},C) is Membership_Func of C
proof
A1:rng chi({},C) c= [.0,1.] by Th1;
dom chi({},C) =C by FUNCT_3:def 3;
hence thesis by A1,Def1;
end;

definition
let C be non empty set;
func EMF(C) -> Membership_Func of C equals :Def13:
chi({},C);
correctness by Th23;
end;

definition
let C be non empty set;
func UMF(C) -> Membership_Func of C equals :Def14:
chi(C,C);
correctness by Th2;
end;

canceled 2;

theorem Th26:
E is FuzzySet of C,EMF(C)
proof
A1:EMF(C) = chi({},C) by Def13;
E = [:C,chi({},C).:C:] by Def11;
hence thesis by A1,Def2;
end;

theorem Th27:
X is FuzzySet of C,UMF(C)
proof
A1:UMF(C) = chi(C,C) by Def14;
X = [:C,chi(C,C).:C:] by Def12;
hence thesis by A1,Def2;
end;

definition let C be non empty set;
redefine mode Empty_FuzzySet of C -> FuzzySet of C,EMF(C);
correctness by Th26;
redefine mode Universal_FuzzySet of C -> FuzzySet of C,UMF(C);
correctness by Th27;
end;

reserve X for Universal_FuzzySet of C;
reserve E for Empty_FuzzySet of C;

theorem Th28:
for a,b be Element of REAL,
f be PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds
(for x being Element of C st x in dom f holds a <= f.x & f.x <= b)
proof
let a,b be Element of REAL;
let f be PartFunc of C,REAL;
assume A1:rng f c= [.a,b.] & a <= b;
for x being Element of C st x in dom f holds a <= f.x & f.x <= b
proof
let x be Element of C;
assume x in dom f;
then A2:f.x in rng f by FUNCT_1:def 5;
reconsider A=[.a,b.] as closed-interval Subset of REAL by A1,INTEGRA1:def 1;
A = [. inf A, sup A .] by INTEGRA1:5;
then a=inf A & b=sup A by INTEGRA1:6;
hence thesis by A1,A2,INTEGRA2:1;
end;
hence thesis;
end;

theorem
E c= A
proof
for x being Element of C holds (EMF(C)).x <= f.x
proof
let x be Element of C;
A1:  dom f = C by Def1;
chi({},C) = EMF(C) by Def13;
then A2:(EMF(C)).x = 0 by FUNCT_3:def 3;
rng f c= [.0,1.] by Def1;
hence thesis by A1,A2,Th28;
end;
hence thesis by Def4;
end;

theorem
A c= X
proof
for x being Element of C holds f.x <= (UMF(C)).x
proof
let x be Element of C;
A1:dom f = C by Def1;
chi(C,C) = UMF(C) by Def14;
then A2:(UMF(C)).x = 1 by FUNCT_3:def 3;
rng f c= [.0,1.] by Def1;
hence thesis by A1,A2,Th28;
end;
hence thesis by Def4;
end;

theorem Th31:
for x be Element of C,h be Membership_Func of C holds
(EMF(C)).x <= h.x & h.x <= (UMF(C)).x
proof
let x be Element of C;
let h be Membership_Func of C;
A1:(EMF(C)).x <= h.x
proof
A2:dom h = C by Def1;
chi({},C) = EMF(C) by Def13;
then A3:(EMF(C)).x = 0 by FUNCT_3:def 3;
rng h c= [.0,1.] by Def1;
hence thesis by A2,A3,Th28;
end;
h.x <= (UMF(C)).x
proof
A4:dom h = C by Def1;
chi(C,C) = UMF(C) by Def14;
then A5:(UMF(C)).x = 1 by FUNCT_3:def 3;
rng h c= [.0,1.] by Def1;
hence thesis by A4,A5,Th28;
end;
hence thesis by A1;
end;

theorem Th32:
max(f,UMF(C)) = UMF(C) & min(f,UMF(C)) = f &
max(f,EMF(C)) = f & min(f,EMF(C)) = EMF(C)
proof
A1:max(f,UMF(C)) = UMF(C)
proof
A2:C = dom max(f,UMF(C)) & C = dom UMF(C) by Def1;
for x being Element of C st x in C holds
(max(f,UMF(C))).x = (UMF(C)).x
proof
let x be Element of C;
A3: f.x <= (UMF(C)).x by Th31;
(max(f,UMF(C))).x
= max(f.x,(UMF(C)).x) by Def6
.=(UMF(C)).x by A3,SQUARE_1:def 2;
hence thesis;
end;
hence thesis by A2,PARTFUN1:34;
end;
A4:min(f,UMF(C)) = f
proof
A5:C = dom min(f,UMF(C)) & C = dom f by Def1;
for x being Element of C st x in C holds
min(f,UMF(C)).x = f.x
proof
let x be Element of C;
A6: f.x <= (UMF(C)).x by Th31;
min(f,UMF(C)).x
= min(f.x,(UMF(C)).x) by Def5
.=f.x by A6,SQUARE_1:def 1;
hence thesis;
end;
hence thesis by A5,PARTFUN1:34;
end;
A7:max(f,EMF(C)) = f
proof
A8:C = dom max(f,EMF(C)) & C = dom f by Def1;
for x being Element of C st x in C holds
max(f,EMF(C)).x = f.x
proof
let x be Element of C;
A9: (EMF(C)).x <= f.x by Th31;
max(f,EMF(C)).x
= max(f.x,(EMF(C)).x) by Def6
.=f.x by A9,SQUARE_1:def 2;
hence thesis;
end;
hence thesis by A8,PARTFUN1:34;
end;
min(f,EMF(C)) = EMF(C)
proof
A10:C = dom min(f,EMF(C)) & C = dom EMF(C) by Def1;
for x being Element of C st x in C holds
min(f,EMF(C)).x = (EMF(C)).x
proof
let x be Element of C;
A11: (EMF(C)).x <= f.x by Th31;
min(f,EMF(C)).x
= min(f.x,(EMF(C)).x) by Def5
.=(EMF(C)).x by A11,SQUARE_1:def 1;
hence thesis;
end;
hence thesis by A10,PARTFUN1:34;
end;
hence thesis by A1,A4,A7;
end;

theorem
A \/ X = X & A /\ X = A
proof
max(f,UMF(C)) = UMF(C) & min(f,UMF(C)) = f by Th32;
hence thesis by Def3;
end;

theorem
A \/ E = A & A /\ E = E
proof
max(f,EMF(C)) = f & min(f,EMF(C)) = EMF(C) by Th32;
hence thesis by Def3;
end;

theorem Th35:
A c= A \/ B
proof
for x being Element of C holds f.x <= max(f,g).x
proof
let x be Element of C;
max(f,g).x = max(f.x,g.x) by Def6;
hence thesis by SQUARE_1:46;
end;
hence thesis by Def4;
end;

theorem Th36:
A c= D & B c= D implies A \/ B c= D
proof
assume
A1:A c= D & B c= D;
for x being Element of C holds max(f,g).x <= h.x
proof
let x be Element of C;
A2:f.x <= h.x & g.x <= h.x by A1,Def4;
max(f.x,g.x) = max(f,g).x by Def6;
hence thesis by A2,SQUARE_1:50;
end;
hence thesis by Def4;
end;

canceled;

theorem
A c= B implies A \/ D c= B \/ D
proof
assume
A1:A c= B;
for x being Element of C holds max(f,h).x <= max(g,h).x
proof
let x be Element of C;
f.x <= g.x by A1,Def4;
then max(f.x,h.x) <= max(g.x,h.x) by RFUNCT_3:7;
then max(f.x,h.x) <= max(g,h).x by Def6;
hence thesis by Def6;
end;
hence thesis by Def4;
end;

theorem
A c= B & D c= D1 implies A \/ D c= B \/ D1
proof
assume A1:A c= B & D c= D1;
for x being Element of C holds max(f,h).x <= max(g,h1).x
proof
let x be Element of C;
f.x <= g.x & h.x <= h1.x by A1,Def4;
then max(f.x,h.x) <= max(g.x,h1.x) by RFUNCT_3:7;
then max(f,h).x <= max(g.x,h1.x) by Def6;
hence thesis by Def6;
end;
hence thesis by Def4;
end;

theorem
A c= B implies A \/ B = B
proof
assume A1:A c= B;
max(f,g) = g
proof
A2:C = dom max(f,g) & C = dom g by Def1;
for x being Element of C st x in C holds max(f,g).x = g.x
proof
let x be Element of C;
f.x <= g.x by A1,Def4;
then g.x = max(f.x,g.x) by SQUARE_1:def 2
.= max(f,g).x by Def6;
hence thesis;
end;
hence thesis by A2,PARTFUN1:34;
end;
hence thesis by Def3;
end;

theorem Th41:
A /\ B c= A
proof
for x being Element of C holds min(f,g).x <= f.x
proof
let x be Element of C;
min(f,g).x = min(f.x,g.x) by Def5;
hence thesis by SQUARE_1:35;
end;
hence thesis by Def4;
end;

theorem
A /\ B c= A \/ B
proof
for x being Element of C holds min(f,g).x <= max(f,g).x
proof
let x be Element of C;
A1:min(f.x,g.x) <= f.x by SQUARE_1:35;
f.x <= max(f.x,g.x) by SQUARE_1:46;
then min(f.x,g.x) <= max(f.x,g.x) by A1,AXIOMS:22;
then min(f.x,g.x) <= max(f,g).x by Def6;
hence thesis by Def5;
end;
hence thesis by Def4;
end;

theorem Th43:
D c= A & D c= B implies D c= A /\ B
proof
assume A1:D c= A & D c= B;
for x being Element of C holds h.x <= min(f,g).x
proof
let x be Element of C;
h.x <= f.x & h.x <= g.x by A1,Def4;
then h.x <= min(f.x,g.x) by SQUARE_1:39;
hence thesis by Def5;
end;
hence thesis by Def4;
end;

theorem Th44:
for a,b,c,d be Element of REAL st a <= b & c <= d holds
min(a,c) <= min(b,d)
proof
let a,b,c,d be Real;
assume A1:a <= b & c <= d;
min(a,c) <= a & min(a,c) <= c by SQUARE_1:35;
then min(a,c) <= b & min(a,c) <= d by A1,AXIOMS:22;
hence thesis by SQUARE_1:39;
end;

theorem
for a,b,c be Element of REAL st a <= b holds
min(a,c) <= min(b,c) by Th44;

theorem
A c= B implies A /\ D c= B /\ D
proof
assume
A1:A c= B;
for x being Element of C holds min(f,h).x <= min(g,h).x
proof
let x be Element of C;
f.x <= g.x by A1,Def4;
then min(f.x,h.x) <= min(g.x,h.x) by Th44;
then min(f,h).x <= min(g.x,h.x) by Def5;
hence thesis by Def5;
end;
hence thesis by Def4;
end;

theorem
A c= B & D c= D1 implies A /\ D c= B /\ D1
proof
assume A1:A c= B & D c= D1;
for x being Element of C holds min(f,h).x <= min(g,h1).x
proof
let x be Element of C;
f.x <= g.x & h.x <= h1.x by A1,Def4;
then min(f.x,h.x) <= min(g.x,h1.x) by Th44;
then min(f,h).x <= min(g.x,h1.x) by Def5;
hence thesis by Def5;
end;
hence thesis by Def4;
end;

theorem Th48:
A c= B implies A /\ B = A
proof
assume A1:A c= B;
min(f,g) = f
proof
A2:C = dom min(f,g) & C = dom f by Def1;
for x being Element of C st x in C holds min(f,g).x = f.x
proof
let x be Element of C;
f.x <= g.x by A1,Def4;
then f.x = min(f.x,g.x) by SQUARE_1:def 1
.= min(f,g).x by Def5;
hence thesis;
end;
hence thesis by A2,PARTFUN1:34;
end;
hence thesis by Def3;
end;

theorem
A c= B & A c= D & B /\ D = E implies A = E
proof
assume A1:A c= B & A c= D & B /\ D = E;
f = EMF(C)
proof
A2:C = dom f & C = dom EMF(C) by Def1;
for x being Element of C st x in C holds f.x = (EMF(C)).x
proof
let x be Element of C;
f.x <= g.x & f.x <= h.x by A1,Def4;
then f.x <= min(g.x,h.x) by SQUARE_1:39;
then f.x <= min(g,h).x by Def5;
then A3: f.x <= (EMF(C)).x by A1,Def3;
(EMF(C)).x <= f.x by Th31;
hence thesis by A3,AXIOMS:21;
end;
hence thesis by A2,PARTFUN1:34;
end;
hence thesis by Def3;
end;

theorem
(A /\ B) \/ (A /\ D) = A implies A c= B \/ D
proof
assume A1:(A /\ B) \/ (A /\ D) = A;
for x being Element of C holds f.x <= max(g,h).x
proof
let x be Element of C;
max(min(f,g),min(f,h)).x = max(min(f,g).x,min(f,h).x) by Def6
.=max(min(f,g).x,min(f.x,h.x)) by Def5
.=max(min(f.x,g.x),min(f.x,h.x)) by Def5
.=min(f.x,max(g.x,h.x)) by SQUARE_1:56;
then f.x = min(f.x,max(g.x,h.x)) by A1,Def3;
then f.x <= max(g.x,h.x) by SQUARE_1:def 1;
hence thesis by Def6;
end;
hence thesis by Def4;
end;

theorem
A c= B & B /\ D = E implies A /\ D = E
proof
assume A1:A c= B & B /\ D = E;
min(f,h) = EMF(C)
proof
A2:C = dom min(f,h) & C = dom EMF(C) by Def1;
for x being Element of C st x in C holds min(f,h).x = (EMF(C)).x
proof
let x be Element of C;
f.x <= g.x & min(g,h) = EMF(C) by A1,Def3,Def4;
then min(f.x,h.x) <= min(g.x,h.x) by Th44;
then min(f.x,h.x) <= min(g,h).x by Def5;
then min(f,h).x <= min(g,h).x by Def5;
then A3:min(f,h).x <= (EMF(C)).x by A1,Def3;
(EMF(C)).x <= min(f,h).x by Th31;
hence thesis by A3,AXIOMS:21;
end;
hence thesis by A2,PARTFUN1:34;
end;
hence thesis by Def3;
end;

theorem
A c= E implies A = E
proof
assume A1:A c= E;
f = EMF(C)
proof
A2:C = dom f & C = dom EMF(C) by Def1;
for x being Element of C st x in C holds f.x = (EMF(C)).x
proof
let x be Element of C;
A3:(EMF(C)).x <= f.x by Th31;
f.x <= (EMF(C)).x by A1,Def4;
hence thesis by A3,AXIOMS:21;
end;
hence thesis by A2,PARTFUN1:34;
end;
hence thesis by Def3;
end;

theorem
A \/ B = E iff A = E & B = E
proof
A1:A \/ B = E implies A = E & B = E
proof
assume A2:A \/ B = E;
A = E & B = E
proof
f = EMF(C) & g = EMF(C)
proof
A3: f = EMF(C)
proof
A4:  C = dom f & C = dom EMF(C) by Def1;
for x being Element of C st x in C holds f.x = (EMF(C)).x
proof
let x be Element of C;
A5:  (EMF(C)).x <= f.x by Th31;
max(f.x,g.x) = max(f,g).x by Def6
.=(EMF(C)).x by A2,Def3;
then f.x <= (EMF(C)).x by SQUARE_1:46;
hence thesis by A5,AXIOMS:21;
end;
hence thesis by A4,PARTFUN1:34;
end;
g = EMF(C)
proof
A6:  C = dom g & C = dom EMF(C) by Def1;
for x being Element of C st x in C holds g.x = (EMF(C)).x
proof
let x be Element of C;
A7:  (EMF(C)).x <= g.x by Th31;
max(f.x,g.x) = max(f,g).x by Def6
.=(EMF(C)).x by A2,Def3;
then g.x <= (EMF(C)).x by SQUARE_1:46;
hence thesis by A7,AXIOMS:21;
end;
hence thesis by A6,PARTFUN1:34;
end;
hence thesis by A3;
end;
hence thesis by Def3;
end;
hence thesis;
end;
A = E & B = E implies A \/ B = E
proof
assume A8:A = E & B = E;
A \/ B = E
proof
max(f,g) = EMF(C)
proof
A9: C = dom max(f,g) & C = dom EMF(C) by Def1;
for x being Element of C st x in C holds max(f,g).x = (EMF(C)).x
proof
let x be Element of C;
f = EMF(C) & g = EMF(C) by A8,Def3;
then max(f,g).x = max((EMF(C)).x,(EMF(C)).x) by Def6
.= (EMF(C)).x;
hence thesis;
end;
hence thesis by A9,PARTFUN1:34;
end;
hence thesis by Def3;
end;
hence thesis;
end;
hence thesis by A1;
end;

theorem
A = B \/ D iff B c= A & D c= A & for h1,D1 st B c= D1 & D c= D1 holds A c= D1
proof
thus A = B \/ D
implies B c= A & D c= A & for h1,D1 st B c= D1 & D c= D1 holds A c= D1
proof
assume A1:A = B \/ D;
B c= A & D c= A & for D1 st B c= D1 & D c= D1 holds A c= D1
proof
A2:B c= A & D c= A
proof
for x being Element of C holds g.x <= f.x & h.x <= f.x
proof
let x be Element of C;
g.x <= max(g.x,h.x) & h.x <= max(g.x,h.x) by SQUARE_1:46;
then g.x <= max(g,h).x & h.x <= max(g,h).x by Def6;
hence thesis by A1,Def3;
end;
hence thesis by Def4;
end;
for D1 st B c= D1 & D c= D1 holds A c= D1
proof
let D1;
assume A3:B c= D1 & D c= D1;
A c= D1
proof
for x being Element of C holds f.x <= h1.x
proof
let x be Element of C;
g.x <= h1.x & h.x <= h1.x by A3,Def4;
then max(g.x,h.x) <= h1.x by SQUARE_1:50;
then max(g,h).x <= h1.x by Def6;
hence thesis by A1,Def3;
end;
hence thesis by Def4;
end;
hence thesis;
end;
hence thesis by A2;
end;
hence thesis;
end;
assume that
A4:B c= A and
A5:D c= A and
A6:for h1,D1 st B c= D1 & D c= D1 holds A c= D1;
A = B \/ D
proof
A7:B \/ D c= A by A4,A5,Th36;
A8:B c= B \/ D & D c= D \/ B by Th35;
B \/ D = D \/ B by Th10;
then D \/ B c= B \/ D by Lm2;
then B c= B \/ D & D c= B \/ D by A8,Th5;
then A c= B \/ D by A6;
hence thesis by A7,Lm1;
end;
hence thesis;
end;

theorem
A = B /\ D iff A c= B & A c= D & for h1,D1 st D1 c= B & D1 c= D holds D1 c= A
proof
thus A = B /\ D implies
A c= B & A c= D & for h1,D1 st D1 c= B & D1 c= D holds D1 c= A
proof
assume A1:A = B /\ D;
A2:A c= B & A c= D
proof
for x being Element of C holds f.x <= g.x & f.x <= h.x
proof
let x be Element of C;
f.x = min(g,h).x by A1,Def3
.= min(g.x,h.x) by Def5;
hence thesis by SQUARE_1:35;
end;
hence thesis by Def4;
end;
for D1 st D1 c= B & D1 c= D holds D1 c= A
proof
let D1;
assume A3:D1 c= B & D1 c= D;
D1 c= A
proof
for x being Element of C holds h1.x <= f.x
proof
let x be Element of C;
A4:  f = min(g,h) by A1,Def3;
h1.x <= g.x & h1.x <= h.x by A3,Def4;
then min(h1.x,h1.x) <= min(g.x,h.x) by Th44;
hence thesis by A4,Def5;
end;
hence thesis by Def4;
end;
hence thesis;
end;
hence thesis by A2;
end;
assume that
A5:A c= B & A c= D and
A6:for h1,D1 st D1 c= B & D1 c= D holds D1 c= A;
A = B /\ D
proof
A7:A c= B /\ D by A5,Th43;
A8:B /\ D c= B & D /\ B c= D by Th41;
B /\ D = D /\ B by Th10;
then B /\ D c= D /\ B by Lm2;
then B /\ D c= B & B /\ D c= D by A8,Th5;
then B /\ D c= A by A6;
hence thesis by A7,Lm1;
end;
hence thesis;
end;

theorem
A c= (B \/ D) & A /\ D = E implies A c= B
proof
assume A1:A c= (B \/ D) & A /\ D = E;
then A /\ (B \/ D) = A by Th48;
then A2:A /\ (B \/ D) c= A & A c= A /\ (B \/ D) by Lm2;
A /\ (B \/ D) = (A /\ B) \/ (A /\ D) by Th17;
then A /\ (B \/ D) c= (A /\ B) \/ (A /\ D)
& (A /\ B) \/ (A /\ D) c= A /\ (B \/ D) by Lm2;
then (A /\ B) \/ (A /\ D) c= A & A c= (A /\ B) \/ (A /\ D) by A2,Th5;
then A3:(A /\ B) \/ (A /\ D) = A by Lm1;
for x being Element of C holds f.x <= g.x
proof
let x be Element of C;
f = max(min(f,g),min(f,h)) by A3,Def3;
then f = max(min(f,g),EMF(C)) by A1,Def3
.= min(f,g) by Th32;
then f.x = min(f.x,g.x) by Def5;
hence thesis by SQUARE_1:def 1;
end;
hence thesis by Def4;
end;

theorem Th57:
A c= B iff B` c= A`
proof
A1:A c= B implies B` c= A`
proof
assume A2:A c= B;
for x being Element of C holds (1_minus(g)).x <= (1_minus(f)).x
proof
let x be Element of C;
f.x <= g.x by A2,Def4;
then 1-(g.x) <= 1-(f.x) by REAL_2:106;
then (1_minus(g)).x <= 1-(f.x) by Def7;
hence thesis by Def7;
end;
hence thesis by Def4;
end;
B` c= A` implies A c= B
proof
assume A3:B` c= A`;
for x being Element of C holds f.x <= g.x
proof
let x be Element of C;
(1_minus(g)).x <= (1_minus(f)).x by A3,Def4;
then 1-g.x <= (1_minus(f)).x by Def7;
then 1-g.x <= 1-f.x by Def7;
then f.x-g.x <= 1-1 by REAL_2:169;
hence thesis by SQUARE_1:11;
end;
hence thesis by Def4;
end;
hence thesis by A1;
end;

theorem
A c= B` implies B c= A`
proof
assume A1:A c= B`;
for x being Element of C holds g.x <= (1_minus(f)).x
proof
let x be Element of C;
f.x <= (1_minus(g)).x by A1,Def4;
then f.x <= 1-g.x by Def7;
then g.x <= 1-f.x by REAL_2:165;
hence thesis by Def7;
end;
hence thesis by Def4;
end;

theorem
A` c= B implies B` c= A
proof
assume A` c= B;
then A1:B` c= (A`)` by Th57;
(A`)` = A by Th19;
then (A`)` c= A by Lm2;
hence thesis by A1,Th5;
end;

theorem
(A \/ B)` c= A` & (A \/ B)` c= B`
proof
thus (A \/ B)` c= A`
proof
for x being Element of C holds (1_minus(max(f,g))).x <= (1_minus(f)).x
proof
let x be Element of C;
f.x <= max(f.x,g.x) by SQUARE_1:46;
then f.x <= max(f,g).x by Def6;
then 1 - f.x >= 1 - max(f,g).x by REAL_2:106;
then (1_minus(f)).x >= 1 - max(f,g).x by Def7;
hence thesis by Def7;
end;
hence thesis by Def4;
end;
(A \/ B)` c= B`
proof
for x being Element of C holds (1_minus(max(f,g))).x <= (1_minus(g)).x
proof
let x be Element of C;
g.x <= max(f.x,g.x) by SQUARE_1:46;
then g.x <= max(f,g).x by Def6;
then 1 - g.x >= 1 - max(f,g).x by REAL_2:106;
then (1_minus(g)).x >= 1 - max(f,g).x by Def7;
hence thesis by Def7;
end;
hence thesis by Def4;
end;
hence thesis;
end;

theorem
A` c= (A /\ B)` & B` c= (A /\ B)`
proof
thus A` c= (A /\ B)`
proof
for x being Element of C holds (1_minus(f)).x <= (1_minus(min(f,g))).x
proof
let x be Element of C;
min(f.x,g.x) <= f.x by SQUARE_1:35;
then min(f,g).x <= f.x by Def5;
then 1 - f.x <= 1 - min(f,g).x by REAL_2:106;
then (1_minus(f)).x <= 1 - min(f,g).x by Def7;
hence thesis by Def7;
end;
hence thesis by Def4;
end;
thus B` c= (A /\ B)`
proof
for x being Element of C holds (1_minus(g)).x <= (1_minus(min(f,g))).x
proof
let x be Element of C;
min(f.x,g.x) <= g.x by SQUARE_1:35;
then min(f,g).x <= g.x by Def5;
then 1 - g.x <= 1 - min(f,g).x by REAL_2:106;
then (1_minus(g)).x <= 1 - min(f,g).x by Def7;
hence thesis by Def7;
end;
hence thesis by Def4;
end;
end;

Lm3:
for x being Element of C holds (EMF(C)).x = 0 & (UMF(C)).x = 1
proof
let x be Element of C;
A1:(UMF(C)).x = 1
proof
chi(C,C).x = 1 by FUNCT_3:def 3;
hence thesis by Def14;
end;
chi({},C).x = 0 by FUNCT_3:def 3;
hence thesis by A1,Def13;
end;

theorem Th62:
1_minus(EMF(C)) = UMF(C) & 1_minus(UMF(C)) = EMF(C)
proof
thus 1_minus(EMF(C)) = UMF(C)
proof
A1:C = dom 1_minus(EMF(C)) & C = dom UMF(C) by Def1;
for x being Element of C st x in C holds (1_minus(EMF(C))).x = (UMF(C)).x
proof
let x be Element of C;
(1_minus(EMF(C))).x = 1 - (EMF(C)).x by Def7
.= 1 - 0 by Lm3
.= 1;
hence thesis by Lm3;
end;
hence thesis by A1,PARTFUN1:34;
end;
thus 1_minus(UMF(C)) = EMF(C)
proof
A2:C = dom 1_minus(UMF(C)) & C = dom EMF(C) by Def1;
for x being Element of C st x in C holds (1_minus(UMF(C))).x = (EMF(C)).x
proof
let x be Element of C;
(1_minus(UMF(C))).x = 1 - (UMF(C)).x by Def7
.= 1 - 1 by Lm3
.= 0;
hence thesis by Lm3;
end;
hence thesis by A2,PARTFUN1:34;
end;
end;

theorem
E` = X & X` = E
proof
1_minus(EMF(C)) = UMF(C) & 1_minus(UMF(C)) = EMF(C) by Th62;
hence thesis by Def3;
end;

begin
::::::Exclusive Sum, Absolute Difference

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,max(min(h,1_minus(g)),min(1_minus(h),g)) equals
[:C,max(min(h,1_minus(g)),min(1_minus(h),g)).:C:];
correctness by Def2;
end;

canceled;

theorem
A \+\ B = B \+\ A
proof
max(min(f,1_minus(g)),min(1_minus(f),g))
= max(min(g,1_minus(f)),min(1_minus(g),f))
proof
A1:C = dom max(min(f,1_minus(g)),min(1_minus(f),g)) &
C = dom max(min(g,1_minus(f)),min(1_minus(g),f)) by Def1;
for x being Element of C st x in C holds
max(min(f,1_minus(g)),min(1_minus(f),g)).x
= max(min(g,1_minus(f)),min(1_minus(g),f)).x
proof
let x be Element of C;
max(min(f,1_minus(g)),min(1_minus(f),g)).x
= max(min(1_minus(g),f),min(1_minus(f),g)).x by Th7
.= max(min(1_minus(g),f),min(g,1_minus(f))).x by Th7
.= max(min(g,1_minus(f)),min(1_minus(g),f)).x by Th7;
hence thesis;
end;
hence thesis by A1,PARTFUN1:34;
end;
hence thesis by Def3;
end;

theorem
A \+\ E = A & E \+\ A = A
proof
thus A \+\ E = A
proof
max(min(f,1_minus(EMF(C))),min(1_minus(f),EMF(C))) = f
proof
A1:C = dom max(min(f,1_minus(EMF(C))),min(1_minus(f),EMF(C))) &
C = dom f by Def1;
for x being Element of C st x in C holds
max(min(f,1_minus(EMF(C))),min(1_minus(f),EMF(C))).x = f.x
proof
let x be Element of C;
max(min(f,1_minus(EMF(C))),min(1_minus(f),EMF(C))).x
=max(min(f,UMF(C)),min(1_minus(f),EMF(C))).x by Th62
.=max(f,min(1_minus(f),EMF(C))).x by Th32
.=max(f,(EMF(C))).x by Th32
.=f.x by Th32;
hence thesis;
end;
hence thesis by A1,PARTFUN1:34;
end;
hence thesis by Def3;
end;
thus E \+\ A = A
proof
max(min(EMF(C),1_minus(f)),min(1_minus(EMF(C)),f)) = f
proof
A2:C = dom max(min(EMF(C),1_minus(f)),min(1_minus(EMF(C)),f)) &
C = dom f by Def1;
for x being Element of C st x in C holds
max(min(EMF(C),1_minus(f)),min(1_minus(EMF(C)),f)).x = f.x
proof
let x be Element of C;
max(min(EMF(C),1_minus(f)),min(1_minus(EMF(C)),f)).x
=max(min(EMF(C),1_minus(f)),min(UMF(C),f)).x by Th62
.=max(min(EMF(C),1_minus(f)),min(f,UMF(C))).x by Th7
.=max(min(EMF(C),1_minus(f)),f).x by Th32
.=max(min(1_minus(f),EMF(C)),f).x by Th7
.=max(EMF(C),f).x by Th32
.=max(f,EMF(C)).x by Th7
.=f.x by Th32;
hence thesis;
end;
hence thesis by A2,PARTFUN1:34;
end;
hence thesis by Def3;
end;
end;

theorem
A \+\ X = A` & X \+\ A = A`
proof
thus A \+\ X = A`
proof
max(min(f,1_minus(UMF(C))),min(1_minus(f),UMF(C))) = 1_minus(f)
proof
A1:C = dom max(min(f,1_minus(UMF(C))),min(1_minus(f),UMF(C))) &
C = dom 1_minus(f) & C = dom 1_minus(f) by Def1;
for x being Element of C st x in C holds
max(min(f,1_minus(UMF(C))),min(1_minus(f),UMF(C))).x = (1_minus(f)).x
proof
let x be Element of C;
max(min(f,1_minus(UMF(C))),min(1_minus(f),UMF(C))).x
= max(min(f,1_minus(UMF(C))),1_minus(f)).x by Th32
.= max(min(f,EMF(C)),1_minus(f)).x by Th62
.= max(EMF(C),1_minus(f)).x by Th32
.= max(1_minus(f),EMF(C)).x by Th7
.= (1_minus(f)).x by Th32;
hence thesis;
end;
hence thesis by A1,PARTFUN1:34;
end;
hence thesis by Def3;
end;
thus X \+\ A = A`
proof
max(min(UMF(C),1_minus(f)),min(1_minus(UMF(C)),f)) = 1_minus(f)
proof
A2:C = dom max(min(UMF(C),1_minus(f)),min(1_minus(UMF(C)),f)) &
C = dom 1_minus(f) by Def1;
for x being Element of C st x in C holds
max(min(UMF(C),1_minus(f)),min(1_minus(UMF(C)),f)).x = (1_minus(f)).x
proof
let x be Element of C;
max(min(UMF(C),1_minus(f)),min(1_minus(UMF(C)),f)).x
= max(min(UMF(C),1_minus(f)),min(EMF(C),f)).x by Th62
.= max(min(UMF(C),1_minus(f)),min(f,EMF(C))).x by Th7
.= max(min(UMF(C),1_minus(f)),EMF(C)).x by Th32
.= min(UMF(C),1_minus(f)).x by Th32
.= min(1_minus(f),UMF(C)).x by Th7
.= (1_minus(f)).x by Th32;
hence thesis;
end;
hence thesis by A2,PARTFUN1:34;
end;
hence thesis by Def3;
end;
end;

theorem
(A /\ B) \/ (B /\ D) \/ (D /\ A) = (A \/ B) /\ (B \/ D) /\ (D \/ A)
proof
min(min(max(f,g),max(g,h)),max(h,f))
= max(min(min(max(f,g),max(g,h)),h),min(min(max(f,g),max(g,h)),f)) by Th16
.=max(min(max(f,g),min(max(g,h),h)),min(min(max(f,g),max(g,h)),f)) by Th11
.=max(min(max(f,g),min(max(g,h),h)),min(max(f,g),min(max(g,h),f))) by Th11
.=max(min(max(f,g),min(max(g,h),h)),min(max(f,g),min(f,max(g,h)))) by Th7
.=max(min(max(f,g),min(max(g,h),h)),min(min(max(f,g),f),max(g,h))) by Th11
.=max(min(max(f,g),min(max(h,g),h)),min(min(max(f,g),f),max(g,h))) by Th7
.=max(min(max(f,g),min(h,max(h,g))),min(min(max(f,g),f),max(g,h))) by Th7
.=max(min(max(f,g),h),min(min(max(f,g),f),max(g,h))) by Th14
.=max(min(max(f,g),h),min(min(f,max(f,g)),max(g,h))) by Th7
.=max(min(max(f,g),h),min(f,max(g,h))) by Th14
.=max(min(max(f,g),h),max(min(f,g),min(f,h) )) by Th16
.=max(min(h,max(f,g)),max(min(f,g),min(f,h) )) by Th7
.=max(max(min(h,f),min(h,g)),max(min(f,g),min(f,h) )) by Th16
.=max(max(min(f,g),min(f,h)),max(min(h,f),min(h,g))) by Th7
.=max(max(min(f,g),min(f,h)),max(min(f,h),min(h,g))) by Th7
.=max(max(max(min(f,g),min(f,h)),min(f,h)),min(h,g)) by Th11
.=max(max(min(f,g),max(min(f,h),min(f,h))),min(h,g)) by Th11
.=max(max(min(f,g),min(f,h)),min(h,g)) by Th7
.=max(min(f,g),max(min(f,h),min(h,g))) by Th11
.=max(min(f,g),max(min(h,g),min(f,h))) by Th7
.=max(max(min(f,g),min(h,g)),min(f,h)) by Th11
.=max(max(min(f,g),min(g,h)),min(f,h)) by Th7
.=max(max(min(f,g),min(g,h)),min(h,f)) by Th7;
hence thesis by Def3;
end;

theorem
(A /\ B) \/ (A` /\ B`) c= (A \+\ B)`
proof
set f1 = 1_minus f,
g1 = 1_minus g;
for x being Element of C holds
max(min(f,g),min(f1,g1)).x <= (1_minus max(min(f,g1),min(f1,g))).x
proof
let x be Element of C;
(1_minus max(min(f,g1),min(f1,g)))
= min( 1_minus min(f,g1) , 1_minus min(f1,g)) by Th20
.= min( max(f1,1_minus g1),1_minus min(f1,g)) by Th20
.= min( max(f1,g),1_minus min(f1,g)) by Th18
.= min( max(f1,g),max(1_minus f1,g1)) by Th20
.= min( max(f1,g),max(f,g1)) by Th18
.= max(min(max(f1,g),f),min(max(f1,g),g1)) by Th16
.= max(min(f,max(f1,g)),min(max(f1,g),g1)) by Th7
.= max( max(min(f,f1),min(f,g)) ,min(max(f1,g),g1)) by Th16
.= max( max(min(f,f1),min(f,g)) ,min(g1,max(f1,g))) by Th7
.= max( max(min(f,f1),min(f,g)) , max(min(g1,f1),min(g1,g))) by Th16
.= max(max(max(min(f,f1),min(f,g)),min(g1,f1)),min(g1,g)) by Th11
.= max( max(max(min(f,g),min(f,f1)),min(g1,f1)) , min(g1,g)) by Th7
.= max( max(min(g1,f1),max(min(f,g),min(f,f1))) , min(g1,g)) by Th7
.= max( max(max(min(g1,f1),min(f,g)),min(f,f1)) , min(g1,g)) by Th11
.= max( max(min(g1,f1),min(f,g)), max(min(f,f1) , min(g1,g))) by Th11;
then (1_minus max(min(f,g1),min(f1,g))).x
=max(max(min(g1,f1),min(f,g)).x,max(min(f,f1),min(g1,g)).x) by Def6
.=max(max(min(f,g),min(g1,f1)).x,max(min(f,f1),min(g1,g)).x) by Th7
.=max(max(min(f,g),min(f1,g1)).x,max(min(f,f1),min(g1,g)).x) by Th7;
hence thesis by SQUARE_1:46;
end;
hence thesis by Def4;
end;

theorem
(A \+\ B) \/ A /\ B c= A \/ B
proof
set f1 = 1_minus f,
g1 = 1_minus g;
for x being Element of C holds
max(f,g).x >= max(max(min(f,g1),min(f1,g)) ,min(f,g)).x
proof
let x be Element of C;
max(max(min(f,g1),min(f1,g)) ,min(f,g))
= max(min(f,g1),max(min(f1,g),min(f,g))) by Th11
.= max(min(f,g1),min(max(min(f1,g),f),max(min(f1,g),g))) by Th16
.= max(min(f,g1),min(max(min(f1,g),f),max(g,min(f1,g)))) by Th7
.= max(min(f,g1),min(max(min(f1,g),f),max(g,min(g,f1)))) by Th7
.= max(min(f,g1),min(max(min(f1,g),f),g)) by Th14
.= min(max(min(f,g1),max(min(f1,g),f)),max(min(f,g1),g)) by Th16
.= min(max(min(f,g1),max(f,min(f1,g))),max(min(f,g1),g)) by Th7
.= min(max(max(min(f,g1),f),min(f1,g)) ,max(min(f,g1),g)) by Th11
.= min(max(max(f,min(f,g1)),min(f1,g)) ,max(min(f,g1),g)) by Th7
.= min(max(f,min(f1,g)) ,max(min(f,g1),g)) by Th14
.= min( min(max(f,f1),max(f,g)) ,max(min(f,g1),g)) by Th16
.= min( min(max(f,f1),max(f,g)) ,max(g,min(f,g1))) by Th7
.= min( min(max(f,f1),max(f,g)) , min(max(g,f),max(g,g1)) ) by Th16
.= min(min( min(max(f,f1),max(f,g)),max(g,f) ),max(g,g1) ) by Th11
.= min(min( max(f,f1),min(max(f,g),max(g,f)) ),max(g,g1) ) by Th11
.= min(min( max(f,f1),min(max(f,g),max(f,g)) ),max(g,g1) ) by Th7
.= min(min( max(f,f1),max(f,g) ),max(g,g1) ) by Th7
.= min(min(max(f,g),max(f,f1)),max(g,g1)) by Th7
.= min(max(f,g),min(max(f,f1),max(g,g1))) by Th11;
then max(max(min(f,g1),min(f1,g)) ,min(f,g)).x
= min(max(f,g).x,min(max(f,f1),max(g,g1)).x) by Def5;
hence thesis by SQUARE_1:35;
end;
hence thesis by Def4;
end;

theorem
A \+\ A = A /\ A`
proof
max(min(f,1_minus f),min(1_minus f,f))
= max(min(f,1_minus f),min(f,1_minus f)) by Th7
.= min(f,1_minus f) by Th7;
hence thesis by Def3;
end;

definition
let C be non empty set;
let h,g be Membership_Func of C;
func ab_difMF(h,g) -> Membership_Func of C means
for c being Element of C holds it.c = abs(h.c - g.c);
existence
proof
defpred P[set,set] means \$2 = abs(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 = abs(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
A7:rng h c= [.0,1.] & rng g c= [.0,1.] by Def1;
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 Def1;
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 h.x - g.x <= 1 - g.x & 1-0 >= 1-g.x &
0 - g.x <= h.x - g.x & -g.x >= -1
by REAL_1:49,50,REAL_2:106;
then - g.x <= h.x - g.x & -g.x >= -1 &
h.x - g.x <= 1 - g.x & 1 >= 1-g.x by XCMPLX_1:150;
then h.x - g.x <= 1 & -1 <= h.x - g.x by AXIOMS:22;
then 0 <= abs(h.x - g.x) & abs(h.x - g.x) <= 1 by ABSVALUE:5,12;
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 Def1;
for c being Element of C holds IT.c = abs(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 = abs(h.c - g.c)
and
A12:for c being Element of C holds G.c = abs(h.c - g.c);
A13:C = dom F & C = dom G by Def1;
for c being Element of C st c in C holds F.c = G.c
proof
let c be Element of C;
F.c = abs(h.c - g.c) & G.c = abs(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 ab_dif(A,B) -> FuzzySet of C,ab_difMF(h,g) equals
[:C,ab_difMF(h,g).:C:];
correctness by Def2;
end;
```