theorem Th63: :: ORDERS_5:52

for A being Preorder
for f being finite-support Function of A,REAL holds support (eqSumOf f) c= (proj A) .: (support f)