:: deftheorem defines being_linear-order ORDERS_1:def 6 :
for R being Relation holds
( R is being_linear-order iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected ) );