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 Def2;
hence SgmX (R,A) = {} ; :: thesis: verum