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, PRE_POLY:18;
R is_reflexive_in X by A1, A2, RELAT_2:def 9;
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 connected & R is being_linear-order )
thus ( R is connected & R is being_linear-order ) by A1, ORDERS_1:def 6; :: thesis: verum