let X be set ; 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; for R being Order of X st R is being_linear-order holds
R linearly_orders S
let R be Order of X; ( 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
; 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 ;
( 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
;
( [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;
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; verum