Copyright (c) 2000 Association of Mizar Users
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;