let n be Nat; :: thesis: ( n > 0 implies FTSL1 n is symmetric )
assume n > 0 ; :: thesis: FTSL1 n is symmetric
then A1: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by Def4;
let x, y be Element of (FTSL1 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 ;
A2: ( 1 <= i & i <= n ) by A1, FINSEQ_1:3;
y in Seg n by A1;
then reconsider j = y as Element of NAT ;
A3: U_FT x = {i,(max (i -' 1),1),(min (i + 1),n)} by A1, Def3;
A4: U_FT y = {j,(max (j -' 1),1),(min (j + 1),n)} by A1, Def3;

now

assume A5: y in U_FT x ; :: thesis: x in U_FT y
then A6: ( y = i or y = max (i -' 1),1 or y = min (i + 1),n ) by A3, ENUMSET1:def 1;

A7: now

assume A8: y = max (i -' 1),1 ; :: thesis: x in U_FT y

now

per cases ( i -' 1 >= 1 or i -' 1 < 1 ) ;

case A9: i -' 1 >= 1 ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

then A10: y = i -' 1 by A8, XXREAL_0:def 10;

now

per cases ( i - 1 >= 0 or i - 1 < 0 ) ;

case i - 1 >= 0 ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

then j = i - 1 by A10, XREAL_0:def 2;
hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) by A2, XXREAL_0:def 9; :: thesis: verum

end;

case i - 1 < 0 ; :: thesis: contradiction

hence contradiction by A9, XREAL_0:def 2; :: thesis: verum

end;

end;

end;

hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) ; :: thesis: verum

end;

case A11: i -' 1 < 1 ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

then A12: y = 1 by A8, XXREAL_0:def 10;

now

assume i > 1 ; :: thesis: contradiction
then A13: i - 1 > 0 by XREAL_1:52;
then i -' 1 = i - 1 by XREAL_0:def 2;
then i -' 1 >= 0 + 1 by A13, NAT_1:13;
hence contradiction by A11; :: thesis: verum

end;

hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) by A2, A12, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence x in U_FT y by A4, ENUMSET1:def 1; :: thesis: verum

end;

now

assume y = min (i + 1),n ; :: thesis: x in U_FT y

now

per cases ( y = i or y = max (i -' 1),1 or y = min (i + 1),n ) by A3, A5, ENUMSET1:def 1;

case y = i ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) ; :: thesis: verum

end;

case A14: y = max (i -' 1),1 ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

now

per cases ( i -' 1 >= 1 or i -' 1 < 1 ) ;

case A15: i -' 1 >= 1 ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

then A16: y = i -' 1 by A14, XXREAL_0:def 10;

now

per cases ( i - 1 >= 0 or i - 1 < 0 ) ;

case i - 1 >= 0 ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

then j = i - 1 by A16, XREAL_0:def 2;
hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) by A2, XXREAL_0:def 9; :: thesis: verum

end;

case i - 1 < 0 ; :: thesis: contradiction

hence contradiction by A15, XREAL_0:def 2; :: thesis: verum

end;

end;

end;

hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) ; :: thesis: verum

end;

case A17: i -' 1 < 1 ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

then A18: y = 1 by A14, XXREAL_0:def 10;

now

assume i > 1 ; :: thesis: contradiction
then A19: i - 1 > 0 by XREAL_1:52;
then i -' 1 = i - 1 by XREAL_0:def 2;
then i -' 1 >= 0 + 1 by A19, NAT_1:13;
hence contradiction by A17; :: thesis: verum

end;

hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) by A2, A18, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) ; :: thesis: verum

end;

case A20: y = min (i + 1),n ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

now

per cases ( i + 1 <= n or i + 1 > n ) ;

case i + 1 <= n ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

then A21: y = i + 1 by A20, XXREAL_0:def 9;
then A22: j - 1 = j -' 1 by XREAL_0:def 2;

now

per cases ( j - 1 >= 1 or j - 1 < 1 ) ;

case j - 1 >= 1 ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) by A21, A22, XXREAL_0:def 10; :: thesis: verum

end;

case j - 1 < 1 ; :: thesis: contradiction

hence contradiction by A1, A21, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) ; :: thesis: verum

end;

case A23: i + 1 > n ; :: thesis: ( x = j or x = max (j -' 1),1 or x = min (j + 1),n )

then y = n by A20, XXREAL_0:def 9;
then j + 1 > n by NAT_1:13;
then A24: min (j + 1),n = n by XXREAL_0:def 9;
i >= n by A23, NAT_1:13;
hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) by A2, A24, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence ( x = j or x = max (j -' 1),1 or x = min (j + 1),n ) ; :: thesis: verum

end;

end;

end;

hence x in U_FT y by A4, ENUMSET1:def 1; :: thesis: verum

end;

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

end;

hence ( not y in U_FT x or x in U_FT y ) ; :: thesis: verum