consider R being Relation such that
A1: R is well-ordering and
A2: field R = X by WELLSET1:6;
reconsider R = R as Relation of X by A2, Th17;
R is reflexive by A1;
then R is_reflexive_in X by A2;
then dom R = X by ORDERS_1:13;
then reconsider R = R as Order of X by A1, PARTFUN1:def 2;
take R ; :: thesis: ( R is being_linear-order & R is well-ordering )
thus ( R is being_linear-order & R is well-ordering ) by A1, ORDERS_1:def 6; :: thesis: verum