consider r being Relation such that
A1: r well_orders 5 by WELLORD2:17;
take r |_2 5 ; :: thesis: r |_2 5 is well-ordering
thus r |_2 5 is well-ordering by A1, WELLORD2:16; :: thesis: verum