let X be set ; :: thesis: for S being Subset of X
for R being Order of X st R is being_linear-order holds
R linearly_orders S
let S be Subset of X; :: thesis: for R being Order of X st R is being_linear-order holds
R linearly_orders S
let R be Order of X; :: thesis: ( R is being_linear-order implies R linearly_orders S )
S c= X ;
then A1: S c= field R by ORDERS_1:15;
assume R is being_linear-order ; :: thesis: R linearly_orders S
hence R linearly_orders S by A1, ORDERS_1:37, ORDERS_1:38; :: thesis: verum