consider R being Relation such that
A1: R is well-ordering and
A2: field R = X by WELLSET1:9;
reconsider R = R as Relation of X by A2, Th4;
A3: R is connected by A1, WELLORD1:def 4;
R is reflexive by A1, WELLORD1:def 4;
then R is_reflexive_in X by A2, RELAT_2:def 9;
then dom R = X by ORDERS_1:98;
then reconsider R = R as Order of X by A1, PARTFUN1:def 4, WELLORD1:def 4;
take R ; :: thesis: ( R is being_linear-order & R is well-ordering )
thus ( R is being_linear-order & R is well-ordering ) by A1, A3, ORDERS_1:def 5; :: thesis: verum