let n be Element of NAT ; :: thesis:
set f = Nbdc1 n;
assume n > 0 ; :: thesis:
then A1: FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #) by Def6;
let x, y be Element of (FTSC1 n); :: according to FIN_TOPO:def 13 :: thesis:
x in Seg n by A1;
then reconsider i = x as Element of NAT ;
A2: 1 <= i by A1, FINSEQ_1:1;
A3: ( i = 1 & i < n implies Im ((Nbdc1 n),i) = {i,n,(i + 1)} ) by A1, Def5;
A4: ( i = 1 & i = n implies Im ((Nbdc1 n),i) = {i} ) by A1, Def5;
A5: i <= n by A1, FINSEQ_1:1;
y in Seg n by A1;
then reconsider j = y as Element of NAT ;
A6: 1 <= j by A1, FINSEQ_1:1;
A7: ( 1 < i & i = n implies Im ((Nbdc1 n),i) = {i,(i -' 1),1} ) by A1, Def5;
A8: ( 1 < i & i < n implies Im ((Nbdc1 n),i) = {i,(i -' 1),(i + 1)} ) by A1, Def5;
assume A9: y in U_FT x ; :: thesis:
A10: j <= n by A1, FINSEQ_1:1;

per cases by A2, A5, XXREAL_0:1;

suppose A11: ( 1 < i & i < n ) ; :: thesis:

A12: now :: thesis:

i - 1 > 0 by A11, XREAL_1:50;
then A13: i -' 1 = i - 1 by XREAL_0:def 2;
assume A14: y = i -' 1 ; :: thesis:

per cases by A14, A13;

suppose A15: x = j ; :: thesis:

then Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A11, Def5;
hence x in U_FT y by A15, ENUMSET1:def 1; :: thesis:

end;

suppose A16: x = j -' 1 ; :: thesis:

then A17: i = (i -' 1) -' 1 by A14;

now :: thesis:

assume i <> 0 ; :: thesis:
then A18: i >= 0 + 1 by NAT_1:13;
then i - 1 >= 1 - 1 by XREAL_1:9;
then A19: i - 1 = i -' 1 by XREAL_0:def 2;

now :: thesis:

assume A20: i = 1 ; :: thesis:
then (i -' 1) - 1 < 0 by A19;
hence contradiction by A14, A16, A20, XREAL_0:def 2; :: thesis:

end;

then i > 1 by A18, XXREAL_0:1;
then i - 1 > 1 - 1 by XREAL_1:9;
then i -' 1 >= 0 + 1 by A19, NAT_1:13;
then (i -' 1) - 1 >= 0 by XREAL_1:48;
then (i -' 1) -' 1 = (i -' 1) - 1 by XREAL_0:def 2;
hence contradiction by A17, A19; :: thesis:

end;

hence x in U_FT y by A11; :: thesis:

end;

suppose A21: x = j + 1 ; :: thesis:

then A22: j < n by A5, NAT_1:13;

A23: now :: thesis:

assume j <> 1 ; :: thesis:
then j > 1 by A6, XXREAL_0:1;
then Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A22, Def5;
hence x in U_FT y by A21, ENUMSET1:def 1; :: thesis:

end;

now :: thesis:

assume j = 1 ; :: thesis:
then Im ( the InternalRel of (FTSC1 n),y) = {j,n,(j + 1)} by A1, A22, Def5;
hence x in U_FT y by A21, ENUMSET1:def 1; :: thesis:

end;

hence x in U_FT y by A23; :: thesis:

end;

end;

end;

A24: now :: thesis:

assume A25: y = i + 1 ; :: thesis:
then A26: j - 1 = x ;

now :: thesis:

per cases by A11, A26, XREAL_0:def 2;

case A27: x = j ; :: thesis:

then Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A11, Def5;
hence x in U_FT y by A27, ENUMSET1:def 1; :: thesis:

end;

case A28: x = j -' 1 ; :: thesis:

now :: thesis:

assume j = 1 ; :: thesis:
then j - 1 = 0 ;
hence contradiction by A11, A28, XREAL_0:def 2; :: thesis:

end;

then A29: j > 1 by A6, XXREAL_0:1;

A30: now :: thesis:

assume j <> n ; :: thesis:
then j < n by A10, XXREAL_0:1;
then Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A29, Def5;
hence x in U_FT y by A28, ENUMSET1:def 1; :: thesis:

end;

now :: thesis:

assume j = n ; :: thesis:
then Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),1} by A1, A29, Def5;
hence x in U_FT y by A28, ENUMSET1:def 1; :: thesis:

end;

hence x in U_FT y by A30; :: thesis:

end;

case x = j + 1 ; :: thesis:

hence contradiction by A25; :: thesis:

end;

end;

end;

hence x in U_FT y ; :: thesis:

end;

( y = i or y = i -' 1 or y = i + 1 ) by A1, A8, A9, A11, ENUMSET1:def 1;
hence x in U_FT y by A9, A12, A24; :: thesis:

end;

suppose A31: ( i = 1 & i < n ) ; :: thesis:

per cases by A1, A3, A9, A31, ENUMSET1:def 1;

suppose ( y = i & y <> n ) ; :: thesis:

hence x in U_FT y by A1, A3, A31, ENUMSET1:def 1; :: thesis:

end;

suppose y = n ; :: thesis:

then Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),1} by A1, A31, Def5;
hence x in U_FT y by A31, ENUMSET1:def 1; :: thesis:

end;

suppose A32: ( y = i + 1 & y <> n ) ; :: thesis:

then j - 1 = i ;
then A33: j -' 1 = i by XREAL_0:def 2;
j < n by A10, A32, XXREAL_0:1;
then Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A31, A32, Def5;
hence x in U_FT y by A33, ENUMSET1:def 1; :: thesis:

end;

end;

end;

suppose A34: ( 1 < i & i = n ) ; :: thesis:

per cases by A1, A7, A9, A34, ENUMSET1:def 1;

suppose ( y = i & y <> 1 ) ; :: thesis:

hence x in U_FT y by A1, A7, A34, ENUMSET1:def 1; :: thesis:

end;

suppose y = 1 ; :: thesis:

then Im ( the InternalRel of (FTSC1 n),y) = {j,n,(j + 1)} by A1, A34, Def5;
hence x in U_FT y by A34, ENUMSET1:def 1; :: thesis:

end;

suppose A35: ( y = i -' 1 & y <> 1 ) ; :: thesis:

then A36: 1 < j by A6, XXREAL_0:1;
n - 1 > 0 by A34, XREAL_1:50;
then A37: n - 1 = n -' 1 by XREAL_0:def 2;
(n - 1) + 1 = n ;
then j < n by A34, A35, A37, NAT_1:13;
then Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A36, Def5;
hence x in U_FT y by A34, A35, A37, ENUMSET1:def 1; :: thesis:

end;

end;

end;

suppose ( i = 1 & i = n ) ; :: thesis:

then j = i by A1, A4, A9, TARSKI:def 1;
hence x in U_FT y by A9; :: thesis:

end;

end;