let a, c be Real; :: thesis: for f being Function of REAL,REAL st c > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / c).|)) ) holds
f is triangular FuzzySet of REAL
let f be Function of REAL,REAL; :: thesis: ( c > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / c).|)) ) implies f is triangular FuzzySet of REAL )
assume B1: c > 0 ; :: thesis: ( ex x being Real st not f . x = max (0,(1 - |.((x - a) / c).|)) or f is triangular FuzzySet of REAL )
assume A1: for x being Real holds f . x = max (0,(1 - |.((x - a) / c).|)) ; :: thesis: f is triangular FuzzySet of REAL
deffunc H₁( Element of REAL ) -> Element of REAL = In ((1 - |.(($1 - a) / c).|),REAL);
consider h being Function of REAL,REAL such that
A3: for x being Element of REAL holds h . x = H₁(x) from FUNCT_2:sch 4();
A5: for x being Real holds f . x = max (0,(min (1,(h . x))))

proof

let x be Real; :: thesis: f . x = max (0,(min (1,(h . x))))
reconsider x = x as Element of REAL by XREAL_0:def 1;
A4: h . x = In ((1 - |.((x - a) / c).|),REAL) by A3;
then h . x <= 1 by XREAL_1:43, COMPLEX1:46;
then max (0,(min (1,(h . x)))) = max (0,(1 - |.((x - a) / c).|)) by A4, XXREAL_0:def 9
.= f . x by A1 ;
hence f . x = max (0,(min (1,(h . x)))) ; :: thesis: verum

end;

reconsider f = f as FuzzySet of REAL by FUZZY_5:25, A5;
thus f is triangular FuzzySet of REAL by FUZZY_5:25, A5, FUZZY_5:66, B1, A1; :: thesis: verum