let R be Relation; ( R is being_linear-order implies R linearly_orders field R )
assume that
A1:
R is_reflexive_in field R
and
A2:
R is_transitive_in field R
and
A3:
R is_antisymmetric_in field R
and
A4:
R is_connected_in field R
; RELAT_2:def 9,RELAT_2:def 12,RELAT_2:def 14,RELAT_2:def 16,ORDERS_1:def 6 R linearly_orders field R
thus
( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R & R is_connected_in field R )
by A1, A2, A3, A4; ORDERS_1:def 9 verum