let R be Relation; :: thesis: for X being set st R partially_orders X holds
R quasi_orders X
let X be set ; :: thesis: ( R partially_orders X implies R quasi_orders X )
assume that
A1: R is_reflexive_in X and
A2: R is_transitive_in X and
R is_antisymmetric_in X ; :: according to ORDERS_1:def 7 :: thesis: R quasi_orders X
thus ( R is_reflexive_in X & R is_transitive_in X ) by A1, A2; :: according to ORDERS_1:def 6 :: thesis: verum