:: Some Properties of Membership Functions Composed of Triangle Functions and 
:: Piecewise Linear Functions
::  by Takashi Mitsuishi
:: 
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, SUBSET_1, XXREAL_1, CARD_1, RELAT_1, TARSKI,
      FUNCT_1, XXREAL_0, PARTFUN1, ARYTM_1, ARYTM_3, COMPLEX1, FUZZY_1,
      MSALIMIT, FUZNUM_1, REAL_1, ORDINAL2, FCONT_1, SQUARE_1, FUNCT_3,
      RCOMP_1, NUMPOLY1, JGRAPH_2, FUNCT_4, FUNCT_7, SIN_COS, FUNCT_9, INT_1,
      VALUED_1, FDIFF_1, SIN_COS9, FUZZY_5;
 notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, COMPLEX1, RELAT_1, SQUARE_1,
      FUNCT_1, INT_1, XCMPLX_0, XXREAL_0, XREAL_0, VALUED_1, PARTFUN1, FUNCT_2,
      FUNCT_3, FUNCT_4, FUNCT_9, FDIFF_1, SIN_COS, RCOMP_1, SIN_COS9, FCONT_1,
      FUZZY_1, FUZNUM_1, LFUZZY_1;
 constructors COMPLEX1, SEQ_4, RELSET_1, FCONT_1, FUNCT_4, FUZNUM_1, LFUZZY_1,
      SIN_COS, SQUARE_1, POWER, FUNCT_9, FDIFF_1, SIN_COS9;
 registrations RELSET_1, NUMBERS, XXREAL_0, MEMBERED, XBOOLE_0, VALUED_0,
      VALUED_1, FUNCT_2, XREAL_0, ORDINAL1, FCONT_1, XCMPLX_0, RCOMP_1,
      SIN_COS, SIN_COS6, SQUARE_1, INT_1, SIN_COS9;
 requirements NUMERALS, REAL, SUBSET, ARITHM;


begin

theorem :: FUZZY_5:1
for a,b,c,d being Real holds
 |. max(c,min(d,a)) - max(c,min(d,b)) .| <= |. a-b .|;

theorem :: FUZZY_5:2
for x being Real holds
 |. sin x .| <= |.x.|;

theorem :: FUZZY_5:3
for x,y being Real holds |. sin x - sin y .| <= |.x-y.|;

theorem :: FUZZY_5:4
for x be Real st exp x = 1 holds x = 0;

theorem :: FUZZY_5:5
for a,b,p,q be Real st
a > 0 & p > 0 & (-b)/a < q/p
holds (-b)/a < (q-b)/(a+p) & (q-b)/(a+p) < q/p & (a*q+b*p)/(a+p) > 0;

theorem :: FUZZY_5:6
for a,b,p,q,s be Real st
a > 0 & p > 0 & (s-b)/a = (s-q)/(-p)
holds (s-b)/a= (q-b)/(a+p) & (s-q)/(-p) = (q-b)/(a+p);

theorem :: FUZZY_5:7
for a,b,p,q,s be Real st
a > 0 & p > 0 & (s-b)/a < (s-q)/(-p) holds
(s-b)/a < (q-b)/(a+p) & (q-b)/(a+p) < (s-q)/(-p);

begin :: The set of membership functions

definition
let X be non empty set;
func Membership_Funcs (X) -> set means
:: FUZZY_5:def 1
for f being object holds
 f in it iff f is Membership_Func of X;
end;

theorem :: FUZZY_5:8
for X be non empty set, x be object
st x in Membership_Funcs (X) holds
ex f be Membership_Func of X st x = f & dom f = X;

theorem :: FUZZY_5:9
Membership_Funcs (REAL)
= {f where f is Function of REAL,REAL : f is FuzzySet of REAL};

::::  characteristic function (indicator function)

theorem :: FUZZY_5:10
for A,X be non empty set holds
{chi (A,X)} c= Membership_Funcs (X);

theorem :: FUZZY_5:11
{chi([.a,b.],REAL) where a,b is Real : a <= b}
c= Membership_Funcs (REAL);

theorem :: FUZZY_5:12
{chi(A,REAL) where A is Subset of REAL : A c= REAL}
c= Membership_Funcs (REAL);

theorem :: FUZZY_5:13
{f where f is FuzzySet of REAL : ex A be Subset of REAL st f=chi(A,REAL) }
c= Membership_Funcs (REAL);

::::  membership functions using min (max) operation

theorem :: FUZZY_5:14
for f,g be Function of REAL,REAL, a being Real st
g is continuous & for x be Real holds f.x = min(a, g.x)
holds f is continuous;

theorem :: FUZZY_5:15 ::: TODO just: min (f,g) is continuous
for F,f,g be Function of REAL,REAL st
f is continuous & g is continuous &
for x be Real holds F.x = min(f.x, g.x)
holds
F is continuous;

theorem :: FUZZY_5:16  ::: should be restated in terms of lambda operators
for F,f,g be Function of REAL,REAL st
f is continuous & g is continuous &
for x be Real holds F.x = max(f.x, g.x)
holds
F is continuous;

theorem :: FUZZY_5:17
for f,g be Function of REAL,REAL,
a being Real st
g is continuous & for x be Real holds f.x= max(a, g.x)
holds f is continuous;

theorem :: FUZZY_5:18
for f,g be Function of REAL,REAL, a,b being Real st
g is continuous & for x be Real holds f.x= max(a,min(b, g.x))
holds f is continuous;

theorem :: FUZZY_5:19
for f,g be Function of REAL,REAL st
g is continuous & for x be Real holds f.x= max(0,min(1, g.x))
holds f is continuous;

theorem :: FUZZY_5:20
for f be Function of REAL,REAL, a,b be Real st
for th be Real holds f.th = 1/2*sin(a*th+b)+1/2
holds f is continuous;

theorem :: FUZZY_5:21
for f be Function of REAL,REAL, a,b be Real st
for x be Real holds f.x = 1/2*sin(a*x+b)+1/2
holds f is continuous;

theorem :: FUZZY_5:22
for r,s be Real, f be Function of REAL,REAL st
for x be Real holds f.x = max(r,min(s,x))
holds
f is Lipschitzian;

theorem :: FUZZY_5:23
for g be Function of REAL,REAL holds
{f where f is Function of REAL,REAL :
for x be Real holds f.x= min(1,max(0, g.x))}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:24
{f where f,g is Function of REAL,REAL :
for x be Real holds f.x= max(0,min(1, g.x))}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:25
for f,g be Function of REAL,REAL st
(for x be Real holds f.x= max(0,min(1, g.x)))
holds
f is FuzzySet of REAL;

theorem :: FUZZY_5:26
for f,g be Function of REAL,REAL st
(for x be Real holds f.x= min(1,max(0, g.x)))
holds f is FuzzySet of REAL;

::::  fuzzy Set from trigonometric function

theorem :: FUZZY_5:27
{f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= 1/2*sin(a*th+b)+1/2}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:28
{f where f is Function of REAL,REAL, a,b is Real:
       for th be Real holds f.th= 1/2*sin(a*th+b)+1/2}
c=Membership_Funcs (REAL);

theorem :: FUZZY_5:29
for a,b be Real, f be Function of REAL,REAL st
(for th be Real holds f.th= 1/2*sin(a*th+b)+1/2)
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:30
{f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= 1/2*cos(a*th+b)+1/2}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:31
for a,b be Real, f be Function of REAL,REAL st
(for th be Real holds f.th= 1/2*cos(a*th+b)+1/2)
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:32
for a,b be Real, f be FuzzySet of REAL st
(a<>0 & for th be Real holds f.th= 1/2*sin(a*th+b)+1/2)
holds
f is normalized;

theorem :: FUZZY_5:33
for f be FuzzySet of REAL st
f in {f where f is Function of REAL,REAL :
ex a,b be Real st a<>0 & for th be Real holds f.th= 1/2*sin(a*th+b)+1/2}
holds
f is normalized;

theorem :: FUZZY_5:34
for f be FuzzySet of REAL
for a,b be Real st a<>0 & for th be Real holds f.th= 1/2*cos(a*th+b)+1/2
holds
f is normalized;

theorem :: FUZZY_5:35
for f be FuzzySet of REAL st
f in {f where f is Function of REAL,REAL :
ex a,b be Real st a<>0 & for th be Real holds f.th= 1/2*cos(a*th+b)+1/2}
holds
f is normalized;

:::: periodicity of membership functions

theorem :: FUZZY_5:36
for F being Function of REAL,REAL, a,b,c,d being Real, i be Integer st
a<>0 & i<>0 & for x be Real holds F.x= max(0,min(1, c*sin(a*x+b)+d))
holds
F is (2 * PI)/a * i -periodic;

theorem :: FUZZY_5:37
for F being Function of REAL,REAL, a,b,c,d being Real st
for x be Real holds F.x= max(0,min(1, c*sin(a*x+b)+d))
holds
F is periodic;

theorem :: FUZZY_5:38
{f where f is Function of REAL,REAL :
ex a,b be Real st for th be Real holds f.th= max(0, sin(a*th+b))}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:39
for a,b be Real, f be Function of REAL,REAL st
(for x be Real holds f.x= max(0, sin(a*x+b)))
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:40
{f where f is Function of REAL,REAL :
ex a,b be Real st for x be Real holds f.x= max(0, cos(a*x+b))}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:41
for a,b be Real, f be Function of REAL,REAL st
(for x be Real holds f.x = max(0, cos(a*x+b)))
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:42
{f where f is Function of REAL,REAL, a,b,c,d is Real:
 for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))}
c= {f where f,g is Function of REAL,REAL :
    for x be Real holds f.x= max(0,min(1, g.x))};

theorem :: FUZZY_5:43
{f where f is Function of REAL,REAL, a,b,c,d is Real:
 for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:44
for f being Function of REAL,REAL, a,b,c,d being Real st
for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:45
{f where f is Function of REAL,REAL, a,b,c,d is Real:
 for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d))}
c= {f where f,g is Function of REAL,REAL :
    for x be Real holds f.x= max(0,min(1, g.x))};

theorem :: FUZZY_5:46
{f where f is Function of REAL,REAL, a,b,c,d is Real:
for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d))}
c= Membership_Funcs (REAL);

theorem :: FUZZY_5:47
for f being Function of REAL,REAL, a,b,c,d being Real st
for x be Real holds f.x= max(0,min(1, c*arctan(a*x+b)+d))
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:48
for f be Function of REAL,REAL, a,b,c,d,r,s be Real st
for x be Real holds f.x= max(r,min(s, c*sin(a*x+b)+d))
holds f is Lipschitzian;

theorem :: FUZZY_5:49
for f be Function of REAL,REAL, a,b,c,d be Real st
for x be Real holds f.x= max(0,min(1, c*sin(a*x+b)+d))
holds f is Lipschitzian;

:::: membership functions from Gaussian function

theorem :: FUZZY_5:50
for a,b be Real, f be Function of REAL,REAL st
(b <> 0 & for x be Real holds f.x= exp_R(-(x-a)^2/(2*b^2)))
holds
f is FuzzySet of REAL;

theorem :: FUZZY_5:51
for a,b be Real, f be Function of REAL,REAL st
(b <> 0 & for x be Real holds f.x= exp(-(x-a)^2/(2*b^2)))
holds
f is FuzzySet of REAL;

theorem :: FUZZY_5:52
for a,b be Real st b<>0 holds
{f where f is Function of REAL,REAL :
for x be Real holds f.x= exp(-(x-a)^2/(2*b^2))}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:53
for a,b be Real, f be FuzzySet of REAL st
(for x be Real holds f.x= exp(-(x-a)^2/(2*b^2)))
holds
f is normalized;

theorem :: FUZZY_5:54:: GauF02:
for a,b be Real, f be FuzzySet of REAL st
(b<>0 & for x be Real holds f.x= exp(-(x-a)^2/(2*b^2)))
holds
f is strictly-normalized;

theorem :: FUZZY_5:55
for a,b be Real, f be Function of REAL,REAL st
(b<>0 & for x be Real holds f.x= exp_R(-(x-a)^2/(2*b^2)))
holds
f is continuous;

theorem :: FUZZY_5:56
for a,b,c,r,s be Real, f be Function of REAL,REAL st
( b<>0 & for x be Real holds f.x= max(r,min(s, exp_R(-(x-a)^2/(2*b^2))+c)) )
holds
f is continuous;

theorem :: FUZZY_5:57
for a,b,c be Real, f be Function of REAL,REAL st
( b<>0 & for x be Real holds f.x= max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c)) )
holds
f is continuous;

theorem :: FUZZY_5:58
for a,b,c be Real, f be Function of REAL,REAL st
( b<>0 & for x be Real holds f.x= max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c)) )
holds
f is FuzzySet of REAL;

theorem :: FUZZY_5:59
{f where f is Function of REAL,REAL, a,b,c is Real:
 b <> 0 & for x be Real holds f.x= max(0,min(1, exp_R(-(x-a)^2/(2*b^2))+c))}
 c= Membership_Funcs (REAL);

:::: S or Z type Membership function

theorem :: FUZZY_5:60
for f be Function of REAL,REAL, a,b,r,s be Real st
for x be Real holds f.x= max(r,min(s, AffineMap (a,b).x))
holds f is Lipschitzian;

theorem :: FUZZY_5:61
for f be Function of REAL,REAL, a,b be Real st
for x be Real holds f.x= max(0,min(1, AffineMap (a,b).x))
holds f is Lipschitzian;

theorem :: FUZZY_5:62:: MM70:
for f be Function of REAL,REAL, a,b be Real st
for x be Real holds f.x= max(0,min(1, AffineMap (a,b).x))
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:63
{f where f is Function of REAL,REAL, a,b is Real:
 for x be Real holds f.x= max(0,min(1, AffineMap (a,b).x))}
 c= Membership_Funcs (REAL);

::::  symmetrical Triangular or Trapezoidal Fuzzy Sets

theorem :: FUZZY_5:64
for a,b be Real, f be Function of REAL,REAL st
(for x be Real holds f.x = max(0,1-|.(x-a)/b.|))
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:65
for a,b be Real st b > 0 holds
for x be Real holds
TriangularFS (a-b,a,a+b).x = max(0,1-|.(x-a)/b.|);

theorem :: FUZZY_5:66
for a,b be Real, f be FuzzySet of REAL st
b > 0 & (for x be Real holds f.x = max(0,1-|.(x-a)/b.|))
holds f is triangular;

theorem :: FUZZY_5:67:: TR8:
for a,b be Real, f be FuzzySet of REAL st
b > 0 & (for x be Real holds f.x = max(0,1-|.(x-a)/b.|))
holds f is strictly-normalized;

theorem :: FUZZY_5:68
for f be Function of REAL,REAL, a,b,c be Real st
(for x be Real holds f.x= max(0,min(1, c*(1-|.(x-a)/b.|))) )
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:69
for f be Function of REAL,REAL, a,b be Real st
b>0 & for x be Real holds f.x = max(0,1-|.(x-a)/b.|)
holds f is continuous;

theorem :: FUZZY_5:70
for f be Function of REAL,REAL, a,b,c,r,s be Real st
( b <> 0 & for x be Real holds f.x= max(r,min(s, c*(1-|.(x-a)/b.|))) )
holds f is Lipschitzian;

theorem :: FUZZY_5:71
for f be Function of REAL,REAL, a,b,c be Real st
( b <> 0 & for x be Real holds f.x= max(0,min(1, c*(1-|.(x-a)/b.|))) )
holds f is Lipschitzian;

theorem :: FUZZY_5:72
{f where f is Function of REAL,REAL, a,b is Real:
  b > 0 & for x be Real holds f.x = max(0,1-|.(x-a)/b.|)}
    c= Membership_Funcs (REAL);

theorem :: FUZZY_5:73
{f where f is Function of REAL,REAL, a,b,c,d is Real:
 b <> 0 & for x be Real holds f.x= max(0,min(1, c*(1-|.(x-a)/b.|)))}
 c= Membership_Funcs (REAL);

:::: asymmetry Trapezoidal or Triangular membership function

theorem :: FUZZY_5:74
for a,b,p,q,s be Real holds
( AffineMap (a,b)|].-infty,s.[ ) +* ( AffineMap (p,q)|[.s,+infty.[ )
is Function of REAL,REAL;

theorem :: FUZZY_5:75:: asymTT1:
for a,b,p,q be Real, f be Function of REAL,REAL st
for x be Real holds
f.x = max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a-p).[)) +*
                     ((AffineMap (p,q))|([.(q-b)/(a-p),+infty.[)) ) .x ))
holds f is FuzzySet of REAL;

theorem :: FUZZY_5:76
for a,b,c be Real st a<b & b<c holds
TriangularFS (a,b,c). a = 0 &
TriangularFS (a,b,c). b = 1 &
TriangularFS (a,b,c). c = 0;

theorem :: FUZZY_5:77
for a,b,c,d be Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d). a = 0 &
TrapezoidalFS (a,b,c,d). b = 1 &
TrapezoidalFS (a,b,c,d). c = 1 &
TrapezoidalFS (a,b,c,d). d = 0;

theorem :: FUZZY_5:78
for a,b,p,q be Real st
a > 0 & p > 0 & (-b)/a < q/p & (1-b)/a = (1-q)/(-p) holds
 for x be Real holds
(TriangularFS ((-b)/a,(1-b)/a,q/p)).x
= max(0,min(1, ((AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
                (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)).x  ));

theorem :: FUZZY_5:79
for a,b,p,q be Real st
a > 0 & p > 0 & (1-b)/a < (1-q)/(-p) holds
 for x be Real holds
(TrapezoidalFS ((-b)/a,(1-b)/a,(1-q)/(-p),q/p)).x
= max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
                 (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ));

theorem :: FUZZY_5:80
for a,b,p,q be Real, f be Function of REAL,REAL st a > 0 & p > 0 &
f = (AffineMap (a,b)|].-infty,(q-b)/(a+p).[) +*
   (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)
holds f is Lipschitzian;

theorem :: FUZZY_5:81
for a,b,p,q be Real st a > 0 & p > 0 holds
ex r being Real st
 ( 0 < r &
 ( for x1, x2 being Real st
x1 in dom ((AffineMap (a,b)|].-infty,(q-b)/(a+p).[)
         +* (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)) &
x2 in dom ((AffineMap (a,b)|].-infty,(q-b)/(a+p).[)
         +* (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)) holds
  |. ((AffineMap (a,b)|].-infty,(q-b)/(a+p).[)
         +* (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)) . x1
  - ((AffineMap (a,b)|].-infty,(q-b)/(a+p).[)
         +* (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[)) . x2.|
  <= r * |.(x1 - x2).| ) );

theorem :: FUZZY_5:82
for a,b,p,q,r,s be Real, f be Function of REAL,REAL st
a > 0 & p > 0 &
for x be Real holds
f.x = max(r,min(s, ( (AffineMap (a,b)|].-infty,(q-b)/(a+p).[) +*
                     (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ))
holds f is Lipschitzian;

theorem :: FUZZY_5:83
for a, b, c being Real st a < b & b < c holds
for x being Real holds
TriangularFS (a,b,c).x =
max(0,min(1, ( (AffineMap ( 1/(b-a),- a/(b-a) )|].-infty,b.[) +*
               (AffineMap ( - 1/(c-b),c/(c-b) )|[.b,+infty.[) ).x  ));

theorem :: FUZZY_5:84
for a, b, c, d being Real st a < b & b < c & c < d holds
for x being Real holds
TrapezoidalFS (a,b,c,d).x =
max(0,min(1, (
(AffineMap ( 1/(b-a),- a/(b-a) )|].-infty,(b*d-a*c)/(d-c+b-a).[) +*
(AffineMap ( - 1/(d-c),d/(d-c) )|[.(b*d-a*c)/(d-c+b-a),+infty.[) ).x  ));

theorem :: FUZZY_5:85
for a,b,p,q be Real, f be Function of REAL,REAL st
a > 0 & p > 0 &
for x be Real holds
f.x = max(0,min(1, ( ((AffineMap (a,b))|(].-infty,(q-b)/(a+p).[)) +*
                     ((AffineMap (-p,q))|([.(q-b)/(a+p),+infty.[)) ) .x ))
holds f is Lipschitzian;

theorem :: FUZZY_5:86
for a, b, c being Real st a < b & b < c holds
TriangularFS (a,b,c) is Lipschitzian;

theorem :: FUZZY_5:87
for a, b, c, d being Real st a < b & b < c & c < d holds
TrapezoidalFS (a,b,c,d) is Lipschitzian;

theorem :: FUZZY_5:88
for a,b,p,q be Real, f be FuzzySet of REAL st
a > 0 & p > 0 & (-b)/a < q/p & (1-b)/a = (1-q)/(-p) &
 for x be Real holds
f.x
= max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
                 (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ))
holds f is triangular & f is strictly-normalized;

theorem :: FUZZY_5:89
for a,b,p,q be Real, f be FuzzySet of REAL st
a > 0 & p > 0 & (1-b)/a < (1-q)/(-p) &
 for x be Real holds
f.x
= max(0,min(1, ( (AffineMap (a,b) |].-infty,(q-b)/(a+p).[) +*
                 (AffineMap (-p,q)|[.(q-b)/(a+p),+infty.[) ) .x ))
holds f is trapezoidal & f is normalized;

theorem :: FUZZY_5:90
{f where f is FuzzySet of REAL:f is triangular}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:91
{TriangularFS (a,b,c) where a,b,c is Real : a < b & b < c}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:92
{f where f is FuzzySet of REAL:f is trapezoidal}
 c= Membership_Funcs (REAL);

theorem :: FUZZY_5:93
{TrapezoidalFS (a,b,c,d) where a,b,c,d is Real : a < b & b < c & c < d}
 c= Membership_Funcs (REAL);