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 )
assume A1: R is being_linear-order ; :: thesis: R linearly_orders S
S c= X ;
then S c= field R by ORDERS_1:100;
hence R linearly_orders S by A1, ORDERS_1:133, ORDERS_1:134; :: thesis: verum