let n be Element of NAT ; :: thesis: ( n > 0 implies FTSC1 n is symmetric )
set f = Nbdc1 n;
assume n > 0 ; :: thesis: FTSC1 n is symmetric
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: ( not y in U_FT x or x in U_FT y )
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: x in U_FT y
A10: j <= n by A1, FINSEQ_1:1;

per cases ( ( 1 < i & i < n ) or ( i = 1 & i < n ) or ( 1 < i & i = n ) or ( i = 1 & i = n ) ) by A2, A5, XXREAL_0:1;

suppose A11: ( 1 < i & i < n ) ; :: thesis: x in U_FT y

A12: now :: thesis: ( y = i -' 1 implies x in U_FT y )

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: x in U_FT y

per cases ( x = j or x = j -' 1 or x = j + 1 ) by A14, A13;

suppose A15: x = j ; :: thesis: x in U_FT y

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: verum

end;

suppose A16: x = j -' 1 ; :: thesis: x in U_FT y

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

now :: thesis: not i <> 0

assume i <> 0 ; :: thesis: contradiction
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: not i = 1

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

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: verum

end;

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

end;

suppose A21: x = j + 1 ; :: thesis: x in U_FT y

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

A23: now :: thesis: ( j <> 1 implies x in U_FT y )

assume j <> 1 ; :: thesis: x in U_FT y
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: verum

end;

now :: thesis: ( j = 1 implies x in U_FT y )

assume j = 1 ; :: thesis: x in U_FT y
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: verum

end;

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

end;

end;

end;

A24: now :: thesis: ( y = i + 1 implies x in U_FT y )

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

now :: thesis: ( ( x = j & x in U_FT y ) or ( x = j -' 1 & x in U_FT y ) or ( x = j + 1 & contradiction ) )

per cases ( x = j or x = j -' 1 or x = j + 1 ) by A11, A26, XREAL_0:def 2;

case A27: x = j ; :: thesis: x in U_FT y

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: verum

end;

case A28: x = j -' 1 ; :: thesis: x in U_FT y

now :: thesis: not j = 1

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

end;

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

A30: now :: thesis: ( j <> n implies x in U_FT y )

assume j <> n ; :: thesis: x in U_FT y
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: verum

end;

now :: thesis: ( j = n implies x in U_FT y )

assume j = n ; :: thesis: x in U_FT y
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: verum

end;

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

end;

case x = j + 1 ; :: thesis: contradiction

hence contradiction by A25; :: thesis: verum

end;

end;

end;

hence x in U_FT y ; :: thesis: verum

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: verum

end;

suppose A31: ( i = 1 & i < n ) ; :: thesis: x in U_FT y

per cases ( ( y = i & y <> n ) or y = n or ( y = i + 1 & y <> n ) ) by A1, A3, A9, A31, ENUMSET1:def 1;

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

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

end;

suppose y = n ; :: thesis: x in U_FT y

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: verum

end;

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

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: verum

end;

end;

end;

suppose A34: ( 1 < i & i = n ) ; :: thesis: x in U_FT y

per cases ( ( y = i & y <> 1 ) or y = 1 or ( y = i -' 1 & y <> 1 ) ) by A1, A7, A9, A34, ENUMSET1:def 1;

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

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

end;

suppose y = 1 ; :: thesis: x in U_FT y

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: verum

end;

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

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: verum

end;

end;

end;

suppose ( i = 1 & i = n ) ; :: thesis: x in U_FT y

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

end;

end;