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

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