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
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 Th15, Th16, Th17, Th18, Th24; :: according to WELLORD1:def 4 :: thesis: verum