let R be Relation; :: thesis: ( R is being_linear-order implies R ~ is being_linear-order )
assume that
A1: R is reflexive and
A2: R is transitive and
A3: R is antisymmetric and
A4: R is connected ; :: according to ORDERS_1:def 5 :: thesis: R ~ is being_linear-order
thus ( R ~ is reflexive & R ~ is transitive & R ~ is antisymmetric & R ~ is connected ) by A1, A2, A3, A4, Lm3, RELAT_2:10, RELAT_2:23, RELAT_2:25; :: according to ORDERS_1:def 5 :: thesis: verum