let Y be set ; :: thesis: for R being Relation st R is well-ordering holds
R |_2 Y is well-ordering
let R be Relation; :: thesis: ( R is well-ordering implies R |_2 Y is well-ordering )
assume R is well-ordering ; :: thesis: R |_2 Y is well-ordering
then ( R is reflexive & R is transitive & R is connected & R is antisymmetric & R is well_founded ) by Def4;
hence ( R |_2 Y is reflexive & R |_2 Y is transitive & R |_2 Y is antisymmetric & R |_2 Y is connected & R |_2 Y is well_founded ) by Th22, Th23, Th24, Th25, Th31; :: according to WELLORD1:def 4 :: thesis: verum