let n be Nat; ( n > 0 implies FTSL1 n is symmetric )
assume
n > 0
; FTSL1 n is symmetric
then A1:
FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #)
by Def4;
let x, y be Element of (FTSL1 n); FIN_TOPO:def 13 ( 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;
hence
( not y in U_FT x or x in U_FT y )
; verum