let f be Function of REAL,REAL; :: thesis: 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
let a, b, c be Real; :: thesis: ( ( for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ) implies f is FuzzySet of REAL )
assume A2: for x being Real holds f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) ; :: thesis: f is FuzzySet of REAL
ex g being Function of REAL,REAL st
for x being Real holds g . x = c * (1 - |.((x - a) / b).|)

proof

deffunc H₁( Element of REAL ) -> Element of REAL = In ((c * (1 - |.(($1 - a) / b).|)),REAL);
consider f being Function of REAL,REAL such that
A1: for x being Element of REAL holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for x being Real holds f . x = c * (1 - |.((x - a) / b).|)
for x being Real holds f . x = c * (1 - |.((x - a) / b).|)

proof

let x be Real; :: thesis: f . x = c * (1 - |.((x - a) / b).|)
reconsider x = x as Element of REAL by XREAL_0:def 1;
f . x = H₁(x) by A1;
hence f . x = c * (1 - |.((x - a) / b).|) ; :: thesis: verum

end;

hence for x being Real holds f . x = c * (1 - |.((x - a) / b).|) ; :: thesis: verum

end;

then consider g being Function of REAL,REAL such that
A4: for x being Real holds g . x = c * (1 - |.((x - a) / b).|) ;
for x being Real holds f . x = max (0,(min (1,(g . x))))

proof

let x be Real; :: thesis: f . x = max (0,(min (1,(g . x))))
f . x = max (0,(min (1,(c * (1 - |.((x - a) / b).|))))) by A2
.= max (0,(min (1,(g . x)))) by A4 ;
hence f . x = max (0,(min (1,(g . x)))) ; :: thesis: verum

end;

hence f is FuzzySet of REAL by MM40; :: thesis: verum