let a, b be Real; :: thesis:
let f be FuzzySet of REAL; :: thesis:
assume A1: b > 0 ; :: thesis:
assume A2: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: thesis:
ex x being Element of REAL st
( f . x = 1 & ( for y being Element of REAL st f . y = 1 holds
y = x ) )

A4: a is Element of REAL by XREAL_0:def 1;
take a ; :: thesis:
A3: f . a = max (0,(1 - |.((a - a) / b).|)) by A2
.= max (0,(1 - 0)) by ABSVALUE:def 1
.= 1 by XXREAL_0:def 10 ;
for y being Element of REAL st f . y = 1 holds
y = a

let y be Element of REAL ; :: thesis:
assume f . y = 1 ; :: thesis:
then max (0,(1 - |.((y - a) / b).|)) = 1 by A2;
then 1 - |.((y - a) / b).| = 1 by XXREAL_0:16;
then y - a = 0 by A1, ABSVALUE:2;
hence y = a ; :: thesis:

end;

hence ( a is set & a is Element of REAL & f . a = 1 & ( for y being Element of REAL st f . y = 1 holds
y = a ) ) by A4, A3; :: thesis:

end;