let n be Element of NAT ; :: thesis: ( n > 0 implies FTSC1 n is filled )
set f = Nbdc1 n;
assume n > 0 ; :: thesis: FTSC1 n is filled
then A1: FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #) by Def6;
let x be Element of (FTSC1 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 ;
A2: ( 1 <= i & i <= n ) by A1, FINSEQ_1:1;
A3: ( i = 1 & i < n implies Im ((Nbdc1 n),i) = {i,n,(i + 1)} ) by A1, Def5;
A4: ( 1 < i & i < n implies Im ((Nbdc1 n),i) = {i,(i -' 1),(i + 1)} ) by A1, Def5;
A5: ( i = 1 & i = n implies Im ((Nbdc1 n),i) = {i} ) by A1, Def5;
A6: ( 1 < i & i = n implies Im ((Nbdc1 n),i) = {i,(i -' 1),1} ) by A1, Def5;

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

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

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

end;

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

hence x in U_FT x by A1, A3, ENUMSET1:def 1; :: thesis: verum

end;

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

hence x in U_FT x by A1, A6, ENUMSET1:def 1; :: thesis: verum

end;

suppose ( i = 1 & i = n ) ; :: thesis: x in U_FT x

hence x in U_FT x by A1, A5, TARSKI:def 1; :: thesis: verum

end;

end;