let n be Element of NAT ; :: thesis: ( n > 0 implies FTSC1 n is reflexive )
assume n > 0 ; :: thesis: FTSC1 n is reflexive
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 ;
set f = Nbdc1 n;
A2: ( 1 <= i & i <= n ) by A1, FINSEQ_1:3;
A3: ( ( 1 < i & i < n implies Im (Nbdc1 n),i = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (Nbdc1 n),i = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (Nbdc1 n),i = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (Nbdc1 n),i = {i} ) ) 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, A3, 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, A3, 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, TARSKI:def 1; :: thesis: verum

end;

end;