let R be Relation; :: thesis: for X being set st R linearly_orders X holds
R ~ linearly_orders X
let X be set ; :: thesis: ( R linearly_orders X implies R ~ linearly_orders X )
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 ~ linearly_orders X
hence ( R ~ is_reflexive_in X & R ~ is_transitive_in X & R ~ is_antisymmetric_in X & R ~ is_connected_in X ) by Lm11, Lm12, Lm13, Lm14; :: according to ORDERS_1:def 8 :: thesis: verum