let n be Nat; :: thesis:
assume n > 0 ; :: thesis:
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:
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:

A6: now :: thesis:

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

now :: thesis:

per cases ;

case A8: i -' 1 >= 1 ; :: thesis:

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

now :: thesis:

per cases ;

case i - 1 >= 0 ; :: thesis:

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:

end;

case i - 1 < 0 ; :: thesis:

hence contradiction by A8, XREAL_0:def 2; :: thesis:

end;

end;

end;

hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; :: thesis:

end;

case A10: i -' 1 < 1 ; :: thesis:

A11: now :: thesis:

assume i > 1 ; :: thesis:
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:

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:

end;

end;

end;

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

end;

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

A14: now :: thesis:

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

now :: thesis:

per cases by A5, A13, ENUMSET1:def 1;

case y = i ; :: thesis:

hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; :: thesis:

end;

case A15: y = max ((i -' 1),1) ; :: thesis:

now :: thesis:

per cases ;

case A16: i -' 1 >= 1 ; :: thesis:

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

now :: thesis:

per cases ;

case i - 1 >= 0 ; :: thesis:

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:

end;

case i - 1 < 0 ; :: thesis:

hence contradiction by A16, XREAL_0:def 2; :: thesis:

end;

end;

end;

hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; :: thesis:

end;

case A18: i -' 1 < 1 ; :: thesis:

A19: now :: thesis:

assume i > 1 ; :: thesis:
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:

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:

end;

end;

end;

hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; :: thesis:

end;

case A21: y = min ((i + 1),n) ; :: thesis:

now :: thesis:

per cases ;

case i + 1 <= n ; :: thesis:

then A22: y = i + 1 by A21, XXREAL_0:def 9;
then A23: j - 1 = j -' 1 by XREAL_0:def 2;

now :: thesis:

per cases ;

case j - 1 >= 1 ; :: thesis:

hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) by A22, A23, XXREAL_0:def 10; :: thesis:

end;

case j - 1 < 1 ; :: thesis:

hence contradiction by A1, A22, FINSEQ_1:1; :: thesis:

end;

end;

end;

hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; :: thesis:

end;

case A24: i + 1 > n ; :: thesis:

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:

end;

end;

end;

hence ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; :: thesis:

end;

end;

end;

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

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:

end;

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