let R be Relation; :: thesis: ( R is being_quasi-order implies R quasi_orders field R )
assume that
A1: R is_reflexive_in field R and
A2: R is_transitive_in field R ; :: according to RELAT_2:def 9,RELAT_2:def 16,ORDERS_1:def 4 :: thesis: R quasi_orders field R
thus ( R is_reflexive_in field R & R is_transitive_in field R ) by A1, A2; :: according to ORDERS_1:def 7 :: thesis: verum