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
; ( 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; 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; ( 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 )
; ( 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 )
; verum