let R be Relation; :: thesis: for X being set st R linearly_orders X holds
R |_2 X is being_linear-order
let X be set ; :: thesis: ( R linearly_orders X implies R |_2 X is being_linear-order )
assume ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X ) ; :: according to ORDERS_1:def 8 :: thesis: R |_2 X is being_linear-order
hence ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric & R |_2 X is connected ) by Lm6, Lm7, Lm8, Lm9; :: according to ORDERS_1:def 5 :: thesis: verum