let R be Relation; for X being set st R linearly_orders X holds
R |_2 X is being_linear-order
let X be set ; ( R linearly_orders X implies R |_2 X is being_linear-order )
assume that
A1:
R is_reflexive_in X
and
A2:
R is_transitive_in X
and
A3:
R is_antisymmetric_in X
and
A4:
R is_connected_in X
; ORDERS_1:def 8 R |_2 X is being_linear-order
thus
( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric & R |_2 X is connected )
by A1, A2, A3, A4, Lm6, Lm7, Lm8, Lm9; ORDERS_1:def 5 verum