let n be Nat; :: thesis: ( n > 0 implies FTSL1 n is filled )
assume n > 0 ; :: thesis: FTSL1 n is filled
then A1: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by Def4;
let x be Element of (FTSL1 n); :: according to FIN_TOPO:def 4 :: thesis: x in U_FT x
x in Seg n by A1;
then reconsider i = x as Element of NAT ;
U_FT x = {i,(max ((i -' 1),1)),(min ((i + 1),n))} by A1, Def3;
hence x in U_FT x by ENUMSET1:def 1; :: thesis: verum