let n be Element of NAT ; :: thesis: ( n > 0 implies FTSC1 n is symmetric )
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 15 :: 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 ;
y in Seg n by A1;
then reconsider j = y as Element of NAT ;
A2: ( 1 <= j & j <= n ) by A1, FINSEQ_1:3;
set f = Nbdc1 n;
A3: ( 1 <= i & i <= n ) by A1, FINSEQ_1:3;
A4: ( ( 1 < i & i < n implies Im (Nbdc1 n),i = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (Nbdc1 n),i = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (Nbdc1 n),i = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (Nbdc1 n),i = {i} ) ) by A1, Def5;
assume A5: y in U_FT x ; :: thesis: x in U_FT y

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

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

then A7: ( y = i or y = i -' 1 or y = i + 1 ) by A1, A4, A5, ENUMSET1:def 1;

A8: now

assume A9: y = i -' 1 ; :: thesis: x in U_FT y
i - 1 > 0 by A6, XREAL_1:52;
then A10: i -' 1 = i - 1 by XREAL_0:def 2;

per cases ( x = j or x = j -' 1 or x = j + 1 ) by A9, A10;

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

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

end;

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

then A13: i = (i -' 1) -' 1 by A9;

now

assume i <> 0 ; :: thesis: contradiction
then i > 0 ;
then A14: i >= 0 + 1 by NAT_1:13;
then i - 1 >= 1 - 1 by XREAL_1:11;
then A15: i - 1 = i -' 1 by XREAL_0:def 2;

now

assume A16: i = 1 ; :: thesis: contradiction
then (i -' 1) - 1 < 0 by A15;
hence contradiction by A9, A12, A16, XREAL_0:def 2; :: thesis: verum

end;

then i > 1 by A14, XXREAL_0:1;
then i - 1 > 1 - 1 by XREAL_1:11;
then i -' 1 >= 0 + 1 by A15, NAT_1:13;
then (i -' 1) - 1 >= 0 by XREAL_1:50;
then (i -' 1) -' 1 = (i -' 1) - 1 by XREAL_0:def 2;
hence contradiction by A13, A15; :: thesis: verum

end;

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

end;

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

then A18: j < n by A3, NAT_1:13;

A19: now

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

end;

now

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

end;

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

end;

end;

end;

now

assume A20: y = i + 1 ; :: thesis: x in U_FT y
then A21: j - 1 = x ;

now

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

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

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

end;

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

now

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

end;

then A24: j > 1 by A2, XXREAL_0:1;

A25: now

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

end;

now

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

end;

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

end;

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

hence contradiction by A20; :: thesis: verum

end;

end;

end;

hence x in U_FT y ; :: thesis: verum

end;

hence x in U_FT y by A5, A7, A8; :: thesis: verum

end;

suppose A26: ( 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, A4, A5, A26, ENUMSET1:def 1;

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

hence x in U_FT y by A1, A4, A26, 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, A26, Def5;
hence x in U_FT y by A26, ENUMSET1:def 1; :: thesis: verum

end;

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

then A28: j < n by A2, XXREAL_0:1;
j - 1 = i by A27;
then A29: j -' 1 = i by XREAL_0:def 2;
Im the InternalRel of (FTSC1 n),y = {j,(j -' 1),(j + 1)} by A1, A26, A27, A28, Def5;
hence x in U_FT y by A29, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

suppose A30: ( 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, A4, A5, A30, ENUMSET1:def 1;

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

hence x in U_FT y by A1, A4, A30, 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, A30, Def5;
hence x in U_FT y by A30, ENUMSET1:def 1; :: thesis: verum

end;

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

then A32: 1 < j by A2, XXREAL_0:1;
n - 1 > 0 by A30, XREAL_1:52;
then A33: n - 1 = n -' 1 by XREAL_0:def 2;
(n - 1) + 1 = n ;
then j < n by A30, A31, A33, NAT_1:13;
then Im the InternalRel of (FTSC1 n),y = {j,(j -' 1),(j + 1)} by A1, A32, Def5;
hence x in U_FT y by A30, A31, A33, 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, A5, TARSKI:def 1;
hence x in U_FT y by A5; :: thesis: verum

end;

end;