:: FINTOPO4 semantic presentation

begin

definition
let FT be non empty RelStr ;
let A, B be Subset of FT;
predA,B are_separated  means :Def1: :: FINTOPO4:def 1
( A ^b misses B & A misses B ^b );
symmetry
 for A, B being Subset of FT st A ^b misses B & A misses B ^b holds
( B ^b misses A & B misses A ^b ) ;
end;

:: deftheorem Def1 defines are_separated FINTOPO4:def_1_:_
 for FT being non empty RelStr
for A, B being Subset of FT holds
( A,B are_separated iff ( A ^b misses B & A misses B ^b ) );

theorem Th1: :: FINTOPO4:1
for FT being non empty filled RelStr
for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Finf (A,n) c= Finf (A,m)
proof
let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Finf (A,n) c= Finf (A,m)
let A be Subset of FT; ::_thesis: for n, m being Element of NAT st n <= m holds
Finf (A,n) c= Finf (A,m)
let n, m be Element of NAT ; ::_thesis: ( n <= m implies Finf (A,n) c= Finf (A,m) )
defpred S1[ Element of NAT ] means  Finf (A,n) c= Finf (A,(n + $1));
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A2: Finf (A,(n + k)) c= Finf (A,((n + k) + 1)) by FINTOPO3:37;
assume  S1[k] ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A2, XBOOLE_1:1; ::_thesis: verum
end;
assume  n <= m ; ::_thesis: Finf (A,n) c= Finf (A,m)
then  m - n >= 0 by XREAL_1:48;
then A3: n + (m -' n) = n + (m - n) by XREAL_0:def_2
.= m ;
A4: S1[ 0 ] ;
 for m2 being Element of NAT holds S1[m2] from NAT_1:sch_1(A4, A1);
hence  Finf (A,n) c= Finf (A,m) by A3; ::_thesis: verum
end;

theorem :: FINTOPO4:2
for FT being non empty filled RelStr
for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Fcl (A,n) c= Fcl (A,m)
proof
let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Fcl (A,n) c= Fcl (A,m)
let A be Subset of FT; ::_thesis: for n, m being Element of NAT st n <= m holds
Fcl (A,n) c= Fcl (A,m)
let n, m be Element of NAT ; ::_thesis: ( n <= m implies Fcl (A,n) c= Fcl (A,m) )
defpred S1[ Element of NAT ] means  Fcl (A,n) c= Fcl (A,(n + $1));
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A2: Fcl (A,(n + k)) c= Fcl (A,((n + k) + 1)) by FINTOPO3:25;
assume  S1[k] ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A2, XBOOLE_1:1; ::_thesis: verum
end;
assume  n <= m ; ::_thesis: Fcl (A,n) c= Fcl (A,m)
then  m - n >= 0 by XREAL_1:48;
then A3: n + (m -' n) = n + (m - n) by XREAL_0:def_2
.= m ;
A4: S1[ 0 ] ;
 for m2 being Element of NAT holds S1[m2] from NAT_1:sch_1(A4, A1);
hence  Fcl (A,n) c= Fcl (A,m) by A3; ::_thesis: verum
end;

theorem :: FINTOPO4:3
for FT being non empty filled RelStr
for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Fdfl (A,m) c= Fdfl (A,n)
proof
let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Fdfl (A,m) c= Fdfl (A,n)
let A be Subset of FT; ::_thesis: for n, m being Element of NAT st n <= m holds
Fdfl (A,m) c= Fdfl (A,n)
let n, m be Element of NAT ; ::_thesis: ( n <= m implies Fdfl (A,m) c= Fdfl (A,n) )
defpred S1[ Element of NAT ] means  Fdfl (A,(n + $1)) c= Fdfl (A,n);
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A2: Fdfl (A,((n + k) + 1)) c= Fdfl (A,(n + k)) by FINTOPO3:44;
assume  S1[k] ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A2, XBOOLE_1:1; ::_thesis: verum
end;
assume  n <= m ; ::_thesis: Fdfl (A,m) c= Fdfl (A,n)
then  m - n >= 0 by XREAL_1:48;
then A3: n + (m -' n) = n + (m - n) by XREAL_0:def_2
.= m ;
A4: S1[ 0 ] ;
 for m2 being Element of NAT holds S1[m2] from NAT_1:sch_1(A4, A1);
hence  Fdfl (A,m) c= Fdfl (A,n) by A3; ::_thesis: verum
end;

theorem :: FINTOPO4:4
for FT being non empty filled RelStr
for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Fint (A,m) c= Fint (A,n)
proof
let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Fint (A,m) c= Fint (A,n)
let A be Subset of FT; ::_thesis: for n, m being Element of NAT st n <= m holds
Fint (A,m) c= Fint (A,n)
let n, m be Element of NAT ; ::_thesis: ( n <= m implies Fint (A,m) c= Fint (A,n) )
defpred S1[ Element of NAT ] means  Fint (A,(n + $1)) c= Fint (A,n);
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A2: Fint (A,((n + k) + 1)) c= Fint (A,(n + k)) by FINTOPO3:26;
assume  S1[k] ; ::_thesis: S1[k + 1]
hence  S1[k + 1] by A2, XBOOLE_1:1; ::_thesis: verum
end;
assume  n <= m ; ::_thesis: Fint (A,m) c= Fint (A,n)
then  m - n >= 0 by XREAL_1:48;
then A3: n + (m -' n) = n + (m - n) by XREAL_0:def_2
.= m ;
A4: S1[ 0 ] ;
 for m2 being Element of NAT holds S1[m2] from NAT_1:sch_1(A4, A1);
hence  Fint (A,m) c= Fint (A,n) by A3; ::_thesis: verum
end;

theorem :: FINTOPO4:5
for FT being non empty RelStr
for A, B being Subset of FT st A,B are_separated holds
B,A are_separated ;

theorem Th6: :: FINTOPO4:6
for FT being non empty filled RelStr
for A, B being Subset of FT st A,B are_separated holds
A misses B
proof
let FT be non empty filled RelStr ; ::_thesis: for A, B being Subset of FT st A,B are_separated holds
A misses B
let A, B be Subset of FT; ::_thesis: ( A,B are_separated implies A misses B )
assume  A,B are_separated ; ::_thesis: A misses B
then  A ^b misses B by Def1;
hence  A misses B by FIN_TOPO:13, XBOOLE_1:63; ::_thesis: verum
end;

theorem :: FINTOPO4:7
for FT being non empty RelStr
for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff ( A ^f misses B & A misses B ^f ) )
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff ( A ^f misses B & A misses B ^f ) )
let A, B be Subset of FT; ::_thesis: ( FT is symmetric implies ( A,B are_separated iff ( A ^f misses B & A misses B ^f ) ) )
assume  FT is symmetric ; ::_thesis: ( A,B are_separated iff ( A ^f misses B & A misses B ^f ) )
then  ( A ^b = A ^f & B ^b = B ^f ) by FIN_TOPO:12;
hence  ( A,B are_separated iff ( A ^f misses B & A misses B ^f ) ) by Def1; ::_thesis: verum
end;

theorem Th8: :: FINTOPO4:8
for FT being non empty filled RelStr
for A, B being Subset of FT st FT is symmetric & A ^b misses B holds
A misses B ^b
proof
let FT be non empty filled RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric & A ^b misses B holds
A misses B ^b
let A, B be Subset of FT; ::_thesis: ( FT is symmetric & A ^b misses B implies A misses B ^b )
assume that
A1: FT is symmetric and
A2: A ^b misses B ; ::_thesis: A misses B ^b
now__::_thesis:_not_A_meets_B_^b
assume  A meets B ^b ; ::_thesis: contradiction
then consider x being set  such that
A3: x in A and
A4: x in B ^b by XBOOLE_0:3;
consider x2 being Element of FT such that
A5: x2 = x and
A6: U_FT x2 meets B by A4;
set y = the Element of (U_FT x2) /\ B;
A7: (U_FT x2) /\ B <> {} by A6, XBOOLE_0:def_7;
then A8: the Element of (U_FT x2) /\ B in U_FT x2 by XBOOLE_0:def_4;
then reconsider y2 = the Element of (U_FT x2) /\ B as Element of FT ;
 x2 in U_FT y2 by A1, A8, FIN_TOPO:def_13;
then  x2 in (U_FT y2) /\ A by A3, A5, XBOOLE_0:def_4;
then  U_FT y2 meets A by XBOOLE_0:def_7;
then A9: y2 in A ^b ;
 the Element of (U_FT x2) /\ B in B by A7, XBOOLE_0:def_4;
hence  contradiction by A2, A9, XBOOLE_0:3; ::_thesis: verum
end;
hence  A misses B ^b ; ::_thesis: verum
end;

theorem :: FINTOPO4:9
for FT being non empty filled RelStr
for A, B being Subset of FT st FT is symmetric & A misses B ^b holds
A ^b misses B by Th8;

theorem :: FINTOPO4:10
for FT being non empty filled RelStr
for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff A ^b misses B )
proof
let FT be non empty filled RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff A ^b misses B )
let A, B be Subset of FT; ::_thesis: ( FT is symmetric implies ( A,B are_separated iff A ^b misses B ) )
assume A1: FT is symmetric ; ::_thesis: ( A,B are_separated iff A ^b misses B )
thus  ( A,B are_separated implies A ^b misses B ) by Def1; ::_thesis: ( A ^b misses B implies A,B are_separated )
thus  ( A ^b misses B implies A,B are_separated ) ::_thesis: verum
proof
assume A2: A ^b misses B ; ::_thesis: A,B are_separated
then  A misses B ^b by A1, Th8;
hence  A,B are_separated by A2, Def1; ::_thesis: verum
end;
end;

theorem :: FINTOPO4:11
for FT being non empty filled RelStr
for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff A misses B ^b )
proof
let FT be non empty filled RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric holds
( A,B are_separated iff A misses B ^b )
let A, B be Subset of FT; ::_thesis: ( FT is symmetric implies ( A,B are_separated iff A misses B ^b ) )
assume A1: FT is symmetric ; ::_thesis: ( A,B are_separated iff A misses B ^b )
thus  ( A,B are_separated implies A misses B ^b ) by Def1; ::_thesis: ( A misses B ^b implies A,B are_separated )
thus  ( A misses B ^b implies A,B are_separated ) ::_thesis: verum
proof
assume A2: A misses B ^b ; ::_thesis: A,B are_separated
then  A ^b misses B by A1, Th8;
hence  A,B are_separated by A2, Def1; ::_thesis: verum
end;
end;

theorem Th12: :: FINTOPO4:12
for FT being non empty filled RelStr
for IT being Subset of FT st FT is symmetric holds
( IT is connected iff for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT )
proof
let FT be non empty filled RelStr ; ::_thesis: for IT being Subset of FT st FT is symmetric holds
( IT is connected iff for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT )
let IT be Subset of FT; ::_thesis: ( FT is symmetric implies ( IT is connected iff for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT ) )
assume A1: FT is symmetric ; ::_thesis: ( IT is connected iff for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT )
A2: now__::_thesis:_(_(_for_A,_B_being_Subset_of_FT_st_IT_=_A_\/_B_&_A,B_are_separated_&_not_A_=_IT_holds_
B_=_IT_)_implies_IT_is_connected_)
assume A3: for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT ; ::_thesis: IT is connected
 for A, B being Subset of FT st IT = A \/ B & A <> {} & B <> {} & A misses B holds
A ^b meets B
proof
let A, B be Subset of FT; ::_thesis: ( IT = A \/ B & A <> {} & B <> {} & A misses B implies A ^b meets B )
assume that
A4: IT = A \/ B and
A5: ( A <> {} & B <> {} ) and
 A misses B ; ::_thesis: A ^b meets B
now__::_thesis:_not_A_^b_misses_B
assume A6: A ^b misses B ; ::_thesis: contradiction
now__::_thesis:_not_A_meets_B_^b
assume  A meets B ^b ; ::_thesis: contradiction
then consider x being set  such that
A7: x in A and
A8: x in B ^b by XBOOLE_0:3;
consider x2 being Element of FT such that
A9: x2 = x and
A10: U_FT x2 meets B by A8;
set y = the Element of (U_FT x2) /\ B;
A11: (U_FT x2) /\ B <> {} by A10, XBOOLE_0:def_7;
then A12: the Element of (U_FT x2) /\ B in U_FT x2 by XBOOLE_0:def_4;
then reconsider y2 = the Element of (U_FT x2) /\ B as Element of FT ;
 x2 in U_FT y2 by A1, A12, FIN_TOPO:def_13;
then  x2 in (U_FT y2) /\ A by A7, A9, XBOOLE_0:def_4;
then  U_FT y2 meets A by XBOOLE_0:def_7;
then A13: y2 in A ^b ;
 the Element of (U_FT x2) /\ B in B by A11, XBOOLE_0:def_4;
hence  contradiction by A6, A13, XBOOLE_0:3; ::_thesis: verum
end;
then  A,B are_separated by A6, Def1;
then A14: ( A = IT or B = IT ) by A3, A4;
A15: A c= A ^b by FIN_TOPO:13;
 (A ^b) /\ B = {} by A6, XBOOLE_0:def_7;
then  A /\ B = {} by A15, XBOOLE_1:3, XBOOLE_1:26;
hence  contradiction by A4, A5, A14, XBOOLE_1:21; ::_thesis: verum
end;
hence  A ^b meets B ; ::_thesis: verum
end;
hence  IT is connected by FIN_TOPO:def_16; ::_thesis: verum
end;
now__::_thesis:_(_IT_is_connected_implies_for_A,_B_being_Subset_of_FT_st_IT_=_A_\/_B_&_A,B_are_separated_&_not_A_=_IT_holds_
B_=_IT_)
assume A16: IT is connected ; ::_thesis: for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT
thus  for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT ::_thesis: verum
proof
let A, B be Subset of FT; ::_thesis: ( IT = A \/ B & A,B are_separated & not A = IT implies B = IT )
assume that
A17: IT = A \/ B and
A18: A,B are_separated ; ::_thesis: ( A = IT or B = IT )
A19: A misses B by A18, Th6;
now__::_thesis:_(_A_<>_{}_&_not_A_=_IT_implies_B_=_IT_)
assume A20: A <> {} ; ::_thesis: ( A = IT or B = IT )
now__::_thesis:_not_B_<>_{}
assume  B <> {} ; ::_thesis: contradiction
then  A ^b meets B by A16, A17, A19, A20, FIN_TOPO:def_16;
hence  contradiction by A18, Def1; ::_thesis: verum
end;
hence  ( A = IT or B = IT ) by A17; ::_thesis: verum
end;
hence  ( A = IT or B = IT ) by A17; ::_thesis: verum
end;
end;
hence  ( IT is connected iff for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT ) by A2; ::_thesis: verum
end;

theorem :: FINTOPO4:13
for FT being non empty filled RelStr
for B being Subset of FT st FT is symmetric holds
( B is connected iff for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) )
proof
let FT be non empty filled RelStr ; ::_thesis: for B being Subset of FT st FT is symmetric holds
( B is connected iff for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) )
let B be Subset of FT; ::_thesis: ( FT is symmetric implies ( B is connected iff for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ) )
assume A1: FT is symmetric ; ::_thesis: ( B is connected iff for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) )
thus  ( B is connected implies for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ) ::_thesis: ( ( for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ) implies B is connected )
proof
assume A2: B is connected ; ::_thesis: for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C )
 for C being Subset of FT st C c= B & C ^b misses B \ C & not C = {} holds
B \ C = {}
proof
let C be Subset of FT; ::_thesis: ( C c= B & C ^b misses B \ C & not C = {} implies B \ C = {} )
assume that
A3: C c= B and
A4: C ^b misses B \ C ; ::_thesis: ( C = {} or B \ C = {} )
 C misses (B \ C) ^b by A1, A4, Th8;
then A5: C,B \ C are_separated by A4, Def1;
C \/ (B \ C) = C \/ B by XBOOLE_1:39
.= B by A3, XBOOLE_1:12 ;
then  ( C = B or B \ C = B ) by A1, A2, A5, Th12;
hence  ( C = {} or B \ C = {} ) by A3, XBOOLE_1:37, XBOOLE_1:38; ::_thesis: verum
end;
hence  for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ; ::_thesis: verum
end;
thus  ( ( for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ) implies B is connected ) ::_thesis: verum
proof
assume A6: for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ; ::_thesis: B is connected
 for A, B2 being Subset of FT st B = A \/ B2 & A,B2 are_separated & not A = B holds
B2 = B
proof
let A, B2 be Subset of FT; ::_thesis: ( B = A \/ B2 & A,B2 are_separated & not A = B implies B2 = B )
assume that
A7: B = A \/ B2 and
A8: A,B2 are_separated ; ::_thesis: ( A = B or B2 = B )
A9: (A \/ B2) \ A = B2 \ A by XBOOLE_1:40;
 A ^b misses B2 by A8, Def1;
then  A ^b misses B \ A by A7, A9, XBOOLE_1:36, XBOOLE_1:63;
then  ( A = {} or B \ A = {} ) by A6, A7, XBOOLE_1:7;
then A10: ( B = B2 or B c= A ) by A7, XBOOLE_1:37;
 A c= B by A7, XBOOLE_1:7;
hence  ( A = B or B2 = B ) by A10, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  B is connected by A1, Th12; ::_thesis: verum
end;
end;

definition
let FT1, FT2 be non empty RelStr ;
let f be Function of FT1,FT2;
let n be Element of NAT ;
predf is_continuous n means :Def2: :: FINTOPO4:def 2
 for x being Element of FT1
for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds
f .: (U_FT (x,0)) c= U_FT (y,n);
end;

:: deftheorem Def2 defines is_continuous FINTOPO4:def_2_:_
 for FT1, FT2 being non empty RelStr
for f being Function of FT1,FT2
for n being Element of NAT holds
( f is_continuous n iff for x being Element of FT1
for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds
f .: (U_FT (x,0)) c= U_FT (y,n) );

theorem :: FINTOPO4:14
for FT1 being non empty RelStr
for FT2 being non empty filled RelStr
for n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous 0 holds
f is_continuous n
proof
let FT1 be non empty RelStr ; ::_thesis: for FT2 being non empty filled RelStr
for n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous 0 holds
f is_continuous n
let FT2 be non empty filled RelStr ; ::_thesis: for n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous 0 holds
f is_continuous n
let n be Element of NAT ; ::_thesis: for f being Function of FT1,FT2 st f is_continuous 0 holds
f is_continuous n
let f be Function of FT1,FT2; ::_thesis: ( f is_continuous 0 implies f is_continuous n )
assume A1: f is_continuous 0 ; ::_thesis: f is_continuous n
 for x being Element of FT1
for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds
f .: (U_FT (x,0)) c= U_FT (y,n)
proof
let x be Element of FT1; ::_thesis: for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds
f .: (U_FT (x,0)) c= U_FT (y,n)
let y be Element of FT2; ::_thesis: ( x in the carrier of FT1 & y = f . x implies f .: (U_FT (x,0)) c= U_FT (y,n) )
assume that
 x in the carrier of FT1 and
A2: y = f . x ; ::_thesis: f .: (U_FT (x,0)) c= U_FT (y,n)
 ( U_FT y = U_FT (y,0) & U_FT (y,n) = Finf ((U_FT y),n) ) by FINTOPO3:47, FINTOPO3:def_10;
then A3: U_FT (y,0) c= U_FT (y,n) by FINTOPO3:36;
 f .: (U_FT (x,0)) c= U_FT (y,0) by A1, A2, Def2;
hence  f .: (U_FT (x,0)) c= U_FT (y,n) by A3, XBOOLE_1:1; ::_thesis: verum
end;
hence  f is_continuous n by Def2; ::_thesis: verum
end;

theorem :: FINTOPO4:15
for FT1 being non empty RelStr
for FT2 being non empty filled RelStr
for n0, n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous n0 & n0 <= n holds
f is_continuous n
proof
let FT1 be non empty RelStr ; ::_thesis: for FT2 being non empty filled RelStr
for n0, n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous n0 & n0 <= n holds
f is_continuous n
let FT2 be non empty filled RelStr ; ::_thesis: for n0, n being Element of NAT
for f being Function of FT1,FT2 st f is_continuous n0 & n0 <= n holds
f is_continuous n
let n0, n be Element of NAT ; ::_thesis: for f being Function of FT1,FT2 st f is_continuous n0 & n0 <= n holds
f is_continuous n
let f be Function of FT1,FT2; ::_thesis: ( f is_continuous n0 & n0 <= n implies f is_continuous n )
assume that
A1: f is_continuous n0 and
A2: n0 <= n ; ::_thesis: f is_continuous n
 for x being Element of FT1
for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds
f .: (U_FT (x,0)) c= U_FT (y,n)
proof
let x be Element of FT1; ::_thesis: for y being Element of FT2 st x in the carrier of FT1 & y = f . x holds
f .: (U_FT (x,0)) c= U_FT (y,n)
let y be Element of FT2; ::_thesis: ( x in the carrier of FT1 & y = f . x implies f .: (U_FT (x,0)) c= U_FT (y,n) )
assume that
 x in the carrier of FT1 and
A3: y = f . x ; ::_thesis: f .: (U_FT (x,0)) c= U_FT (y,n)
 ( U_FT (y,n0) = Finf ((U_FT y),n0) & U_FT (y,n) = Finf ((U_FT y),n) ) by FINTOPO3:def_10;
then A4: U_FT (y,n0) c= U_FT (y,n) by A2, Th1;
 f .: (U_FT (x,0)) c= U_FT (y,n0) by A1, A3, Def2;
hence  f .: (U_FT (x,0)) c= U_FT (y,n) by A4, XBOOLE_1:1; ::_thesis: verum
end;
hence  f is_continuous n by Def2; ::_thesis: verum
end;

theorem Th16: :: FINTOPO4:16
for FT1, FT2 being non empty RelStr
for A being Subset of FT1
for B being Subset of FT2
for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b) c= B ^b
proof
let FT1, FT2 be non empty RelStr ; ::_thesis: for A being Subset of FT1
for B being Subset of FT2
for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b) c= B ^b
let A be Subset of FT1; ::_thesis: for B being Subset of FT2
for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b) c= B ^b
let B be Subset of FT2; ::_thesis: for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b) c= B ^b
let f be Function of FT1,FT2; ::_thesis: ( f is_continuous 0 & B = f .: A implies f .: (A ^b) c= B ^b )
assume that
A1: f is_continuous 0 and
A2: B = f .: A ; ::_thesis: f .: (A ^b) c= B ^b
thus  f .: (A ^b) c= B ^b ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (A ^b) or y in B ^b )
assume  y in f .: (A ^b) ; ::_thesis: y in B ^b
then consider x being set  such that
A3: x in dom f and
A4: x in A ^b and
A5: y = f . x by FUNCT_1:def_6;
reconsider x0 = x as Element of FT1 by A3;
reconsider y0 = y as Element of FT2 by A3, A5, FUNCT_2:5;
 f .: (U_FT (x0,0)) c= U_FT (y0,0) by A1, A5, Def2;
then  f .: (U_FT x0) c= U_FT (y0,0) by FINTOPO3:47;
then  f .: (U_FT x0) c= U_FT y0 by FINTOPO3:47;
then A6: ( f .: ((U_FT x0) /\ A) c= (f .: (U_FT x0)) /\ (f .: A) & (f .: (U_FT x0)) /\ (f .: A) c= (U_FT y0) /\ (f .: A) ) by RELAT_1:121, XBOOLE_1:26;
 ex z being Element of FT1 st
( z = x & U_FT z meets A ) by A4;
then A7: (U_FT x0) /\ A <> {} by XBOOLE_0:def_7;
 dom f = the carrier of FT1 by FUNCT_2:def_1;
then  f .: ((U_FT x0) /\ A) <> {} by A7, RELAT_1:119;
then  (U_FT y0) /\ (f .: A) <> {} by A6;
then  U_FT y0 meets B by A2, XBOOLE_0:def_7;
hence  y in B ^b ; ::_thesis: verum
end;
end;

theorem :: FINTOPO4:17
for FT1, FT2 being non empty RelStr
for A being Subset of FT1
for B being Subset of FT2
for f being Function of FT1,FT2 st A is connected & f is_continuous 0 & B = f .: A holds
B is connected
proof
let FT1, FT2 be non empty RelStr ; ::_thesis: for A being Subset of FT1
for B being Subset of FT2
for f being Function of FT1,FT2 st A is connected & f is_continuous 0 & B = f .: A holds
B is connected
let A be Subset of FT1; ::_thesis: for B being Subset of FT2
for f being Function of FT1,FT2 st A is connected & f is_continuous 0 & B = f .: A holds
B is connected
let B be Subset of FT2; ::_thesis: for f being Function of FT1,FT2 st A is connected & f is_continuous 0 & B = f .: A holds
B is connected
let f be Function of FT1,FT2; ::_thesis: ( A is connected & f is_continuous 0 & B = f .: A implies B is connected )
assume that
A1: A is connected and
A2: f is_continuous 0 and
A3: B = f .: A ; ::_thesis: B is connected
 for B2, C2 being Subset of FT2 st B = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 holds
B2 ^b meets C2
proof
let B2, C2 be Subset of FT2; ::_thesis: ( B = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 implies B2 ^b meets C2 )
assume that
A4: B = B2 \/ C2 and
A5: B2 <> {} and
A6: C2 <> {} and
A7: B2 misses C2 ; ::_thesis: B2 ^b meets C2
reconsider C1 = f " C2 as Subset of FT1 ;
reconsider C10 = C1 /\ A as Subset of FT1 ;
reconsider B1 = f " B2 as Subset of FT1 ;
reconsider B10 = B1 /\ A as Subset of FT1 ;
A8: C10 c= C1 by XBOOLE_1:17;
set x6 = the Element of C2;
 the Element of C2 in B by A4, A6, XBOOLE_0:def_3;
then consider z6 being set  such that
A9: z6 in dom f and
A10: z6 in A and
A11: the Element of C2 = f . z6 by A3, FUNCT_1:def_6;
 z6 in f " C2 by A6, A9, A11, FUNCT_1:def_7;
then A12: C10 <> {} by A10, XBOOLE_0:def_4;
set x5 = the Element of B2;
 the Element of B2 in B by A4, A5, XBOOLE_0:def_3;
then consider z5 being set  such that
A13: z5 in dom f and
A14: z5 in A and
A15: the Element of B2 = f . z5 by A3, FUNCT_1:def_6;
 A c= the carrier of FT1 ;
then A16: A c= dom f by FUNCT_2:def_1;
 B2 /\ C2 = {} by A7, XBOOLE_0:def_7;
then  f " (B2 /\ C2) = {} ;
then  ( B10 c= B1 & (f " B2) /\ (f " C2) = {} ) by FUNCT_1:68, XBOOLE_1:17;
then  B10 /\ C10 = {} by A8, XBOOLE_1:3, XBOOLE_1:27;
then A17: B10 misses C10 by XBOOLE_0:def_7;
 (f " B2) \/ (f " C2) = f " (f .: A) by A3, A4, RELAT_1:140;
then  A c= B1 \/ C1 by A16, FUNCT_1:76;
then  A c= A /\ (B1 \/ C1) by XBOOLE_1:19;
then A18: A c= B10 \/ C10 by XBOOLE_1:23;
 ( B10 c= A & C10 c= A ) by XBOOLE_1:17;
then  B10 \/ C10 c= A by XBOOLE_1:8;
then A19: A = B10 \/ C10 by A18, XBOOLE_0:def_10;
 z5 in f " B2 by A5, A13, A15, FUNCT_1:def_7;
then  B10 <> {} by A14, XBOOLE_0:def_4;
then  B10 ^b meets C10 by A1, A19, A12, A17, FIN_TOPO:def_16;
then A20: (B10 ^b) /\ C10 <> {} by XBOOLE_0:def_7;
reconsider B20 = f .: B1 as Subset of FT2 ;
A21: dom f = the carrier of FT1 by FUNCT_2:def_1;
 f .: B1 c= B2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: B1 or y in B2 )
assume  y in f .: B1 ; ::_thesis: y in B2
then  ex x2 being set st
( x2 in dom f & x2 in B1 & y = f . x2 ) by FUNCT_1:def_6;
hence  y in B2 by FUNCT_1:def_7; ::_thesis: verum
end;
then A22: B20 ^b c= B2 ^b by FIN_TOPO:14;
 f .: (B1 ^b) c= B20 ^b by A2, Th16;
then  f .: (B1 ^b) c= B2 ^b by A22, XBOOLE_1:1;
then A23: ( (f .: (B1 ^b)) /\ (f .: C1) c= (f .: (B1 ^b)) /\ C2 & (f .: (B1 ^b)) /\ C2 c= (B2 ^b) /\ C2 ) by FUNCT_1:75, XBOOLE_1:26;
 B10 ^b c= B1 ^b by FIN_TOPO:14, XBOOLE_1:17;
then  (B1 ^b) /\ C1 <> {} by A8, A20, XBOOLE_1:3, XBOOLE_1:27;
then  f .: ((B1 ^b) /\ C1) <> {} by A21, RELAT_1:119;
then  (f .: (B1 ^b)) /\ (f .: C1) <> {} by RELAT_1:121, XBOOLE_1:3;
then  (B2 ^b) /\ C2 <> {} by A23;
hence  B2 ^b meets C2 by XBOOLE_0:def_7; ::_thesis: verum
end;
hence  B is connected by FIN_TOPO:def_16; ::_thesis: verum
end;

definition
let n be Nat;
func Nbdl1 n ->  Relation of (Seg n) means :Def3: :: FINTOPO4:def 3
 for i being Element of NAT st i in Seg n holds
Im (it,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))};
existence
 ex b1 being Relation of (Seg n) st
for i being Element of NAT st i in Seg n holds
Im (b1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))}
proof
deffunc H1( Nat) ->  set = {$1,(max (($1 -' 1),1)),(min (($1 + 1),n))};
A1: for x being Element of NAT st x in Seg n holds
H1(x) c= Seg n
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies H1(i) c= Seg n )
set y0 = {i,(max ((i -' 1),1)),(min ((i + 1),n))};
assume A2: i in Seg n ; ::_thesis: H1(i) c= Seg n
then  Seg n <> {} ;
then  n > 0 ;
then A3: 0 + 1 <= n by NAT_1:13;
thus  {i,(max ((i -' 1),1)),(min ((i + 1),n))} c= Seg n ::_thesis: verum
proof
let z1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z1 in {i,(max ((i -' 1),1)),(min ((i + 1),n))} or z1 in Seg n )
assume A4: z1 in {i,(max ((i -' 1),1)),(min ((i + 1),n))} ; ::_thesis: z1 in Seg n
then  ( z1 = i or z1 = max ((i -' 1),1) or z1 = min ((i + 1),n) ) by ENUMSET1:def_1;
then reconsider z2 = z1 as Element of NAT by ORDINAL1:def_12;
A5: now__::_thesis:_(_z1_=_max_((i_-'_1),1)_implies_z1_in_Seg_n_)
 ( i -' 1 <= i & i <= n ) by A2, FINSEQ_1:1, NAT_D:35;
then  i -' 1 <= n by XXREAL_0:2;
then A6: ( 1 <= max ((i -' 1),1) & max ((i -' 1),1) <= n ) by A3, XXREAL_0:28, XXREAL_0:30;
assume  z1 = max ((i -' 1),1) ; ::_thesis: z1 in Seg n
hence  z1 in Seg n by A6; ::_thesis: verum
end;
now__::_thesis:_(_z1_=_min_((i_+_1),n)_implies_z2_in_Seg_n_)
 1 <= i + 1 by NAT_1:12;
then A7: 1 <= min ((i + 1),n) by A3, XXREAL_0:20;
A8: min ((i + 1),n) <= n by XXREAL_0:17;
assume  z1 = min ((i + 1),n) ; ::_thesis: z2 in Seg n
hence  z2 in Seg n by A7, A8; ::_thesis: verum
end;
hence  z1 in Seg n by A2, A4, A5, ENUMSET1:def_1; ::_thesis: verum
end;
end;
consider f being Relation of (Seg n) such that
A9: for x3 being Element of NAT st x3 in Seg n holds
Im (f,x3) = H1(x3) from RELSET_1:sch_3(A1);
take  f ; ::_thesis: for i being Element of NAT st i in Seg n holds
Im (f,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))}
thus  for i being Element of NAT st i in Seg n holds
Im (f,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} by A9; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
Im (b1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) & ( for i being Element of NAT st i in Seg n holds
Im (b2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) holds
b1 = b2
proof
thus  for f1, f2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
Im (f1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) & ( for i being Element of NAT st i in Seg n holds
Im (f2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) holds
f1 = f2 ::_thesis: verum
proof
let f1, f2 be Relation of (Seg n); ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
Im (f1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) & ( for i being Element of NAT st i in Seg n holds
Im (f2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ) implies f1 = f2 )
assume that
A10: for i being Element of NAT st i in Seg n holds
Im (f1,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} and
A11: for i being Element of NAT st i in Seg n holds
Im (f2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} ; ::_thesis: f1 = f2
 for x being set st x in Seg n holds
Im (f1,x) = Im (f2,x)
proof
let x be set ; ::_thesis: ( x in Seg n implies Im (f1,x) = Im (f2,x) )
assume A12: x in Seg n ; ::_thesis: Im (f1,x) = Im (f2,x)
then reconsider i2 = x as Element of NAT ;
 Im (f1,i2) = {i2,(max ((i2 -' 1),1)),(min ((i2 + 1),n))} by A10, A12;
hence  Im (f1,x) = Im (f2,x) by A11, A12; ::_thesis: verum
end;
hence  f1 = f2 by RELSET_1:31; ::_thesis: verum
end;
end;
end;

:: deftheorem Def3 defines Nbdl1 FINTOPO4:def_3_:_
 for n being Nat
for b2 being Relation of (Seg n) holds
( b2 = Nbdl1 n iff for i being Element of NAT st i in Seg n holds
Im (b2,i) = {i,(max ((i -' 1),1)),(min ((i + 1),n))} );

definition
let n be Nat;
assume A1: n > 0 ;
func FTSL1 n ->  non empty RelStr  equals :Def4: :: FINTOPO4:def 4
 RelStr(# (Seg n),(Nbdl1 n) #);
correctness
coherence
RelStr(# (Seg n),(Nbdl1 n) #) is non empty RelStr ;
by A1;
end;

:: deftheorem Def4 defines FTSL1 FINTOPO4:def_4_:_
 for n being Nat st n > 0 holds
FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #);

theorem :: FINTOPO4:18
for n being Nat st n > 0 holds
FTSL1 n is filled
proof
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
end;

theorem :: FINTOPO4:19
for n being Nat st n > 0 holds
FTSL1 n is symmetric
proof
let n be Nat; ::_thesis: ( n > 0 implies FTSL1 n is symmetric )
assume  n > 0 ; ::_thesis: FTSL1 n is symmetric
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: ( 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;
now__::_thesis:_(_y_in_U_FT_x_implies_x_in_U_FT_y_)
A6: now__::_thesis:_(_y_=_max_((i_-'_1),1)_implies_x_in_U_FT_y_)
assume A7: y = max ((i -' 1),1) ; ::_thesis: x in U_FT y
now__::_thesis:_(_(_i_-'_1_>=_1_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_or_(_i_-'_1_<_1_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_)
percases ( i -' 1 >= 1 or i -' 1 < 1 ) ;
caseA8: i -' 1 >= 1 ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
then A9: y = i -' 1 by A7, XXREAL_0:def_10;
now__::_thesis:_(_(_i_-_1_>=_0_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_or_(_i_-_1_<_0_&_contradiction_)_)
percases ( i - 1 >= 0 or i - 1 < 0 ) ;
case i - 1 >= 0 ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
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: verum
end;
case i - 1 < 0 ; ::_thesis: contradiction
hence  contradiction by A8, XREAL_0:def_2; ::_thesis: verum
end;
end;
end;
hence  ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; ::_thesis: verum
end;
caseA10: i -' 1 < 1 ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
A11: now__::_thesis:_not_i_>_1
assume  i > 1 ; ::_thesis: contradiction
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: verum
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: verum
end;
end;
end;
hence  x in U_FT y by A4, ENUMSET1:def_1; ::_thesis: verum
end;
assume A13: y in U_FT x ; ::_thesis: x in U_FT y
A14: now__::_thesis:_(_y_=_min_((i_+_1),n)_implies_x_in_U_FT_y_)
assume  y = min ((i + 1),n) ; ::_thesis: x in U_FT y
now__::_thesis:_(_(_y_=_i_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_or_(_y_=_max_((i_-'_1),1)_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_or_(_y_=_min_((i_+_1),n)_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_)
percases ( y = i or y = max ((i -' 1),1) or y = min ((i + 1),n) ) by A5, A13, ENUMSET1:def_1;
case y = i ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
hence  ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; ::_thesis: verum
end;
caseA15: y = max ((i -' 1),1) ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
now__::_thesis:_(_(_i_-'_1_>=_1_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_or_(_i_-'_1_<_1_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_)
percases ( i -' 1 >= 1 or i -' 1 < 1 ) ;
caseA16: i -' 1 >= 1 ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
then A17: y = i -' 1 by A15, XXREAL_0:def_10;
now__::_thesis:_(_(_i_-_1_>=_0_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_or_(_i_-_1_<_0_&_contradiction_)_)
percases ( i - 1 >= 0 or i - 1 < 0 ) ;
case i - 1 >= 0 ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
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: verum
end;
case i - 1 < 0 ; ::_thesis: contradiction
hence  contradiction by A16, XREAL_0:def_2; ::_thesis: verum
end;
end;
end;
hence  ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; ::_thesis: verum
end;
caseA18: i -' 1 < 1 ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
A19: now__::_thesis:_not_i_>_1
assume  i > 1 ; ::_thesis: contradiction
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: verum
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: verum
end;
end;
end;
hence  ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; ::_thesis: verum
end;
caseA21: y = min ((i + 1),n) ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
now__::_thesis:_(_(_i_+_1_<=_n_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_or_(_i_+_1_>_n_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_)
percases ( i + 1 <= n or i + 1 > n ) ;
case i + 1 <= n ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
then A22: y = i + 1 by A21, XXREAL_0:def_9;
then A23: j - 1 = j -' 1 by XREAL_0:def_2;
now__::_thesis:_(_(_j_-_1_>=_1_&_(_x_=_j_or_x_=_max_((j_-'_1),1)_or_x_=_min_((j_+_1),n)_)_)_or_(_j_-_1_<_1_&_contradiction_)_)
percases ( j - 1 >= 1 or j - 1 < 1 ) ;
case j - 1 >= 1 ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
hence  ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) by A22, A23, XXREAL_0:def_10; ::_thesis: verum
end;
case j - 1 < 1 ; ::_thesis: contradiction
hence  contradiction by A1, A22, FINSEQ_1:1; ::_thesis: verum
end;
end;
end;
hence  ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; ::_thesis: verum
end;
caseA24: i + 1 > n ; ::_thesis: ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) )
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: verum
end;
end;
end;
hence  ( x = j or x = max ((j -' 1),1) or x = min ((j + 1),n) ) ; ::_thesis: verum
end;
end;
end;
hence  x in U_FT y by A4, ENUMSET1:def_1; ::_thesis: verum
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: verum
end;
hence  ( not y in U_FT x or x in U_FT y ) ; ::_thesis: verum
end;

definition
let n be Nat;
func Nbdc1 n ->  Relation of (Seg n) means :Def5: :: FINTOPO4:def 5
 for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (it,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (it,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (it,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (it,i) = {i} ) );
existence
 ex b1 being Relation of (Seg n) st
for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b1,i) = {i} ) )
proof
defpred S1[ set , set ] means  for i being Element of NAT st i = $1 holds
( ( 1 < i & i < n implies $2 = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies $2 = {i,n,(i + 1)} ) & ( 1 < i & i = n implies $2 = {i,(i -' 1),1} ) & ( i = 1 & i = n implies $2 = {i} ) );
A1: for x being set st x in Seg n holds
ex y being set st
( y in bool (Seg n) & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in Seg n implies ex y being set st
( y in bool (Seg n) & S1[x,y] ) )
assume A2: x in Seg n ; ::_thesis: ex y being set st
( y in bool (Seg n) & S1[x,y] )
then reconsider i2 = x as Element of NAT ;
A3: ( 1 <= i2 & i2 <= n ) by A2, FINSEQ_1:1;
now__::_thesis:_(_(_1_<_i2_&_i2_<_n_&_ex_y_being_set_st_
(_y_in_bool_(Seg_n)_&_S1[x,y]_)_)_or_(_i2_=_1_&_i2_<_n_&_ex_y_being_set_st_
(_y_in_bool_(Seg_n)_&_S1[x,y]_)_)_or_(_1_<_i2_&_i2_=_n_&_ex_y_being_set_st_
(_y_in_bool_(Seg_n)_&_S1[x,y]_)_)_or_(_i2_=_1_&_i2_=_n_&_ex_y_being_set_st_
(_y_in_bool_(Seg_n)_&_S1[x,y]_)_)_)
percases ( ( 1 < i2 & i2 < n ) or ( i2 = 1 & i2 < n ) or ( 1 < i2 & i2 = n ) or ( i2 = 1 & i2 = n ) ) by A3, XXREAL_0:1;
caseA4: ( 1 < i2 & i2 < n ) ; ::_thesis: ex y being set st
( y in bool (Seg n) & S1[x,y] )
 i2 <= i2 + 1 by NAT_1:12;
then A5: 1 < i2 + 1 by A4, XXREAL_0:2;
 i2 + 1 <= n by A4, NAT_1:13;
then A6: i2 + 1 in Seg n by A5;
set y0 = {i2,(i2 -' 1),(i2 + 1)};
 i2 - 1 > 0 by A4, XREAL_1:50;
then  i2 -' 1 > 0 by XREAL_0:def_2;
then A7: i2 -' 1 >= 0 + 1 by NAT_1:13;
 i2 -' 1 <= i2 by NAT_D:35;
then  i2 -' 1 < n by A4, XXREAL_0:2;
then A8: i2 -' 1 in Seg n by A7;
A9: {i2,(i2 -' 1),(i2 + 1)} c= Seg n
proof
let z1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z1 in {i2,(i2 -' 1),(i2 + 1)} or z1 in Seg n )
assume  z1 in {i2,(i2 -' 1),(i2 + 1)} ; ::_thesis: z1 in Seg n
hence  z1 in Seg n by A2, A8, A6, ENUMSET1:def_1; ::_thesis: verum
end;
 S1[x,{i2,(i2 -' 1),(i2 + 1)}] by A4;
hence  ex y being set st
( y in bool (Seg n) & S1[x,y] ) by A9; ::_thesis: verum
end;
caseA10: ( i2 = 1 & i2 < n ) ; ::_thesis: ex y being set st
( y in bool (Seg n) & S1[x,y] )
then  i2 + 1 <= n by NAT_1:13;
then A11: i2 + 1 in Seg n by A10;
set y0 = {i2,n,(i2 + 1)};
A12: n in Seg n by A10, FINSEQ_1:1;
A13: {i2,n,(i2 + 1)} c= Seg n
proof
let z1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z1 in {i2,n,(i2 + 1)} or z1 in Seg n )
assume  z1 in {i2,n,(i2 + 1)} ; ::_thesis: z1 in Seg n
hence  z1 in Seg n by A2, A12, A11, ENUMSET1:def_1; ::_thesis: verum
end;
 S1[x,{i2,n,(i2 + 1)}] by A10;
hence  ex y being set st
( y in bool (Seg n) & S1[x,y] ) by A13; ::_thesis: verum
end;
caseA14: ( 1 < i2 & i2 = n ) ; ::_thesis: ex y being set st
( y in bool (Seg n) & S1[x,y] )
then  i2 - 1 > 0 by XREAL_1:50;
then  i2 -' 1 > 0 by XREAL_0:def_2;
then A15: i2 -' 1 >= 0 + 1 by NAT_1:13;
set y0 = {i2,(i2 -' 1),1};
A16: 1 in Seg n by A14;
 i2 -' 1 <= n by A14, NAT_D:35;
then A17: i2 -' 1 in Seg n by A15;
A18: {i2,(i2 -' 1),1} c= Seg n
proof
let z1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z1 in {i2,(i2 -' 1),1} or z1 in Seg n )
assume  z1 in {i2,(i2 -' 1),1} ; ::_thesis: z1 in Seg n
hence  z1 in Seg n by A2, A17, A16, ENUMSET1:def_1; ::_thesis: verum
end;
 S1[x,{i2,(i2 -' 1),1}] by A14;
hence  ex y being set st
( y in bool (Seg n) & S1[x,y] ) by A18; ::_thesis: verum
end;
caseA19: ( i2 = 1 & i2 = n ) ; ::_thesis: ex y being set st
( y in bool (Seg n) & S1[x,y] )
set y0 = {i2};
A20: {i2} c= Seg n
proof
let z1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z1 in {i2} or z1 in Seg n )
assume  z1 in {i2} ; ::_thesis: z1 in Seg n
hence  z1 in Seg n by A2, TARSKI:def_1; ::_thesis: verum
end;
 S1[x,{i2}] by A19;
hence  ex y being set st
( y in bool (Seg n) & S1[x,y] ) by A20; ::_thesis: verum
end;
end;
end;
hence  ex y being set st
( y in bool (Seg n) & S1[x,y] ) ; ::_thesis: verum
end;
consider f2 being Function of (Seg n),(bool (Seg n)) such that
A21: for x3 being set st x3 in Seg n holds
S1[x3,f2 . x3] from FUNCT_2:sch_1(A1);
consider R being Relation of (Seg n) such that
A22: for i being set st i in Seg n holds
Im (R,i) = f2 . i by FUNCT_2:93;
take  R ; ::_thesis: for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) )
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) ) )
assume A23: i in Seg n ; ::_thesis: ( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) )
then  Im (R,i) = f2 . i by A22;
hence  ( ( 1 < i & i < n implies Im (R,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (R,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (R,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (R,i) = {i} ) ) by A21, A23; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of (Seg n) st ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b1,i) = {i} ) ) ) & ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b2,i) = {i} ) ) ) holds
b1 = b2
proof
let f1, f2 be Relation of (Seg n); ::_thesis: ( ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (f1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (f1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (f1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (f1,i) = {i} ) ) ) & ( for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (f2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (f2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (f2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (f2,i) = {i} ) ) ) implies f1 = f2 )
assume that
A24: for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (f1,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (f1,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (f1,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (f1,i) = {i} ) ) and
A25: for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (f2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (f2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (f2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (f2,i) = {i} ) ) ; ::_thesis: f1 = f2
 for x being set st x in Seg n holds
Im (f1,x) = Im (f2,x)
proof
let x be set ; ::_thesis: ( x in Seg n implies Im (f1,x) = Im (f2,x) )
assume A26: x in Seg n ; ::_thesis: Im (f1,x) = Im (f2,x)
then reconsider i2 = x as Element of NAT ;
A27: ( 1 <= i2 & i2 <= n ) by A26, FINSEQ_1:1;
percases ( ( 1 < i2 & i2 < n ) or ( i2 = 1 & i2 < n ) or ( 1 < i2 & i2 = n ) or ( i2 = 1 & i2 = n ) ) by A27, XXREAL_0:1;
supposeA28: ( 1 < i2 & i2 < n ) ; ::_thesis: Im (f1,x) = Im (f2,x)
set y0 = {i2,(i2 -' 1),(i2 + 1)};
 Im (f1,x) = {i2,(i2 -' 1),(i2 + 1)} by A24, A26, A28;
hence  Im (f1,x) = Im (f2,x) by A25, A26, A28; ::_thesis: verum
end;
supposeA29: ( i2 = 1 & i2 < n ) ; ::_thesis: Im (f1,x) = Im (f2,x)
set y0 = {i2,n,(i2 + 1)};
 Im (f1,x) = {i2,n,(i2 + 1)} by A24, A26, A29;
hence  Im (f1,x) = Im (f2,x) by A25, A26, A29; ::_thesis: verum
end;
supposeA30: ( 1 < i2 & i2 = n ) ; ::_thesis: Im (f1,x) = Im (f2,x)
set y0 = {i2,(i2 -' 1),1};
 Im (f1,x) = {i2,(i2 -' 1),1} by A24, A26, A30;
hence  Im (f1,x) = Im (f2,x) by A25, A26, A30; ::_thesis: verum
end;
supposeA31: ( i2 = 1 & i2 = n ) ; ::_thesis: Im (f1,x) = Im (f2,x)
set y0 = {i2};
 Im (f1,x) = {i2} by A24, A26, A31;
hence  Im (f1,x) = Im (f2,x) by A25, A26, A31; ::_thesis: verum
end;
end;
end;
hence  f1 = f2 by RELSET_1:31; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines Nbdc1 FINTOPO4:def_5_:_
 for n being Nat
for b2 being Relation of (Seg n) holds
( b2 = Nbdc1 n iff for i being Element of NAT st i in Seg n holds
( ( 1 < i & i < n implies Im (b2,i) = {i,(i -' 1),(i + 1)} ) & ( i = 1 & i < n implies Im (b2,i) = {i,n,(i + 1)} ) & ( 1 < i & i = n implies Im (b2,i) = {i,(i -' 1),1} ) & ( i = 1 & i = n implies Im (b2,i) = {i} ) ) );

definition
let n be Nat;
assume A1: n > 0 ;
func FTSC1 n ->  non empty RelStr  equals :Def6: :: FINTOPO4:def 6
 RelStr(# (Seg n),(Nbdc1 n) #);
correctness
coherence
RelStr(# (Seg n),(Nbdc1 n) #) is non empty RelStr ;
by A1;
end;

:: deftheorem Def6 defines FTSC1 FINTOPO4:def_6_:_
 for n being Nat st n > 0 holds
FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #);

theorem :: FINTOPO4:20
for n being Element of NAT st n > 0 holds
FTSC1 n is filled
proof
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;
percases ( ( 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;
end;

theorem :: FINTOPO4:21
for n being Element of NAT st n > 0 holds
FTSC1 n is symmetric
proof
let n be Element of NAT ; ::_thesis: ( n > 0 implies FTSC1 n is symmetric )
set f = Nbdc1 n;
assume  n > 0 ; ::_thesis: FTSC1 n is symmetric
then A1: FTSC1 n = RelStr(# (Seg n),(Nbdc1 n) #) by Def6;
let x, y be Element of (FTSC1 n); :: according to FIN_TOPO:def_13 ::_thesis: ( 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 = 1 & i < n implies Im ((Nbdc1 n),i) = {i,n,(i + 1)} ) by A1, Def5;
A4: ( i = 1 & i = n implies Im ((Nbdc1 n),i) = {i} ) by A1, Def5;
A5: i <= n by A1, FINSEQ_1:1;
 y in Seg n by A1;
then reconsider j = y as Element of NAT ;
A6: 1 <= j by A1, FINSEQ_1:1;
A7: ( 1 < i & i = n implies Im ((Nbdc1 n),i) = {i,(i -' 1),1} ) by A1, Def5;
A8: ( 1 < i & i < n implies Im ((Nbdc1 n),i) = {i,(i -' 1),(i + 1)} ) by A1, Def5;
assume A9: y in U_FT x ; ::_thesis: x in U_FT y
A10: j <= n by A1, FINSEQ_1:1;
percases ( ( 1 < i & i < n ) or ( i = 1 & i < n ) or ( 1 < i & i = n ) or ( i = 1 & i = n ) ) by A2, A5, XXREAL_0:1;
supposeA11: ( 1 < i & i < n ) ; ::_thesis: x in U_FT y
A12: now__::_thesis:_(_y_=_i_-'_1_implies_x_in_U_FT_y_)
 i - 1 > 0 by A11, XREAL_1:50;
then A13: i -' 1 = i - 1 by XREAL_0:def_2;
assume A14: y = i -' 1 ; ::_thesis: x in U_FT y
percases ( x = j or x = j -' 1 or x = j + 1 ) by A14, A13;
supposeA15: x = j ; ::_thesis: x in U_FT y
then  Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A11, Def5;
hence  x in U_FT y by A15, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA16: x = j -' 1 ; ::_thesis: x in U_FT y
then A17: i = (i -' 1) -' 1 by A14;
now__::_thesis:_not_i_<>_0
assume  i <> 0 ; ::_thesis: contradiction
then A18: i >= 0 + 1 by NAT_1:13;
then  i - 1 >= 1 - 1 by XREAL_1:9;
then A19: i - 1 = i -' 1 by XREAL_0:def_2;
now__::_thesis:_not_i_=_1
assume A20: i = 1 ; ::_thesis: contradiction
then  (i -' 1) - 1 < 0 by A19;
hence  contradiction by A14, A16, A20, XREAL_0:def_2; ::_thesis: verum
end;
then  i > 1 by A18, XXREAL_0:1;
then  i - 1 > 1 - 1 by XREAL_1:9;
then  i -' 1 >= 0 + 1 by A19, NAT_1:13;
then  (i -' 1) - 1 >= 0 by XREAL_1:48;
then  (i -' 1) -' 1 = (i -' 1) - 1 by XREAL_0:def_2;
hence  contradiction by A17, A19; ::_thesis: verum
end;
hence  x in U_FT y by A11; ::_thesis: verum
end;
supposeA21: x = j + 1 ; ::_thesis: x in U_FT y
then A22: j < n by A5, NAT_1:13;
A23: now__::_thesis:_(_j_<>_1_implies_x_in_U_FT_y_)
assume  j <> 1 ; ::_thesis: x in U_FT y
then  j > 1 by A6, XXREAL_0:1;
then  Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A22, Def5;
hence  x in U_FT y by A21, ENUMSET1:def_1; ::_thesis: verum
end;
now__::_thesis:_(_j_=_1_implies_x_in_U_FT_y_)
assume  j = 1 ; ::_thesis: x in U_FT y
then  Im ( the InternalRel of (FTSC1 n),y) = {j,n,(j + 1)} by A1, A22, Def5;
hence  x in U_FT y by A21, ENUMSET1:def_1; ::_thesis: verum
end;
hence  x in U_FT y by A23; ::_thesis: verum
end;
end;
end;
A24: now__::_thesis:_(_y_=_i_+_1_implies_x_in_U_FT_y_)
assume A25: y = i + 1 ; ::_thesis: x in U_FT y
then A26: j - 1 = x ;
now__::_thesis:_(_(_x_=_j_&_x_in_U_FT_y_)_or_(_x_=_j_-'_1_&_x_in_U_FT_y_)_or_(_x_=_j_+_1_&_contradiction_)_)
percases ( x = j or x = j -' 1 or x = j + 1 ) by A11, A26, XREAL_0:def_2;
caseA27: x = j ; ::_thesis: x in U_FT y
then  Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A11, Def5;
hence  x in U_FT y by A27, ENUMSET1:def_1; ::_thesis: verum
end;
caseA28: x = j -' 1 ; ::_thesis: x in U_FT y
now__::_thesis:_not_j_=_1
assume  j = 1 ; ::_thesis: contradiction
then  j - 1 = 0 ;
hence  contradiction by A11, A28, XREAL_0:def_2; ::_thesis: verum
end;
then A29: j > 1 by A6, XXREAL_0:1;
A30: now__::_thesis:_(_j_<>_n_implies_x_in_U_FT_y_)
assume  j <> n ; ::_thesis: x in U_FT y
then  j < n by A10, XXREAL_0:1;
then  Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A29, Def5;
hence  x in U_FT y by A28, ENUMSET1:def_1; ::_thesis: verum
end;
now__::_thesis:_(_j_=_n_implies_x_in_U_FT_y_)
assume  j = n ; ::_thesis: x in U_FT y
then  Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),1} by A1, A29, Def5;
hence  x in U_FT y by A28, ENUMSET1:def_1; ::_thesis: verum
end;
hence  x in U_FT y by A30; ::_thesis: verum
end;
case x = j + 1 ; ::_thesis: contradiction
hence  contradiction by A25; ::_thesis: verum
end;
end;
end;
hence  x in U_FT y ; ::_thesis: verum
end;
 ( y = i or y = i -' 1 or y = i + 1 ) by A1, A8, A9, A11, ENUMSET1:def_1;
hence  x in U_FT y by A9, A12, A24; ::_thesis: verum
end;
supposeA31: ( i = 1 & i < n ) ; ::_thesis: x in U_FT y
percases ( ( y = i & y <> n ) or y = n or ( y = i + 1 & y <> n ) ) by A1, A3, A9, A31, ENUMSET1:def_1;
suppose ( y = i & y <> n ) ; ::_thesis: x in U_FT y
hence  x in U_FT y by A1, A3, A31, ENUMSET1:def_1; ::_thesis: verum
end;
suppose y = n ; ::_thesis: x in U_FT y
then  Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),1} by A1, A31, Def5;
hence  x in U_FT y by A31, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA32: ( y = i + 1 & y <> n ) ; ::_thesis: x in U_FT y
then  j - 1 = i ;
then A33: j -' 1 = i by XREAL_0:def_2;
 j < n by A10, A32, XXREAL_0:1;
then  Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A31, A32, Def5;
hence  x in U_FT y by A33, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
supposeA34: ( 1 < i & i = n ) ; ::_thesis: x in U_FT y
percases ( ( y = i & y <> 1 ) or y = 1 or ( y = i -' 1 & y <> 1 ) ) by A1, A7, A9, A34, ENUMSET1:def_1;
suppose ( y = i & y <> 1 ) ; ::_thesis: x in U_FT y
hence  x in U_FT y by A1, A7, A34, ENUMSET1:def_1; ::_thesis: verum
end;
suppose y = 1 ; ::_thesis: x in U_FT y
then  Im ( the InternalRel of (FTSC1 n),y) = {j,n,(j + 1)} by A1, A34, Def5;
hence  x in U_FT y by A34, ENUMSET1:def_1; ::_thesis: verum
end;
supposeA35: ( y = i -' 1 & y <> 1 ) ; ::_thesis: x in U_FT y
then A36: 1 < j by A6, XXREAL_0:1;
 n - 1 > 0 by A34, XREAL_1:50;
then A37: n - 1 = n -' 1 by XREAL_0:def_2;
 (n - 1) + 1 = n ;
then  j < n by A34, A35, A37, NAT_1:13;
then  Im ( the InternalRel of (FTSC1 n),y) = {j,(j -' 1),(j + 1)} by A1, A36, Def5;
hence  x in U_FT y by A34, A35, A37, ENUMSET1:def_1; ::_thesis: verum
end;
end;
end;
suppose ( i = 1 & i = n ) ; ::_thesis: x in U_FT y
then  j = i by A1, A4, A9, TARSKI:def_1;
hence  x in U_FT y by A9; ::_thesis: verum
end;
end;
end;