set Q = R |_2 S;
A1: ( R |_2 S is total Relation of S & R |_2 S is reflexive & R |_2 S is transitive & R |_2 S is antisymmetric & R |_2 S is connected ) by Th6, WELLORD1:16, WELLORD1:17, WELLORD1:18;
then R |_2 S, RelIncl (order_type_of (R |_2 S)) are_isomorphic by WELLORD2:def 2;
then consider f being Function such that
A2: f is_isomorphism_of RelIncl (order_type_of (R |_2 S)),R |_2 S by WELLORD1:def 8, WELLORD1:40;
field (RelIncl (order_type_of (R |_2 S))) = order_type_of (R |_2 S) by WELLORD2:def 1;
then A3: dom f = order_type_of (R |_2 S) by A2;
A4: ( rng f = field (R |_2 S) & f is one-to-one ) by A2;
then order_type_of (R |_2 S), field (R |_2 S) are_equipotent by A3, WELLORD2:def 4;
then order_type_of (R |_2 S) is finite by CARD_1:38;
then reconsider f = f as XFinSequence by A3, AFINSQ_1:5;
field (R |_2 S) c= S by WELLORD1:13;
then reconsider f = f as XFinSequence of X by RELAT_1:def 19, A4, XBOOLE_1:1;
take f ; :: thesis: ( rng f = S & f is one-to-one & ( for i, j being Nat st i in dom f & j in dom f holds
( i <= j iff f . i,f . j in R ) ) )
thus A5: ( rng f = S & f is one-to-one ) by A4, A1, ORDERS_1:12; :: thesis: for i, j being Nat st i in dom f & j in dom f holds
( i <= j iff f . i,f . j in R )
let i, j be Nat; :: thesis: ( i in dom f & j in dom f implies ( i <= j iff f . i,f . j in R ) )
assume A6: ( i in dom f & j in dom f ) ; :: thesis: ( i <= j iff f . i,f . j in R )
then A7: ( f . i in S & f . j in S ) by A5, FUNCT_1:def 3;
( [i,j] in RelIncl (order_type_of (R |_2 S)) iff Segm i c= Segm j ) by A3, A6, WELLORD2:def 1;
then ( i <= j iff [(f . i),(f . j)] in R |_2 S ) by A2, A6, NAT_1:39;
then ( i <= j iff [(f . i),(f . j)] in R ) by A7, Th4;
hence ( i <= j iff f . i,f . j in R ) ; :: thesis: verum