let X be non empty set ; :: thesis: for A being finite Subset of X
for R being being_linear-order Order of X holds len (SgmX R,A) = card A
let A be finite Subset of X; :: thesis: for R being being_linear-order Order of X holds len (SgmX R,A) = card A
let R be being_linear-order Order of X; :: thesis: len (SgmX R,A) = card A
A1: field R = X by ORDERS_1:100;
R linearly_orders field R by ORDERS_1:133;
hence len (SgmX R,A) = card A by A1, ORDERS_1:134, TRIANG_1:9; :: thesis: verum