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 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 <= n by A1, FINSEQ_1:1;
y in Seg n by A1;
then reconsider j = y as Element of NAT ;
A4: U_FT y = {j,(max ((j -' 1),1)),(min ((j + 1),n))} by A1, Def3;
A5: U_FT x = {i,(max ((i -' 1),1)),(min ((i + 1),n))} by A1, Def3;

now :: thesis: ( y in U_FT x implies x in U_FT y )

A6: now :: thesis: ( y = max ((i -' 1),1) implies x in U_FT y )

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

now :: thesis: ( ( i -' 1 >= 1 & ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ) or ( i -' 1 < 1 & ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ) )

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

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

then A9: y = i -' 1 by A7, XXREAL_0:def 10;

now :: thesis: ( ( i - 1 >= 0 & ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ) or ( i - 1 < 0 & contradiction ) )

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 A9, XREAL_0:def 2;
hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) by A3, XXREAL_0:def 9; :: thesis: verum

end;

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

hence contradiction by A8, 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 A10: i -' 1 < 1 ; :: thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )

A11: now :: thesis: not i > 1

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

end;

y = 1 by A7, A10, XXREAL_0:def 10;
hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) by A2, A11, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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

end;

assume A13: y in U_FT x ; :: thesis: x in U_FT y

A14: now :: thesis: ( y = min ((i + 1),n) implies x in U_FT y )

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

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

per cases ( y = i or y = max ((i -' 1),1) or y = min ((i + 1),n) ) by A5, A13, 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 A15: y = max ((i -' 1),1) ; :: thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )

now :: thesis: ( ( i -' 1 >= 1 & ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ) or ( i -' 1 < 1 & ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ) )

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

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

then A17: y = i -' 1 by A15, XXREAL_0:def 10;

now :: thesis: ( ( i - 1 >= 0 & ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ) or ( i - 1 < 0 & contradiction ) )

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 A17, XREAL_0:def 2;
hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) by A3, XXREAL_0:def 9; :: thesis: verum

end;

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

hence contradiction by A16, 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 A18: i -' 1 < 1 ; :: thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )

A19: now :: thesis: not i > 1

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

end;

y = 1 by A15, A18, XXREAL_0:def 10;
hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) by A2, A19, 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 A21: y = min ((i + 1),n) ; :: thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )

now :: thesis: ( ( i + 1 <= n & ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ) or ( i + 1 > n & ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ) )

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 A22: y = i + 1 by A21, XXREAL_0:def 9;
then A23: j - 1 = j -' 1 by XREAL_0:def 2;

now :: thesis: ( ( j - 1 >= 1 & ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ) or ( j - 1 < 1 & contradiction ) )

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 A22, A23, XXREAL_0:def 10; :: thesis: verum

end;

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

hence contradiction by A1, A22, FINSEQ_1: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 A24: i + 1 > n ; :: thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )

then y = n by A21, XXREAL_0:def 9;
then j + 1 > n by NAT_1:13;
then A25: min ((j + 1),n) = n by XXREAL_0:def 9;
i >= n by A24, NAT_1:13;
hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) by A3, A25, 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;

( y = i or y = max ((i -' 1),1) or y = min ((i + 1),n) ) by A5, A13, ENUMSET1:def 1;
hence x in U_FT y by A13, A6, A14; :: thesis: verum

end;

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