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 )
A1: field R = X by ORDERS_1:12;
A3: for x, y, z being object st x in S & y in S & z in S & [x,y] in R & [y,z] in R holds
[x,z] in R by A1, RELAT_2:def 8, RELAT_2:def 16;
A4: for x, y being object st x in S & y in S & [x,y] in R & [y,x] in R holds
x = y by A1, RELAT_2:def 4, RELAT_2:def 12;
assume R is being_linear-order ; :: thesis: R linearly_orders S
then A2: for x, y being object st x in S & y in S & x <> y & not [x,y] in R holds
[y,x] in R by A1, RELAT_2:def 14, RELAT_2:def 6;
for x being object st x in S holds
[x,x] in R by A1, RELAT_2:def 1, RELAT_2:def 9;
hence R linearly_orders S by A4, A3, A2, RELAT_2:def 6, RELAT_2:def 1, RELAT_2:def 4, RELAT_2:def 8; :: thesis: verum