consider r being Relation such that
A1: r well_orders {0,1,2,3,4} by WELLORD2:17;
take r |_2 {0,1,2,3,4} ; :: thesis: r |_2 {0,1,2,3,4} is well-ordering
thus r |_2 {0,1,2,3,4} is well-ordering by A1, WELLORD2:16; :: thesis: verum