let R be Relation; :: thesis: ( R is being_linear-order implies R ~ is being_linear-order )
assume ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) ; :: according to ORDERS_1:def 5 :: thesis: R ~ is being_linear-order
hence ( R ~ is reflexive & R ~ is transitive & R ~ is antisymmetric & R ~ is connected ) by Lm3, RELAT_2:27, RELAT_2:40, RELAT_2:42; :: according to ORDERS_1:def 5 :: thesis: verum