theorem :: PRE_POLY:76

for X being set
for A being empty Subset of X
for R being Order of X st R linearly_orders A holds
SgmX (R,A) = {}