let R be Relation; :: thesis: ( R is being_linear-order implies R linearly_orders field R )
assume ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R & R is_connected_in field R ) ; :: according to RELAT_2:def 9,RELAT_2:def 12,RELAT_2:def 14,RELAT_2:def 16,ORDERS_1:def 5 :: thesis: R linearly_orders field R
hence ( R is_reflexive_in field R & R is_transitive_in field R & R is_antisymmetric_in field R & R is_connected_in field R ) ; :: according to ORDERS_1:def 8 :: thesis: verum