A1: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 4;
defpred S₁[ set , set ] means ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = $1 & p . (len p) = $2 & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) );
set P = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) } ;
A2: for x, y being set holds
( [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) } iff ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) )

proof

let x, y be set ; :: thesis:

hereby :: thesis:

assume [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) } ; :: thesis:
then consider x1, y1 being Element of R such that
A3: [x,y] = [x1,y1] and
A4: ( x1 in the carrier of R & y1 in the carrier of R & S₁[x1,y1] ) ;
( x = x1 & y = y1 ) by A3, ZFMISC_1:33;
hence ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) by A4; :: thesis:

end;

thus ( x in the carrier of R & y in the carrier of R & S₁[x,y] implies [x,y] in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) } ) ; :: thesis:

end;

{ [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) } c= [:the carrier of R,the carrier of R:]

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A5: z in { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) } ; :: thesis:
consider x, y being Element of R such that
A6: ( z = [x,y] & x in the carrier of R & y in the carrier of R & S₁[x,y] ) by A5;
thus z in [:the carrier of R,the carrier of R:] by A6, ZFMISC_1:106; :: thesis:

end;

then reconsider P1 = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) } as Relation of the carrier of R ;

now

let x be set ; :: thesis:
assume A7: x in the carrier of R ; :: thesis:
S₁[x,x]

proof

set F = <*x,x*>;
A8: ( <*x,x*> . 1 = x & <*x,x*> . 2 = x ) by FINSEQ_1:61;
A9: len <*x,x*> = 2 by FINSEQ_1:61;
rng <*x,x*> = {x,x} by FINSEQ_2:147
.= {x} by ENUMSET1:69 ;
then rng <*x,x*> c= the carrier of R by A7, ZFMISC_1:37;
then reconsider F1 = <*x,x*> as FinSequence of the carrier of R by FINSEQ_1:def 4;
take F1 ; :: thesis:
thus 1 < len F1 by A9; :: thesis:
thus ( F1 . 1 = x & F1 . (len F1) = x ) by A9, FINSEQ_1:61; :: thesis:
let n1 be Nat; :: thesis:
assume A10: ( 2 <= n1 & n1 <= len F1 ) ; :: thesis:
n1 = 2 by A9, A10, XXREAL_0:1;
hence ( [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R or [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R ) by A1, A7, A8, RELAT_2:def 1; :: thesis:

end;

hence [x,x] in P1 by A7; :: thesis:

end;

then P1 is_reflexive_in the carrier of R by RELAT_2:def 1;
then A11: ( dom P1 = the carrier of R & field P1 = the carrier of R ) by ORDERS_1:98;

now

let x, y be set ; :: thesis:
assume A12: ( x in the carrier of R & y in the carrier of R & [x,y] in P1 ) ; :: thesis:
then consider p being FinSequence of the carrier of R such that
A13: ( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) by A2;
S₁[y,x]

proof

take F = Rev p; :: thesis:
A14: len F = len p by FINSEQ_5:def 3;
thus 1 < len F by A13, FINSEQ_5:def 3; :: thesis:
thus ( F . 1 = y & F . (len F) = x ) by A13, A14, FINSEQ_5:65; :: thesis:
let n1 be Nat; :: thesis:
assume A15: ( 2 <= n1 & n1 <= len F ) ; :: thesis:
A16: 1 <= n1 by A15, XXREAL_0:2;
A17: 2 - 1 <= n1 - 1 by A15, XREAL_1:11;
then reconsider n11 = n1 - 1 as Element of NAT by INT_1:16, XXREAL_0:2;
n1 - 1 <= (len F) - 0 by A15, XREAL_1:15;
then A18: n11 in dom p by A14, A17, FINSEQ_3:27;
then A19: ( n1 in dom p & n1 - 1 in dom p ) by A14, A15, A16, FINSEQ_3:27;
A20: F . (n1 - 1) = p . (((len p) - (n1 - 1)) + 1) by A18, FINSEQ_5:61
.= p . (((len p) - n1) + 2) ;
set n2 = ((len p) - n1) + 2;
0 <= (len p) - n1 by A14, A15, XREAL_1:50;
then A21: 2 + 0 <= ((len p) - n1) + 2 by XREAL_1:8;
(len p) - n1 <= (len p) - 2 by A15, XREAL_1:15;
then A22: ((len p) - n1) + 2 <= ((len p) - 2) + 2 by XREAL_1:8;
reconsider n2 = ((len p) - n1) + 2 as Element of NAT by A21, INT_1:16, XXREAL_0:2;
p . (n2 - 1) = p . (((len p) - n1) + (2 - 1))
.= F . n1 by A19, FINSEQ_5:61 ;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A13, A20, A21, A22; :: thesis:

end;

hence [y,x] in P1 by A12; :: thesis:

end;

then A23: P1 is_symmetric_in the carrier of R by RELAT_2:def 3;

now

let x, y, z be set ; :: thesis:
assume A24: ( x in the carrier of R & y in the carrier of R & z in the carrier of R & [x,y] in P1 & [y,z] in P1 ) ; :: thesis:
then ( S₁[x,y] & S₁[y,z] ) by A2;
then consider p1, p2 being FinSequence of the carrier of R such that
A25: ( 1 < len p1 & p1 . 1 = x & p1 . (len p1) = y & ( for n being Nat st 2 <= n & n <= len p1 & not [(p1 . n),(p1 . (n - 1))] in the InternalRel of R holds
[(p1 . (n - 1)),(p1 . n)] in the InternalRel of R ) ) and
A26: ( 1 < len p2 & p2 . 1 = y & p2 . (len p2) = z & ( for n being Nat st 2 <= n & n <= len p2 & not [(p2 . n),(p2 . (n - 1))] in the InternalRel of R holds
[(p2 . (n - 1)),(p2 . n)] in the InternalRel of R ) ) ;
S₁[x,z]

proof

take F = p1 ^ p2; :: thesis:
A27: len F = (len p1) + (len p2) by FINSEQ_1:35;
1 + 1 < (len p1) + (len p2) by A25, A26, XREAL_1:10;
hence 1 < len F by A27, XXREAL_0:2; :: thesis:
1 in dom p1 by A25, FINSEQ_3:27;
hence F . 1 = x by A25, FINSEQ_1:def 7; :: thesis:
len p2 in dom p2 by A26, FINSEQ_3:27;
hence F . (len F) = z by A26, A27, FINSEQ_1:def 7; :: thesis:
let n1 be Nat; :: thesis:
assume A28: ( 2 <= n1 & n1 <= len F ) ; :: thesis:
A29: 1 <= n1 by A28, XXREAL_0:2;
A30: 2 - 1 <= n1 - 1 by A28, XREAL_1:11;
then reconsider n11 = n1 - 1 as Element of NAT by INT_1:16, XXREAL_0:2;
A31: n1 - 1 <= (len F) - 0 by A28, XREAL_1:15;
A32: ( not (len p1) + 1 <= n1 or (len p1) + 1 = n1 or (len p1) + 1 < n1 ) by XXREAL_0:1;

per cases by A32, INT_1:20;

suppose A33: n1 <= len p1 ; :: thesis:

then A34: n1 in dom p1 by A29, FINSEQ_3:27;
n1 - 1 <= (len p1) - 0 by A33, XREAL_1:15;
then n11 in dom p1 by A30, FINSEQ_3:27;
then ( F . n1 = p1 . n1 & F . (n1 - 1) = p1 . (n1 - 1) ) by A34, FINSEQ_1:def 7;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A25, A28, A33; :: thesis:

end;

suppose A35: (len p1) + 1 < n1 ; :: thesis:

len p1 < (len p1) + 1 by XREAL_1:31;
then A36: len p1 < n1 by A35, XXREAL_0:2;
((len p1) + 1) - 1 < n1 - 1 by A35, XREAL_1:11;
then A37: F . n11 = p2 . (n11 - (len p1)) by A31, FINSEQ_1:37;
reconsider k = n1 - (len p1) as Element of NAT by A36, INT_1:16, XREAL_1:50;
A38: ( F . n1 = p2 . k & F . (n1 - 1) = p2 . (k - 1) ) by A28, A36, A37, FINSEQ_1:37;
1 < n1 - (len p1) by A35, XREAL_1:22;
then A39: 1 + 1 <= n1 - (len p1) by INT_1:20;
n1 <= (len p1) + (len p2) by A28, FINSEQ_1:35;
then ( 2 <= k & k <= len p2 ) by A39, XREAL_1:22;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A26, A38; :: thesis:

end;

suppose A40: (len p1) + 1 = n1 ; :: thesis:

A41: len p1 in dom p1 by A25, FINSEQ_3:27;
A42: (len p1) + 1 <= (len p1) + (len p2) by A26, XREAL_1:10;
A43: F . (n1 - 1) = y by A25, A40, A41, FINSEQ_1:def 7;
((len p1) + 1) - (len p1) = 1 ;
then F . n1 = y by A26, A40, A42, FINSEQ_1:36;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A1, A24, A43, RELAT_2:def 1; :: thesis:

end;

hence [x,z] in P1 by A24; :: thesis:

end;

then P1 is_transitive_in the carrier of R by RELAT_2:def 8;
then reconsider P1 = { [x,y] where x, y is Element of R : ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) } as Equivalence_Relation of the carrier of R by A11, A23, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16;
take P1 ; :: thesis:
thus for x, y being set holds
( [x,y] in P1 iff ( x in the carrier of R & y in the carrier of R & ex p being FinSequence of the carrier of R st
( 1 < len p & p . 1 = x & p . (len p) = y & ( for n being Nat st 2 <= n & n <= len p & not [(p . n),(p . (n - 1))] in the InternalRel of R holds
[(p . (n - 1)),(p . n)] in the InternalRel of R ) ) ) ) by A2; :: thesis: