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

proof

let x, y be object ; :: thesis: ( x in S & y in S & x <> y & not [x,y] in R implies [y,x] in R )
assume that
A6: x in S and
A7: y in S and
A8: x <> y ; :: thesis: ( [x,y] in R or [y,x] in R )
A9: field R = (dom R) \/ (rng R) by RELAT_1:def 6;
[y,y] in R by A2, A7, RELAT_2:def 1;
then y in dom R by XTUPLE_0:def 12;
then A10: y in field R by A9, XBOOLE_0:def 3;
[x,x] in R by A2, A6, RELAT_2:def 1;
then x in dom R by XTUPLE_0:def 12;
then x in field R by A9, XBOOLE_0:def 3;
hence ( [x,y] in R or [y,x] in R ) by A5, A8, A10, RELAT_2:def 6; :: thesis: verum

end;

then A11: R is_connected_in S by RELAT_2:def 6;
for x being object st x in S holds
[x,x] in R by A2, RELAT_2:def 1;
then R is_reflexive_in S by RELAT_2:def 1;
hence R linearly_orders S by A4, A3, A11, ORDERS_1:def 9; :: thesis: verum