theorem Lm223: :: FUZZY_8:21

for a, b, c, d being Real st b > 0 & c > 0 & d > 0 & d < b holds
centroid ((d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))),['(a - c),(a + c)']) = a