let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st b > 1 & c > 0 & ( for x being Real holds f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) ) holds
f is trapezoidal FuzzySet of REAL
let f be Function of REAL,REAL; :: thesis: ( b > 1 & c > 0 & ( for x being Real holds f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) ) implies f is trapezoidal FuzzySet of REAL )
assume A1: b > 1 ; :: thesis: ( not c > 0 or ex x being Real st not f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) or f is trapezoidal FuzzySet of REAL )
assume A2: c > 0 ; :: thesis: ( ex x being Real st not f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) or f is trapezoidal FuzzySet of REAL )
assume A3: for x being Real holds f . x = min (1,(max (0,(b - |.((b * (x - a)) / c).|)))) ; :: thesis: f is trapezoidal FuzzySet of REAL
reconsider f = f as FuzzySet of REAL by Lm1, A1, A3;
A4: ((1 - (b + ((a * b) / c))) / (- (b / c))) - ((1 - (b - ((a * b) / c))) / (b / c)) = ((- (1 - (b + ((a * b) / c)))) / (b / c)) - ((1 - (b - ((a * b) / c))) / (b / c)) by XCMPLX_1:192
.= ((- (1 - (b + ((a * b) / c)))) - (1 - (b - ((a * b) / c)))) / (b / c) by XCMPLX_1:120
.= ((2 * b) - 2) / (b / c) ;
b - 1 > 1 - 1 by A1, XREAL_1:9;
then 2 * (b - 1) > 0 ;
then B2: 0 + ((1 - (b - ((a * b) / c))) / (b / c)) < (((1 - (b + ((a * b) / c))) / (- (b / c))) - ((1 - (b - ((a * b) / c))) / (b / c))) + ((1 - (b - ((a * b) / c))) / (b / c)) by XREAL_1:29, A4, A1, A2;
for x being Real holds f . x = max (0,(min (1,((((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))).[) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))),+infty.[)) . x))))

proof

let x be Real; :: thesis: f . x = max (0,(min (1,((((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))).[) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))),+infty.[)) . x))))
C2: ((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c)) = (((b + ((a * b) / c)) - b) + ((a * b) / c)) / ((b / c) + (b / c))
.= ((a * (b / c)) + ((a * b) / c)) / ((b / c) + (b / c)) by XCMPLX_1:74
.= ((a * (b / c)) + (a * (b / c))) / ((b / c) + (b / c)) by XCMPLX_1:74
.= (a * ((b / c) + (b / c))) / ((b / c) + (b / c))
.= a by XCMPLX_1:89, A1, A2 ;
C1: (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))).[) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))),+infty.[)) . x = (((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,a.]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.a,+infty.[)) . x by FUZZY_6:35, C2
.= b - |.((b * (x - a)) / c).| by Th1, A1, A2 ;
set F = (AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))).[;
set G = (AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))),+infty.[;
thus f . x = min (1,(max (0,((((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))).[) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))),+infty.[)) . x)))) by C1, A3
.= max (0,(min (1,((((AffineMap ((b / c),(b - ((a * b) / c)))) | ].-infty,(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))).[) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) + (b / c))),+infty.[)) . x)))) by XXREAL_0:37 ; :: thesis: verum

end;

hence f is trapezoidal FuzzySet of REAL by FUZZY_5:89, A1, A2, B2; :: thesis: verum