let a, b, c be Real; :: thesis: ( a < b & b < c & b - a = c - b implies centroid ((TriangularFS (a,b,c)),['a,c']) = b )
assume that
A1: ( a < b & b < c ) and
A2: b - a = c - b ; :: thesis: centroid ((TriangularFS (a,b,c)),['a,c']) = b
A4: b - a > a - a by A1, XREAL_1:9;
for x being Real holds (TriangularFS (a,b,c)) . x = max (0,(1 - |.((1 * (x - b)) / (b - a)).|))

proof

let x be Real; :: thesis: (TriangularFS (a,b,c)) . x = max (0,(1 - |.((1 * (x - b)) / (b - a)).|))
max (0,(1 - |.((x - b) / (b - a)).|)) = (TriangularFS ((b - (b - a)),b,(b + (b - a)))) . x by FUZZY_5:65, A4;
hence (TriangularFS (a,b,c)) . x = max (0,(1 - |.((1 * (x - b)) / (b - a)).|)) by A2; :: thesis: verum

end;

then centroid ((TriangularFS (a,b,c)),['(b - (b - a)),(b + (b - a))']) = b by Th19, A4;
hence centroid ((TriangularFS (a,b,c)),['a,c']) = b by A2; :: thesis: verum