theorem LmSymTrape2: :: FUZZY_7:44

for a, b, c, d, r being Real st a < b & b < c & c < d holds
(((AffineMap ((1 / (b - a)),(- (a / (b - a))))) | [.a,b.]) +* ((AffineMap (0,1)) | [.b,c.])) +* ((AffineMap ((- (1 / (d - c))),(d / (d - c)))) | [.c,d.]) = (TrapezoidalFS (a,b,c,d)) | [.a,d.]