:: Some Properties of Membership Functions Composed of Triangle Functions and Piecewise Linear Functions
:: by Takashi Mitsuishi
::
:: Copyright (c) 2021 Association of Mizar Users

ABS1: for x, y being Real st x >= 0 & x <= y holds
|.x.| <= |.y.|

by TOPREAL6:2;

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

theorem LmSin1: :: FUZZY_5:2
for x being Real holds |.(sin x).| <= |.x.|
proof end;

theorem LmSin2: :: FUZZY_5:3
for x, y being Real holds |.((sin x) - (sin y)).| <= |.(x - y).|
proof end;

EXpReq11: for x being Real st exp_R x = 1 holds
x = 0

by SIN_COS7:29;

theorem EXpReq12: :: FUZZY_5:4
for x being Real st exp x = 1 holds
x = 0
proof end;

theorem asymTT2: :: FUZZY_5:5
for a, b, p, q being 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 )
proof end;

theorem asymTT3: :: FUZZY_5:6
for a, b, p, q, s being 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) )
proof end;

theorem asymTT4: :: FUZZY_5:7
for a, b, p, q, s being 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) )
proof end;

definition
let X be non empty set ;
func Membership_Funcs X -> set means :Def1: :: FUZZY_5:def 1
for f being object holds
( f in it iff f is Membership_Func of X );
existence
ex b1 being set st
for f being object holds
( f in b1 iff f is Membership_Func of X )
proof end;
uniqueness
for b1, b2 being set st ( for f being object holds
( f in b1 iff f is Membership_Func of X ) ) & ( for f being object holds
( f in b2 iff f is Membership_Func of X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Membership_Funcs FUZZY_5:def 1 :
for X being non empty set
for b2 being set holds
( b2 = Membership_Funcs X iff for f being object holds
( f in b2 iff f is Membership_Func of X ) );

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

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

:::: characteristic function (indicator function)
theorem :: FUZZY_5:10
for A, X being non empty set holds {(chi (A,X))} c= Membership_Funcs X
proof end;

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

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

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

:::: membership functions using min (max) operation
theorem MMcon1: :: FUZZY_5:14
for f, g being Function of REAL,REAL
for a being Real st g is continuous & ( for x being Real holds f . x = min (a,(g . x)) ) holds
f is continuous
proof end;

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

theorem MMcon2: :: FUZZY_5:16
for F, f, g being Function of REAL,REAL st f is continuous & g is continuous & ( for x being Real holds F . x = max ((f . x),(g . x)) ) holds
F is continuous
proof end;

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

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

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

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

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

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

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

MM4: for g being Function of REAL,REAL holds { f where f is Function of REAL,REAL : for x being Real holds f . x = max (0,(min (1,(g . x)))) } c= Membership_Funcs REAL
proof end;

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

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

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

:::: fuzzy Set from trigonometric function
theorem :: FUZZY_5:27
{ f where f is Function of REAL,REAL : ex a, b being Real st
for th being Real holds f . th = ((1 / 2) * (sin ((a * th) + b))) + (1 / 2)
}
c= Membership_Funcs REAL
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: FUZZY_5:42
{ f where f is Function of REAL,REAL, a, b, c, d is Real : for x being 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 being Real holds f . x = max (0,(min (1,(g . x)))) }
proof end;

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

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

theorem MM60: :: FUZZY_5:45
{ f where f is Function of REAL,REAL, a, b, c, d is Real : for x being 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 being Real holds f . x = max (0,(min (1,(g . x)))) }
proof end;

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

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

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

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

:::: membership functions from Gaussian function
theorem GauF04: :: FUZZY_5:50
for a, b being Real
for f being Function of REAL,REAL st b <> 0 & ( for x being Real holds f . x = exp_R (- (((x - a) ^2) / (2 * (b ^2)))) ) holds
f is FuzzySet of REAL
proof end;

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

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

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

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

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

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

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

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

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

:::: S or Z type Membership function
theorem MMLip3: :: FUZZY_5:60
for f being Function of REAL,REAL
for a, b, r, s being Real st ( for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . x)))) ) holds
f is Lipschitzian
proof end;

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

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

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

:::: symmetrical Triangular or Trapezoidal Fuzzy Sets
theorem :: FUZZY_5:64
for a, b being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) holds
f is FuzzySet of REAL
proof end;

LmABS: for a, x being Real st 0 <= a holds
( ( x <= - a or a <= x ) iff a <= |.x.| )

proof end;

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

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

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

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

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

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

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

TR2XX: { (TriangularFS (a,b,c)) where a, b, c is Real : ( a < b & b < c ) } c= Membership_Funcs REAL
proof end;

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

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

:::: asymmetry Trapezoidal or Triangular membership function
theorem asymTT10: :: FUZZY_5:74
for a, b, p, q, s being Real holds ((AffineMap (a,b)) | ) +* ((AffineMap (p,q)) | ) is Function of REAL,REAL
proof end;

theorem :: FUZZY_5:75
for a, b, p, q being Real
for f being Function of REAL,REAL st ( for x being 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
proof end;

theorem TrAng1: :: FUZZY_5:76
for a, b, c being 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 )
proof end;

theorem TrZoi1: :: FUZZY_5:77
for a, b, c, d being 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 )
proof end;

theorem asymTT6: :: FUZZY_5:78
for a, b, p, q being Real st a > 0 & p > 0 & (- b) / a < q / p & (1 - b) / a = (1 - q) / (- p) holds
for x being 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))))
proof end;

theorem asymTT7: :: FUZZY_5:79
for a, b, p, q being Real st a > 0 & p > 0 & (1 - b) / a < (1 - q) / (- p) holds
for x being 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))))
proof end;

theorem asymTT50: :: FUZZY_5:80
for a, b, p, q being Real
for f being 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
proof end;

theorem asymTT51: :: FUZZY_5:81
for a, b, p, q being 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).| ) )
proof end;

theorem asymTT5: :: FUZZY_5:82
for a, b, p, q, r, s being Real
for f being Function of REAL,REAL st a > 0 & p > 0 & ( for x being 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
proof end;

theorem asymTT9: :: 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))))) | ) +* ((AffineMap ((- (1 / (c - b))),(c / (c - b)))) | )) . x))))
proof end;

theorem asymTT8: :: 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))))
proof end;

theorem :: FUZZY_5:85
for a, b, p, q being Real
for f being Function of REAL,REAL st a > 0 & p > 0 & ( for x being 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 by asymTT5;

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

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
proof end;

theorem :: FUZZY_5:88
for a, b, p, q being Real
for f being FuzzySet of REAL st a > 0 & p > 0 & (- b) / a < q / p & (1 - b) / a = (1 - q) / (- p) & ( for x being 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 )
proof end;

theorem :: FUZZY_5:89
for a, b, p, q being Real
for f being FuzzySet of REAL st a > 0 & p > 0 & (1 - b) / a < (1 - q) / (- p) & ( for x being 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 )
proof end;

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

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

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

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
proof end;