defpred S₁[ object , object ] means for i being Element of NAT st i = $1 holds
( ( 1 < i & i < n implies $2 = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies $2 = {i,n,(i + 1)} ) & ( 1 < i & i = n implies $2 = {i,(i -' 1),1} ) & ( i = 1 & i = n implies $2 = {i} ) );
A1: for x being object st x in Seg n holds
ex y being object st
( y in bool (Seg n) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Seg n implies ex y being object st
( y in bool (Seg n) & S₁[x,y] ) )
assume A2: x in Seg n ; :: thesis: ex y being object st
( y in bool (Seg n) & S₁[x,y] )
then reconsider i2 = x as Element of NAT ;
A3: ( 1 <= i2 & i2 <= n ) by A2, FINSEQ_1:1;

now :: thesis: ( ( 1 < i2 & i2 < n & ex y being object st
( y in bool (Seg n) & S₁[x,y] ) ) or ( i2 = 1 & i2 < n & ex y being object st
( y in bool (Seg n) & S₁[x,y] ) ) or ( 1 < i2 & i2 = n & ex y being object st
( y in bool (Seg n) & S₁[x,y] ) ) or ( i2 = 1 & i2 = n & ex y being object st
( y in bool (Seg n) & S₁[x,y] ) ) )

per cases ( ( 1 < i2 & i2 < n ) or ( i2 = 1 & i2 < n ) or ( 1 < i2 & i2 = n ) or ( i2 = 1 & i2 = n ) ) by A3, XXREAL_0:1;

case A4: ( 1 < i2 & i2 < n ) ; :: thesis: ex y being object st
( y in bool (Seg n) & S₁[x,y] )

i2 <= i2 + 1 by NAT_1:12;
then A5: 1 < i2 + 1 by A4, XXREAL_0:2;
i2 + 1 <= n by A4, NAT_1:13;
then A6: i2 + 1 in Seg n by A5;
set y0 = {i2,(i2 -' 1),(i2 + 1)};
i2 - 1 > 0 by A4, XREAL_1:50;
then i2 -' 1 > 0 by XREAL_0:def 2;
then A7: i2 -' 1 >= 0 + 1 by NAT_1:13;
i2 -' 1 <= i2 by NAT_D:35;
then i2 -' 1 < n by A4, XXREAL_0:2;
then A8: i2 -' 1 in Seg n by A7;
A9: {i2,(i2 -' 1),(i2 + 1)} c= Seg n by A2, A8, A6, ENUMSET1:def 1;
S₁[x,{i2,(i2 -' 1),(i2 + 1)}] by A4;
hence ex y being object st
( y in bool (Seg n) & S₁[x,y] ) by A9; :: thesis: verum

end;

case A10: ( i2 = 1 & i2 < n ) ; :: thesis: ex y being object st
( y in bool (Seg n) & S₁[x,y] )

then i2 + 1 <= n by NAT_1:13;
then A11: i2 + 1 in Seg n by A10;
set y0 = {i2,n,(i2 + 1)};
A12: n in Seg n by A10;
A13: {i2,n,(i2 + 1)} c= Seg n by A2, A12, A11, ENUMSET1:def 1;
S₁[x,{i2,n,(i2 + 1)}] by A10;
hence ex y being object st
( y in bool (Seg n) & S₁[x,y] ) by A13; :: thesis: verum

end;

case A14: ( 1 < i2 & i2 = n ) ; :: thesis: ex y being object st
( y in bool (Seg n) & S₁[x,y] )

then i2 - 1 > 0 by XREAL_1:50;
then i2 -' 1 > 0 by XREAL_0:def 2;
then A15: i2 -' 1 >= 0 + 1 by NAT_1:13;
set y0 = {i2,(i2 -' 1),1};
A16: 1 in Seg n by A14;
i2 -' 1 <= n by A14, NAT_D:35;
then A17: i2 -' 1 in Seg n by A15;
A18: {i2,(i2 -' 1),1} c= Seg n by A2, A17, A16, ENUMSET1:def 1;
S₁[x,{i2,(i2 -' 1),1}] by A14;
hence ex y being object st
( y in bool (Seg n) & S₁[x,y] ) by A18; :: thesis: verum

end;

case A19: ( i2 = 1 & i2 = n ) ; :: thesis: ex y being object st
( y in bool (Seg n) & S₁[x,y] )

set y0 = {i2};
A20: {i2} c= Seg n by A2, TARSKI:def 1;
S₁[x,{i2}] by A19;
hence ex y being object st
( y in bool (Seg n) & S₁[x,y] ) by A20; :: thesis: verum

end;

end;

end;

hence ex y being object st
( y in bool (Seg n) & S₁[x,y] ) ; :: thesis: verum

end;

consider f2 being Function of (Seg n),(bool (Seg n)) such that
A21: for x3 being object st x3 in Seg n holds
S₁[x3,f2 . x3] from FUNCT_2:sch 1(A1);
consider R being Relation of (Seg n) such that
A22: for i being set st i in Seg n holds
Im (R,i) = f2 . i by FUNCT_2:93;
take R ; :: thesis: for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) )
let i be Element of NAT ; :: thesis: ( i in Seg n implies ( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) ) )
assume A23: i in Seg n ; :: thesis: ( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) )
then Im (R,i) = f2 . i by A22;
hence ( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) ) by A21, A23; :: thesis: verum