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