let X be set ; :: thesis: for A being empty Subset of X
for R being Order of X st R linearly_orders A holds
SgmX R,A = {}
let A be empty Subset of X; :: thesis: for R being Order of X st R linearly_orders A holds
SgmX R,A = {}
let R be Order of X; :: thesis: ( R linearly_orders A implies SgmX R,A = {} )
assume R linearly_orders A ; :: thesis: SgmX R,A = {}
then rng (SgmX R,A) = {} by TRIANG_1:def 2;
hence SgmX R,A = {} by RELAT_1:64; :: thesis: verum