let R be Relation; :: thesis: for X being set st R is being_partial-order holds
R |_2 X is being_partial-order
let X be set ; :: thesis: ( R is being_partial-order implies R |_2 X is being_partial-order )
assume that
A1: R is reflexive and
A2: R is transitive and
A3: R is antisymmetric ; :: according to ORDERS_1:def 4 :: thesis: R |_2 X is being_partial-order
thus ( R |_2 X is reflexive & R |_2 X is transitive & R |_2 X is antisymmetric ) by A1, A2, A3, WELLORD1:15, WELLORD1:17, WELLORD1:18; :: according to ORDERS_1:def 4 :: thesis: verum