defpred S₁[ object , object ] 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] ) } ;
{ [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:]

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume 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:
then ex x, y being Element of R st
( z = [x,y] & x in the carrier of R & y in the carrier of R & S₁[x,y] ) ;
hence z in [: the carrier of R, the carrier of R:] by ZFMISC_1:87; :: 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 ;
A1: for x, y being object 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 object ; :: 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
A2: [x,y] = [x1,y1] and
x1 in the carrier of R and
y1 in the carrier of R and
A3: S₁[x1,y1] ;
( x = x1 & y = y1 ) by A2, XTUPLE_0:1;
hence ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) by A3; :: 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;

now :: thesis:

let x, y be object ; :: thesis:
assume that
A4: ( x in the carrier of R & y in the carrier of R ) and
A5: [x,y] in P1 ; :: thesis:
consider p being FinSequence of the carrier of R such that
A6: 1 < len p and
A7: ( p . 1 = x & p . (len p) = y ) and
A8: 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 A1, A5;
S₁[y,x]

proof

take F = Rev p; :: thesis:
thus 1 < len F by A6, FINSEQ_5:def 3; :: thesis:
A9: len F = len p by FINSEQ_5:def 3;
hence ( F . 1 = y & F . (len F) = x ) by A7, FINSEQ_5:62; :: thesis:
let n1 be Nat; :: thesis:
assume that
A10: 2 <= n1 and
A11: n1 <= len F ; :: thesis:
1 <= n1 by A10, XXREAL_0:2;
then A12: n1 in dom p by A9, A11, FINSEQ_3:25;
set n2 = ((len p) - n1) + 2;
0 <= (len p) - n1 by A9, A11, XREAL_1:48;
then A13: 2 + 0 <= ((len p) - n1) + 2 by XREAL_1:6;
A14: 2 - 1 <= n1 - 1 by A10, XREAL_1:9;
then reconsider n11 = n1 - 1 as Element of NAT by INT_1:3, XXREAL_0:2;
n1 - 1 <= (len F) - 0 by A11, XREAL_1:13;
then n11 in dom p by A9, A14, FINSEQ_3:25;
then A15: F . (n1 - 1) = p . (((len p) - (n1 - 1)) + 1) by FINSEQ_5:58
.= p . (((len p) - n1) + 2) ;
reconsider n2 = ((len p) - n1) + 2 as Element of NAT by A13, INT_1:3, XXREAL_0:2;
(len p) - n1 <= (len p) - 2 by A10, XREAL_1:13;
then A16: ((len p) - n1) + 2 <= ((len p) - 2) + 2 by XREAL_1:6;
p . (n2 - 1) = p . (((len p) - n1) + (2 - 1))
.= F . n1 by A12, FINSEQ_5:58 ;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A8, A15, A13, A16; :: thesis:

end;

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

end;

then A17: P1 is_symmetric_in the carrier of R by RELAT_2:def 3;
A18: the InternalRel of R is_reflexive_in the carrier of R by ORDERS_2:def 2;

now :: thesis:

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

proof

set F = <*x,x*>;
rng <*x,x*> = {x,x} by FINSEQ_2:127
.= {x} by ENUMSET1:29 ;
then rng <*x,x*> c= the carrier of R by A19, ZFMISC_1:31;
then reconsider F1 = <*x,x*> as FinSequence of the carrier of R by FINSEQ_1:def 4;
take F1 ; :: thesis:
A20: len <*x,x*> = 2 by FINSEQ_1:44;
hence 1 < len F1 ; :: thesis:
thus ( F1 . 1 = x & F1 . (len F1) = x ) by A20; :: thesis:
let n1 be Nat; :: thesis:
assume ( 2 <= n1 & n1 <= len F1 ) ; :: thesis:
then A21: n1 = 2 by A20, XXREAL_0:1;
thus ( [(F1 . n1),(F1 . (n1 - 1))] in the InternalRel of R or [(F1 . (n1 - 1)),(F1 . n1)] in the InternalRel of R ) by A18, A19, A21, RELAT_2:def 1; :: thesis:

end;

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

end;

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

now :: thesis:

let x, y, z be object ; :: thesis:
assume that
A23: x in the carrier of R and
A24: y in the carrier of R and
A25: z in the carrier of R and
A26: ( [x,y] in P1 & [y,z] in P1 ) ; :: thesis:
( S₁[x,y] & S₁[y,z] ) by A1, A26;
then consider p1, p2 being FinSequence of the carrier of R such that
A27: 1 < len p1 and
A28: p1 . 1 = x and
A29: p1 . (len p1) = y and
A30: 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
A31: 1 < len p2 and
A32: p2 . 1 = y and
A33: p2 . (len p2) = z and
A34: 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:
A35: len F = (len p1) + (len p2) by FINSEQ_1:22;
1 + 1 < (len p1) + (len p2) by A27, A31, XREAL_1:8;
hence 1 < len F by A35, XXREAL_0:2; :: thesis:
1 in dom p1 by A27, FINSEQ_3:25;
hence F . 1 = x by A28, FINSEQ_1:def 7; :: thesis:
len p2 in dom p2 by A31, FINSEQ_3:25;
hence F . (len F) = z by A33, A35, FINSEQ_1:def 7; :: thesis:
let n1 be Nat; :: thesis:
assume that
A36: 2 <= n1 and
A37: n1 <= len F ; :: thesis:
A38: 1 <= n1 by A36, XXREAL_0:2;
A39: 2 - 1 <= n1 - 1 by A36, XREAL_1:9;
then reconsider n11 = n1 - 1 as Element of NAT by INT_1:3, XXREAL_0:2;
A40: ( not (len p1) + 1 <= n1 or (len p1) + 1 = n1 or (len p1) + 1 < n1 ) by XXREAL_0:1;
A41: n1 - 1 <= (len F) - 0 by A37, XREAL_1:13;

per cases by A40, INT_1:7;

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

then n1 - 1 <= (len p1) - 0 by XREAL_1:13;
then n11 in dom p1 by A39, FINSEQ_3:25;
then A43: F . (n1 - 1) = p1 . (n1 - 1) by FINSEQ_1:def 7;
n1 in dom p1 by A38, A42, FINSEQ_3:25;
then F . n1 = p1 . n1 by 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 A30, A36, A42, A43; :: thesis:

end;

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

len p1 < (len p1) + 1 by XREAL_1:29;
then A45: len p1 < n1 by A44, XXREAL_0:2;
then reconsider k = n1 - (len p1) as Element of NAT by INT_1:3, XREAL_1:48;
((len p1) + 1) - 1 < n1 - 1 by A44, XREAL_1:9;
then F . n11 = p2 . (n11 - (len p1)) by A41, FINSEQ_1:24;
then A46: F . (n1 - 1) = p2 . (k - 1) ;
1 < n1 - (len p1) by A44, XREAL_1:20;
then A47: 1 + 1 <= n1 - (len p1) by INT_1:7;
n1 <= (len p1) + (len p2) by A37, FINSEQ_1:22;
then A48: k <= len p2 by XREAL_1:20;
F . n1 = p2 . k by A37, A45, FINSEQ_1:24;
hence ( [(F . n1),(F . (n1 - 1))] in the InternalRel of R or [(F . (n1 - 1)),(F . n1)] in the InternalRel of R ) by A34, A46, A47, A48; :: thesis:

end;

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

( (len p1) + 1 <= (len p1) + (len p2) & ((len p1) + 1) - (len p1) = 1 ) by A31, XREAL_1:8;
then A50: F . n1 = y by A32, A49, FINSEQ_1:23;
len p1 in dom p1 by A27, FINSEQ_3:25;
then F . (n1 - 1) = y by A29, A49, 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 A18, A24, A50, RELAT_2:def 1; :: thesis:

end;

hence [x,z] in P1 by A23, A25; :: 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 A22, A17, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
take P1 ; :: thesis:
thus for x, y being object 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 A1; :: thesis: