let a, b be Real; :: thesis: 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

let f be FuzzySet of REAL; :: thesis: ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) implies f is triangular )

assume A1: b > 0 ; :: thesis: ( ex x being Real st not f . x = max (0,(1 - |.((x - a) / b).|)) or f is triangular )

assume A2: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: thesis: f is triangular

take a - b ; :: according to FUZNUM_1:def 9 :: thesis: not for b_{1}, b_{2} being object holds R32( REAL , REAL ,f, TriangularFS ((a - b),b_{1},b_{2}))

take a ; :: thesis: not for b_{1} being object holds R32( REAL , REAL ,f, TriangularFS ((a - b),a,b_{1}))

take a + b ; :: thesis: R32( REAL , REAL ,f, TriangularFS ((a - b),a,(a + b)))

A4: ( dom (TriangularFS ((a - b),a,(a + b))) = REAL & dom f = REAL ) by FUNCT_2:def 1;

for x being object st x in dom f holds

f . x = (TriangularFS ((a - b),a,(a + b))) . x

f is triangular

let f be FuzzySet of REAL; :: thesis: ( b > 0 & ( for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ) implies f is triangular )

assume A1: b > 0 ; :: thesis: ( ex x being Real st not f . x = max (0,(1 - |.((x - a) / b).|)) or f is triangular )

assume A2: for x being Real holds f . x = max (0,(1 - |.((x - a) / b).|)) ; :: thesis: f is triangular

take a - b ; :: according to FUZNUM_1:def 9 :: thesis: not for b

take a ; :: thesis: not for b

take a + b ; :: thesis: R32( REAL , REAL ,f, TriangularFS ((a - b),a,(a + b)))

A4: ( dom (TriangularFS ((a - b),a,(a + b))) = REAL & dom f = REAL ) by FUNCT_2:def 1;

for x being object st x in dom f holds

f . x = (TriangularFS ((a - b),a,(a + b))) . x

proof

hence
R32( REAL , REAL ,f, TriangularFS ((a - b),a,(a + b)))
by FUNCT_1:2, A4; :: thesis: verum
let x be object ; :: thesis: ( x in dom f implies f . x = (TriangularFS ((a - b),a,(a + b))) . x )

assume x in dom f ; :: thesis: f . x = (TriangularFS ((a - b),a,(a + b))) . x

then reconsider x = x as Real by A4;

f . x = max (0,(1 - |.((x - a) / b).|)) by A2

.= (TriangularFS ((a - b),a,(a + b))) . x by A1, TR6 ;

hence f . x = (TriangularFS ((a - b),a,(a + b))) . x ; :: thesis: verum

end;assume x in dom f ; :: thesis: f . x = (TriangularFS ((a - b),a,(a + b))) . x

then reconsider x = x as Real by A4;

f . x = max (0,(1 - |.((x - a) / b).|)) by A2

.= (TriangularFS ((a - b),a,(a + b))) . x by A1, TR6 ;

hence f . x = (TriangularFS ((a - b),a,(a + b))) . x ; :: thesis: verum