:: FIN_TOPO semantic presentation

begin

theorem Th1: :: FIN_TOPO:1
for A being set
for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j
proof
let A be set ; ::_thesis: for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j
let f be FinSequence of bool A; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) implies for i, j being Element of NAT st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j )
assume A1: for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ; ::_thesis: for i, j being Element of NAT st i <= j & 1 <= i & j <= len f holds
f /. i c= f /. j
let i, j be Element of NAT ; ::_thesis: ( i <= j & 1 <= i & j <= len f implies f /. i c= f /. j )
assume that
A2: i <= j and
A3: 1 <= i and
A4: j <= len f ; ::_thesis: f /. i c= f /. j
consider k being Nat such that
A5: i + k = j by A2, NAT_1:10;
defpred S1[ Element of NAT ] means ( i + $1 <= j implies f /. i c= f /. (i + $1) );
A6: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A7: (i + k) + 1 = i + (k + 1) ;
assume A8: S1[k] ; ::_thesis: S1[k + 1]
thus  S1[k + 1] ::_thesis: verum
proof
 i + k >= i by NAT_1:11;
then A9: i + k >= 1 by A3, XXREAL_0:2;
assume A10: i + (k + 1) <= j ; ::_thesis: f /. i c= f /. (i + (k + 1))
then  i + k < j by A7, NAT_1:13;
then  i + k < len f by A4, XXREAL_0:2;
then  f /. (i + k) c= f /. (i + (k + 1)) by A1, A7, A9;
hence  f /. i c= f /. (i + (k + 1)) by A7, A8, A10, NAT_1:13, XBOOLE_1:1; ::_thesis: verum
end;
end;
A11: S1[ 0 ] ;
A12: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A6);
 k in NAT by ORDINAL1:def_12;
hence  f /. i c= f /. j by A12, A5; ::_thesis: verum
end;

theorem Th2: :: FIN_TOPO:2
for A being set
for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
proof
let A be set ; ::_thesis: for f being FinSequence of bool A st ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) holds
for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
let f be FinSequence of bool A; ::_thesis: ( ( for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ) implies for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k )
assume A1: for i being Element of NAT st 1 <= i & i < len f holds
f /. i c= f /. (i + 1) ; ::_thesis: for i, j being Element of NAT st 1 <= i & j <= len f & f /. j c= f /. i holds
for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
let i, j be Element of NAT ; ::_thesis: ( 1 <= i & j <= len f & f /. j c= f /. i implies for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k )
assume that
A2: 1 <= i and
A3: j <= len f and
A4: f /. j c= f /. i ; ::_thesis: for k being Element of NAT st i <= k & k <= j holds
f /. j = f /. k
let k be Element of NAT ; ::_thesis: ( i <= k & k <= j implies f /. j = f /. k )
assume that
A5: i <= k and
A6: k <= j ; ::_thesis: f /. j = f /. k
 1 <= k by A2, A5, XXREAL_0:2;
then A7: f /. k c= f /. j by A1, A3, A6, Th1;
defpred S1[ Element of NAT ] means ( i + $1 <= j implies f /. j c= f /. (i + $1) );
A8: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; ::_thesis: S1[k + 1]
A10: (i + k) + 1 = i + (k + 1) ;
thus  S1[k + 1] ::_thesis: verum
proof
 i + k >= i by NAT_1:11;
then A11: i + k >= 1 by A2, XXREAL_0:2;
assume A12: i + (k + 1) <= j ; ::_thesis: f /. j c= f /. (i + (k + 1))
then  i + k < j by A10, NAT_1:13;
then  i + k < len f by A3, XXREAL_0:2;
then  f /. (i + k) c= f /. ((i + k) + 1) by A1, A11;
hence  f /. j c= f /. (i + (k + 1)) by A9, A12, NAT_1:13, XBOOLE_1:1; ::_thesis: verum
end;
end;
A13: S1[ 0 ] by A4;
A14: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A8);
consider m being Nat such that
A15: k = i + m by A5, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def_12;
 k = i + m by A15;
then  f /. j c= f /. k by A14, A6;
hence  f /. j = f /. k by A7, XBOOLE_0:def_10; ::_thesis: verum
end;

scheme :: FIN_TOPO:sch 1
MaxFinSeqEx{ F1() ->  non empty set , F2() ->  Subset of F1(), F3() ->  Subset of F1(), F4( Subset of F1()) ->  Subset of F1() } :
 ex f being FinSequence of bool F1() st
( len f > 0 & f /. 1 = F3() & ( for i being Element of NAT st i > 0 & i < len f holds
f /. (i + 1) = F4((f /. i)) ) & F4((f /. (len f))) = f /. (len f) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len f holds
( f /. i c= F2() & f /. i c< f /. j ) ) )
provided
A1: F2() is finite and
A2: F3() c= F2() and
A3: for A being Subset of F1() st A c= F2() holds
( A c= F4(A) & F4(A) c= F2() )
proof
deffunc H1( Nat, Subset of F1()) ->  Subset of F1() = F4($2);
consider f being Function of NAT,(bool F1()) such that
A4: f . 0 = F3() and
A5: for n being Nat holds f . (n + 1) = H1(n,f . n) from NAT_1:sch_12();
defpred S1[ Nat] means f . $1 c= F2();
A6: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; ::_thesis: S1[n + 1]
 f . (n + 1) = F4((f . n)) by A5;
hence  S1[n + 1] by A3, A7; ::_thesis: verum
end;
A8: S1[ 0 ] by A2, A4;
A9: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A6);
A10: for i being Element of NAT holds f . i c= f . (i + 1)
proof
let i be Element of NAT ; ::_thesis: f . i c= f . (i + 1)
 ( f . (i + 1) = F4((f . i)) & f . i c= F2() ) by A5, A9;
hence  f . i c= f . (i + 1) by A3; ::_thesis: verum
end;
A11: dom f = NAT by FUNCT_2:def_1;
A12: rng f is c=-linear
proof
let B, C be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not B in rng f or not C in rng f or B,C are_c=-comparable )
assume  B in rng f ; ::_thesis: ( not C in rng f or B,C are_c=-comparable )
then consider i being set  such that
A13: i in NAT and
A14: B = f . i by A11, FUNCT_1:def_3;
reconsider i = i as Element of NAT by A13;
assume  C in rng f ; ::_thesis: B,C are_c=-comparable
then consider j being set  such that
A15: j in NAT and
A16: C = f . j by A11, FUNCT_1:def_3;
reconsider j = j as Element of NAT by A15;
 ( i <= j or j <= i ) ;
hence  ( B c= C or C c= B ) by A10, A14, A16, MEASURE2:18; :: according to XBOOLE_0:def_9 ::_thesis: verum
end;
A17: rng f c= bool F2()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in bool F2() )
assume  x in rng f ; ::_thesis: x in bool F2()
then  x in f .: NAT by RELSET_1:22;
then  ex k being Element of NAT st
( k in NAT & f . k = x ) by FUNCT_2:65;
then  x c= F2() by A9;
hence  x in bool F2() ; ::_thesis: verum
end;
 rng f <> {} by A4, A11, FUNCT_1:def_3;
then consider m being set  such that
A18: m in rng f and
A19: for C being set st C in rng f holds
C c= m by A1, A17, A12, FINSET_1:12;
deffunc H2( Nat) ->  Element of bool F1() = f . (abs ($1 - 1));
defpred S2[ set ] means ( $1 in NAT & f . $1 = m );
 m in f .: NAT by A18, RELSET_1:22;
then  ex k being Element of NAT st S2[k] by FUNCT_2:65;
then A20: ex k being Nat st S2[k] ;
consider k being Nat such that
A21: S2[k] and
A22: for n being Nat st S2[n] holds
k <= n from NAT_1:sch_5(A20);
consider z being FinSequence of bool F1() such that
A23: len z = k + 1 and
A24: for j being Nat st j in dom z holds
z . j = H2(j) from FINSEQ_2:sch_1();
A25: 0 + 1 <= len z by A23, NAT_1:13;
then A26: 1 in Seg (k + 1) by A23, FINSEQ_1:1;
take  z ; ::_thesis: ( len z > 0 & z /. 1 = F3() & ( for i being Element of NAT st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
thus  0 < len z by A23; ::_thesis: ( z /. 1 = F3() & ( for i being Element of NAT st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
A27: dom z = Seg (k + 1) by A23, FINSEQ_1:def_3;
thus z /. 1 = z . 1 by A25, FINSEQ_4:15
.= f . (abs (1 - 1)) by A24, A27, A26
.= F3() by A4, ABSVALUE:2 ; ::_thesis: ( ( for i being Element of NAT st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ) & F4((z /. (len z))) = z /. (len z) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
thus A28: for i being Element of NAT st i > 0 & i < len z holds
z /. (i + 1) = F4((z /. i)) ::_thesis: ( F4((z /. (len z))) = z /. (len z) & ( for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j ) ) )
proof
let i be Element of NAT ; ::_thesis: ( i > 0 & i < len z implies z /. (i + 1) = F4((z /. i)) )
assume that
A29: i > 0 and
A30: i < len z ; ::_thesis: z /. (i + 1) = F4((z /. i))
A31: ( 0 + 1 < i + 1 & i + 1 <= k + 1 ) by A23, A29, A30, NAT_1:13, XREAL_1:6;
then A32: i + 1 in Seg (k + 1) by FINSEQ_1:1;
A33: 0 + 1 <= i by A29, NAT_1:13;
then  i in Seg (k + 1) by A23, A30, FINSEQ_1:1;
then A34: ( z . i = f . (abs (i - 1)) & i in dom z ) by A24, A27;
 1 - 1 <= i - 1 by A33, XREAL_1:9;
then A35: 0 <= (i - 1) * 1 ;
thus z /. (i + 1) = z . (i + 1) by A23, A31, FINSEQ_4:15
.= f . (abs ((i + 1) - 1)) by A24, A27, A32
.= f . (abs ((i - 1) + 1))
.= f . ((abs (i - 1)) + (abs 1)) by A35, ABSVALUE:11
.= f . ((abs (i - 1)) + 1) by ABSVALUE:def_1
.= F4((f . (abs (i - 1)))) by A5
.= F4((z /. i)) by A34, PARTFUN1:def_6 ; ::_thesis: verum
end;
thus  F4((z /. (len z))) = z /. (len z) ::_thesis: for i, j being Element of NAT st i > 0 & i < j & j <= len z holds
( z /. i c= F2() & z /. i c< z /. j )
proof
 k + 1 in NAT ;
then  k + 1 in dom f by FUNCT_2:def_1;
then  f . (k + 1) in rng f by FUNCT_1:def_3;
then A36: f . (k + 1) c= f . k by A19, A21;
reconsider k9 = k as Element of NAT by ORDINAL1:def_12;
 k in NAT by ORDINAL1:def_12;
then A37: f . k c= f . (k + 1) by A10;
 ( len z = 0 or len z in Seg (len z) ) by FINSEQ_1:3;
then A38: len z in dom z by A23, FINSEQ_1:def_3;
A39: z . (len z) = f . (abs ((k + 1) - 1)) by A23, A24, A27, FINSEQ_1:3
.= f . k by ABSVALUE:def_1 ;
hence F4((z /. (len z))) = F4((f . k9)) by A38, PARTFUN1:def_6
.= f . (k + 1) by A5
.= z . (len z) by A37, A36, A39, XBOOLE_0:def_10
.= z /. (len z) by A38, PARTFUN1:def_6 ;
::_thesis: verum
end;
let i, j be Element of NAT ; ::_thesis: ( i > 0 & i < j & j <= len z implies ( z /. i c= F2() & z /. i c< z /. j ) )
assume that
A40: 0 < i and
A41: i < j and
A42: j <= len z ; ::_thesis: ( z /. i c= F2() & z /. i c< z /. j )
A43: 0 + 1 <= i by A40, NAT_1:13;
then reconsider l = i - 1 as Element of NAT by INT_1:5;
A44: i <= len z by A41, A42, XXREAL_0:2;
then A45: i in Seg (k + 1) by A23, A43, FINSEQ_1:1;
A46: z /. i = z . i by A43, A44, FINSEQ_4:15
.= f . (abs (i - 1)) by A24, A27, A45
.= f . l by ABSVALUE:def_1 ;
hence  z /. i c= F2() by A9; ::_thesis: z /. i c< z /. j
A47: for i being Element of NAT st 1 <= i & i < len z holds
z /. i c= z /. (i + 1)
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len z implies z /. i c= z /. (i + 1) )
assume that
A48: 1 <= i and
A49: i < len z ; ::_thesis: z /. i c= z /. (i + 1)
A50: i in Seg (k + 1) by A23, A48, A49, FINSEQ_1:1;
A51: 1 - 1 <= i - 1 by A48, XREAL_1:9;
then A52: i - 1 is Element of NAT by INT_1:3;
A53: ( 1 <= i + 1 & i + 1 <= len z ) by A48, A49, NAT_1:13;
then A54: i + 1 in Seg (k + 1) by A23, FINSEQ_1:1;
A55: z /. (i + 1) = z . (i + 1) by A53, FINSEQ_4:15
.= f . (abs ((i + 1) - 1)) by A24, A27, A54
.= f . ((i - 1) + 1) by ABSVALUE:def_1 ;
z /. i = z . i by A48, A49, FINSEQ_4:15
.= f . (abs (i - 1)) by A24, A27, A50
.= f . (i - 1) by A51, ABSVALUE:def_1 ;
hence  z /. i c= z /. (i + 1) by A10, A55, A52; ::_thesis: verum
end;
hence  z /. i c= z /. j by A41, A42, A43, Th1; :: according to XBOOLE_0:def_8 ::_thesis: not z /. i = z /. j
defpred S3[ Element of NAT ] means ( i + $1 <= len z implies z /. i = z /. (i + $1) );
A56: ( i <= i + 1 & i + 1 <= j ) by A41, NAT_1:13;
 k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A57: k + 1 in dom z by A23, FINSEQ_1:def_3;
A58: i < len z by A41, A42, XXREAL_0:2;
assume  z /. i = z /. j ; ::_thesis: contradiction
then A59: z /. i = z /. (i + 1) by A42, A43, A47, A56, Th2
.= F4((z /. i)) by A28, A40, A58 ;
A60: now__::_thesis:_for_n_being_Element_of_NAT_st_S3[n]_holds_
S3[n_+_1]
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A61: S3[n] ; ::_thesis: S3[n + 1]
thus  S3[n + 1] ::_thesis: verum
proof
assume  i + (n + 1) <= len z ; ::_thesis: z /. i = z /. (i + (n + 1))
then  (i + n) + 1 <= len z ;
then  i + n < len z by NAT_1:13;
hence z /. i = z /. ((i + n) + 1) by A28, A40, A59, A61
.= z /. (i + (n + 1)) ;
::_thesis: verum
end;
end;
consider n0 being Nat such that
A62: i + n0 = len z by A41, A42, NAT_1:10, XXREAL_0:2;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def_12;
A63: i + n0 = len z by A62;
A64: S3[ 0 ] ;
 for n being Element of NAT holds S3[n] from NAT_1:sch_1(A64, A60);
then f . l = z /. (k + 1) by A23, A46, A63
.= z . (k + 1) by A57, PARTFUN1:def_6
.= f . (abs ((k + 1) - 1)) by A24, A27, FINSEQ_1:4
.= m by A21, ABSVALUE:def_1 ;
then  k <= l by A22;
then  len z <= l + 1 by A23, XREAL_1:6;
hence  contradiction by A41, A42, XXREAL_0:2; ::_thesis: verum
end;

registration
cluster non empty strict for RelStr ;
existence
 ex b1 being RelStr st
( not b1 is empty & b1 is strict )
proof
set D = the non empty set ;
set f = the Relation of the non empty set ;
take  RelStr(# the non empty set , the Relation of the non empty set #) ; ::_thesis: ( not RelStr(# the non empty set , the Relation of the non empty set #) is empty & RelStr(# the non empty set , the Relation of the non empty set #) is strict )
thus  not the carrier of RelStr(# the non empty set , the Relation of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: RelStr(# the non empty set , the Relation of the non empty set #) is strict
thus  RelStr(# the non empty set , the Relation of the non empty set #) is strict ; ::_thesis: verum
end;
end;


definition
let FT be RelStr ;
let x be Element of FT;
func U_FT x ->  Subset of FT equals :: FIN_TOPO:def 1
 Class ( the InternalRel of FT,x);
coherence
 Class ( the InternalRel of FT,x) is Subset of FT ;
end;

:: deftheorem  defines U_FT FIN_TOPO:def_1_:_
 for FT being RelStr
for x being Element of FT holds U_FT x = Class ( the InternalRel of FT,x);

definition
let x be set ;
let y be Subset of {x};
:: original: .-->
redefine funcx .--> y ->  Function of {x},(bool {x});
coherence
 x .--> y is Function of {x},(bool {x})
proof
A1: dom (x .--> y) = {x} by FUNCOP_1:13;
 rng (x .--> y) = {y} by FUNCOP_1:8;
then reconsider R = x .--> y as Relation of {x},(bool {x}) by A1, RELSET_1:4;
 R is quasi_total by A1, FUNCT_2:def_1;
hence  x .--> y is Function of {x},(bool {x}) ; ::_thesis: verum
end;
end;

definition
let x be set ;
func SinglRel x ->  Relation of {x} equals :: FIN_TOPO:def 2
{[x,x]};
coherence
 {[x,x]} is Relation of {x}
proof
 x in {x} by TARSKI:def_1;
hence  {[x,x]} is Relation of {x} by RELSET_1:3; ::_thesis: verum
end;
end;

:: deftheorem  defines SinglRel FIN_TOPO:def_2_:_
 for x being set holds SinglRel x = {[x,x]};

definition
func FT{0}  ->  strict RelStr  equals :: FIN_TOPO:def 3
 RelStr(# {0},(SinglRel 0) #);
coherence
 RelStr(# {0},(SinglRel 0) #) is strict RelStr ;
end;

:: deftheorem  defines FT{0} FIN_TOPO:def_3_:_
 FT{0} = RelStr(# {0},(SinglRel 0) #);

registration
cluster FT{0}  ->  non empty strict ;
coherence
 not FT{0} is empty ;
end;

notation
let IT be non empty RelStr ;
synonym  filled IT for  reflexive ;
end;

definition
let IT be non empty RelStr ;
redefine attr IT is reflexive  means :Def4: :: FIN_TOPO:def 4
 for x being Element of IT holds x in U_FT x;
compatibility
 ( IT is filled iff for x being Element of IT holds x in U_FT x )
proof
thus  ( IT is filled implies for x being Element of IT holds x in U_FT x ) ::_thesis: ( ( for x being Element of IT holds x in U_FT x ) implies IT is filled )
proof
assume A1: IT is filled ; ::_thesis: for x being Element of IT holds x in U_FT x
let x be Element of IT; ::_thesis: x in U_FT x
 x <= x by A1, ORDERS_2:1;
then  [x,x] in the InternalRel of IT by ORDERS_2:def_5;
hence  x in U_FT x by EQREL_1:18; ::_thesis: verum
end;
assume A2: for x being Element of IT holds x in U_FT x ; ::_thesis: IT is filled
let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of IT or [x,x] in the InternalRel of IT )
assume  x in the carrier of IT ; ::_thesis: [x,x] in the InternalRel of IT
then reconsider x = x as Element of IT ;
 x in U_FT x by A2;
hence  [x,x] in the InternalRel of IT by EQREL_1:18; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines filled FIN_TOPO:def_4_:_
 for IT being non empty RelStr holds
( IT is filled iff for x being Element of IT holds x in U_FT x );

theorem Th3: :: FIN_TOPO:3
FT{0} is filled
proof
let x be Element of FT{0}; :: according to FIN_TOPO:def_4 ::_thesis: x in U_FT x
 ( x = 0 & [0,0] in SinglRel 0 ) by TARSKI:def_1;
hence  x in U_FT x by RELAT_1:def_13; ::_thesis: verum
end;

registration
cluster FT{0}  ->  finite strict filled ;
coherence
 ( FT{0} is filled & FT{0} is finite ) by Th3;
end;

registration
cluster non empty finite strict filled for RelStr ;
existence
 ex b1 being non empty RelStr st
( b1 is finite & b1 is filled & b1 is strict ) by Th3;
end;

theorem :: FIN_TOPO:4
for FT being non empty filled RelStr holds  {  (U_FT x) where x is Element of FT : verum  }  is Cover of FT
proof
let FT be non empty filled RelStr ; ::_thesis:  {  (U_FT x) where x is Element of FT : verum  }  is Cover of FT
let a be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not a in the carrier of FT or a in union  {  (U_FT x) where x is Element of FT : verum  }  )
assume  a in the carrier of FT ; ::_thesis: a in union  {  (U_FT x) where x is Element of FT : verum  }
then reconsider b = a as Element of FT ;
 ( b in U_FT b & U_FT b in  {  (U_FT x) where x is Element of FT : verum  }  ) by Def4;
hence  a in union  {  (U_FT x) where x is Element of FT : verum  }  by TARSKI:def_4; ::_thesis: verum
end;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^delta  ->  Subset of FT equals :: FIN_TOPO:def 5
 {  x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` )  }  ;
coherence
  {  x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` )  }  is Subset of FT
proof
defpred S1[ Element of FT] means ( U_FT $1 meets A & U_FT $1 meets A ` );
  {  x where x is Element of FT : S1[x]  }  is Subset of FT from DOMAIN_1:sch_7();
hence   {  x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` )  }  is Subset of FT ; ::_thesis: verum
end;
end;

:: deftheorem  defines ^delta FIN_TOPO:def_5_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^delta =  {  x where x is Element of FT : ( U_FT x meets A & U_FT x meets A ` )  }  ;

theorem Th5: :: FIN_TOPO:5
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )
let A be Subset of FT; ::_thesis: ( x in A ^delta iff ( U_FT x meets A & U_FT x meets A ` ) )
thus  ( x in A ^delta implies ( U_FT x meets A & U_FT x meets A ` ) ) ::_thesis: ( U_FT x meets A & U_FT x meets A ` implies x in A ^delta )
proof
assume  x in A ^delta ; ::_thesis: ( U_FT x meets A & U_FT x meets A ` )
then  ex y being Element of FT st
( y = x & U_FT y meets A & U_FT y meets A ` ) ;
hence  ( U_FT x meets A & U_FT x meets A ` ) ; ::_thesis: verum
end;
assume  ( U_FT x meets A & U_FT x meets A ` ) ; ::_thesis: x in A ^delta
hence  x in A ^delta ; ::_thesis: verum
end;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^deltai  ->  Subset of FT equals :: FIN_TOPO:def 6
A /\ (A ^delta);
coherence
 A /\ (A ^delta) is Subset of FT ;
funcA ^deltao  ->  Subset of FT equals :: FIN_TOPO:def 7
(A `) /\ (A ^delta);
coherence
 (A `) /\ (A ^delta) is Subset of FT ;
end;

:: deftheorem  defines ^deltai FIN_TOPO:def_6_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^deltai = A /\ (A ^delta);

:: deftheorem  defines ^deltao FIN_TOPO:def_7_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^deltao = (A `) /\ (A ^delta);

theorem :: FIN_TOPO:6
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^deltai) \/ (A ^deltao)
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^delta = (A ^deltai) \/ (A ^deltao)
let A be Subset of FT; ::_thesis: A ^delta = (A ^deltai) \/ (A ^deltao)
 for x being set holds
( x in A ^delta iff x in (A ^deltai) \/ (A ^deltao) )
proof
let x be set ; ::_thesis: ( x in A ^delta iff x in (A ^deltai) \/ (A ^deltao) )
thus  ( x in A ^delta implies x in (A ^deltai) \/ (A ^deltao) ) ::_thesis: ( x in (A ^deltai) \/ (A ^deltao) implies x in A ^delta )
proof
assume  x in A ^delta ; ::_thesis: x in (A ^deltai) \/ (A ^deltao)
then  x in ([#] the carrier of FT) /\ (A ^delta) by XBOOLE_1:28;
then  x in (A \/ (A `)) /\ (A ^delta) by SUBSET_1:10;
hence  x in (A ^deltai) \/ (A ^deltao) by XBOOLE_1:23; ::_thesis: verum
end;
assume  x in (A ^deltai) \/ (A ^deltao) ; ::_thesis: x in A ^delta
then  x in (A \/ (A `)) /\ (A ^delta) by XBOOLE_1:23;
then  x in ([#] the carrier of FT) /\ (A ^delta) by SUBSET_1:10;
hence  x in A ^delta by XBOOLE_1:28; ::_thesis: verum
end;
hence  A ^delta = (A ^deltai) \/ (A ^deltao) by TARSKI:1; ::_thesis: verum
end;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^i  ->  Subset of FT equals :: FIN_TOPO:def 8
 {  x where x is Element of FT : U_FT x c= A  }  ;
coherence
  {  x where x is Element of FT : U_FT x c= A  }  is Subset of FT
proof
defpred S1[ Element of FT] means  U_FT $1 c= A;
  {  x where x is Element of FT : S1[x]  }  is Subset of FT from DOMAIN_1:sch_7();
hence   {  x where x is Element of FT : U_FT x c= A  }  is Subset of FT ; ::_thesis: verum
end;
funcA ^b  ->  Subset of FT equals :: FIN_TOPO:def 9
 {  x where x is Element of FT : U_FT x meets A  }  ;
coherence
  {  x where x is Element of FT : U_FT x meets A  }  is Subset of FT
proof
defpred S1[ Element of FT] means  U_FT $1 meets A;
  {  x where x is Element of FT : S1[x]  }  is Subset of FT from DOMAIN_1:sch_7();
hence   {  x where x is Element of FT : U_FT x meets A  }  is Subset of FT ; ::_thesis: verum
end;
funcA ^s  ->  Subset of FT equals :: FIN_TOPO:def 10
 {  x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A )  }  ;
coherence
  {  x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A )  }  is Subset of FT
proof
defpred S1[ Element of FT] means ( $1 in A & (U_FT $1) \ {$1} misses A );
  {  x where x is Element of FT : S1[x]  }  is Subset of FT from DOMAIN_1:sch_7();
hence   {  x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A )  }  is Subset of FT ; ::_thesis: verum
end;
end;

:: deftheorem  defines ^i FIN_TOPO:def_8_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^i =  {  x where x is Element of FT : U_FT x c= A  }  ;

:: deftheorem  defines ^b FIN_TOPO:def_9_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^b =  {  x where x is Element of FT : U_FT x meets A  }  ;

:: deftheorem  defines ^s FIN_TOPO:def_10_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^s =  {  x where x is Element of FT : ( x in A & (U_FT x) \ {x} misses A )  }  ;

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^n  ->  Subset of FT equals :: FIN_TOPO:def 11
A \ (A ^s);
coherence
 A \ (A ^s) is Subset of FT ;
funcA ^f  ->  Subset of FT equals :: FIN_TOPO:def 12
 {  x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y )  }  ;
coherence
  {  x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y )  }  is Subset of FT
proof
defpred S1[ Element of FT] means  ex y being Element of FT st
( y in A & $1 in U_FT y );
  {  x where x is Element of FT : S1[x]  }  is Subset of FT from DOMAIN_1:sch_7();
hence   {  x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y )  }  is Subset of FT ; ::_thesis: verum
end;
end;

:: deftheorem  defines ^n FIN_TOPO:def_11_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^n = A \ (A ^s);

:: deftheorem  defines ^f FIN_TOPO:def_12_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^f =  {  x where x is Element of FT : ex y being Element of FT st
( y in A & x in U_FT y )  }  ;

definition
let IT be non empty RelStr ;
attrIT is symmetric  means :Def13: :: FIN_TOPO:def 13
 for x, y being Element of IT st y in U_FT x holds
x in U_FT y;
end;

:: deftheorem Def13 defines symmetric FIN_TOPO:def_13_:_
 for IT being non empty RelStr holds
( IT is symmetric iff for x, y being Element of IT st y in U_FT x holds
x in U_FT y );

theorem Th7: :: FIN_TOPO:7
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff U_FT x c= A )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff U_FT x c= A )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^i iff U_FT x c= A )
let A be Subset of FT; ::_thesis: ( x in A ^i iff U_FT x c= A )
thus  ( x in A ^i implies U_FT x c= A ) ::_thesis: ( U_FT x c= A implies x in A ^i )
proof
assume  x in A ^i ; ::_thesis: U_FT x c= A
then  ex y being Element of FT st
( y = x & U_FT y c= A ) ;
hence  U_FT x c= A ; ::_thesis: verum
end;
assume  U_FT x c= A ; ::_thesis: x in A ^i
hence  x in A ^i ; ::_thesis: verum
end;

theorem Th8: :: FIN_TOPO:8
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^b iff U_FT x meets A )
let A be Subset of FT; ::_thesis: ( x in A ^b iff U_FT x meets A )
thus  ( x in A ^b implies U_FT x meets A ) ::_thesis: ( U_FT x meets A implies x in A ^b )
proof
assume  x in A ^b ; ::_thesis: U_FT x meets A
then  ex y being Element of FT st
( y = x & U_FT y meets A ) ;
hence  U_FT x meets A ; ::_thesis: verum
end;
assume  U_FT x meets A ; ::_thesis: x in A ^b
hence  x in A ^b ; ::_thesis: verum
end;

theorem Th9: :: FIN_TOPO:9
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )
let A be Subset of FT; ::_thesis: ( x in A ^s iff ( x in A & (U_FT x) \ {x} misses A ) )
thus  ( x in A ^s implies ( x in A & (U_FT x) \ {x} misses A ) ) ::_thesis: ( x in A & (U_FT x) \ {x} misses A implies x in A ^s )
proof
assume  x in A ^s ; ::_thesis: ( x in A & (U_FT x) \ {x} misses A )
then  ex y being Element of FT st
( y = x & y in A & (U_FT y) \ {y} misses A ) ;
hence  ( x in A & (U_FT x) \ {x} misses A ) ; ::_thesis: verum
end;
assume  ( x in A & (U_FT x) \ {x} misses A ) ; ::_thesis: x in A ^s
hence  x in A ^s ; ::_thesis: verum
end;

theorem :: FIN_TOPO:10
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
let A be Subset of FT; ::_thesis: ( x in A ^n iff ( x in A & (U_FT x) \ {x} meets A ) )
thus  ( x in A ^n implies ( x in A & (U_FT x) \ {x} meets A ) ) ::_thesis: ( x in A & (U_FT x) \ {x} meets A implies x in A ^n )
proof
assume  x in A ^n ; ::_thesis: ( x in A & (U_FT x) \ {x} meets A )
then  ( x in A & not x in A ^s ) by XBOOLE_0:def_5;
hence  ( x in A & (U_FT x) \ {x} meets A ) ; ::_thesis: verum
end;
assume that
A1: x in A and
A2: (U_FT x) \ {x} meets A ; ::_thesis: x in A ^n
 not x in A ^s by A2, Th9;
hence  x in A ^n by A1, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th11: :: FIN_TOPO:11
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )
let x be Element of FT; ::_thesis: for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )
let A be Subset of FT; ::_thesis: ( x in A ^f iff ex y being Element of FT st
( y in A & x in U_FT y ) )
thus  ( x in A ^f implies ex y being Element of FT st
( y in A & x in U_FT y ) ) ::_thesis: ( ex y being Element of FT st
( y in A & x in U_FT y ) implies x in A ^f )
proof
assume  x in A ^f ; ::_thesis: ex y being Element of FT st
( y in A & x in U_FT y )
then  ex y being Element of FT st
( y = x & ex z being Element of FT st
( z in A & y in U_FT z ) ) ;
hence  ex y being Element of FT st
( y in A & x in U_FT y ) ; ::_thesis: verum
end;
assume  ex z being Element of FT st
( z in A & x in U_FT z ) ; ::_thesis: x in A ^f
hence  x in A ^f ; ::_thesis: verum
end;

theorem :: FIN_TOPO:12
for FT being non empty RelStr holds
( FT is symmetric iff for A being Subset of FT holds A ^b = A ^f )
proof
let FT be non empty RelStr ; ::_thesis: ( FT is symmetric iff for A being Subset of FT holds A ^b = A ^f )
thus  ( FT is symmetric implies for A being Subset of FT holds A ^b = A ^f ) ::_thesis: ( ( for A being Subset of FT holds A ^b = A ^f ) implies FT is symmetric )
proof
assume A1: FT is symmetric ; ::_thesis: for A being Subset of FT holds A ^b = A ^f
let A be Subset of FT; ::_thesis: A ^b = A ^f
thus  A ^b c= A ^f :: according to XBOOLE_0:def_10 ::_thesis: A ^f c= A ^b
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^b or x in A ^f )
assume A2: x in A ^b ; ::_thesis: x in A ^f
then reconsider y = x as Element of FT ;
 U_FT y meets A by A2, Th8;
then consider z being set  such that
A3: z in (U_FT y) /\ A by XBOOLE_0:4;
reconsider z = z as Element of FT by A3;
 z in U_FT y by A3, XBOOLE_0:def_4;
then A4: y in U_FT z by A1, Def13;
 z in A by A3, XBOOLE_0:def_4;
hence  x in A ^f by A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^f or x in A ^b )
assume A5: x in A ^f ; ::_thesis: x in A ^b
then reconsider y = x as Element of FT ;
consider z being Element of FT such that
A6: z in A and
A7: y in U_FT z by A5, Th11;
 z in U_FT y by A1, A7, Def13;
then  U_FT y meets A by A6, XBOOLE_0:3;
hence  x in A ^b ; ::_thesis: verum
end;
assume A8: for A being Subset of FT holds A ^b = A ^f ; ::_thesis: FT is symmetric
let x, y be Element of FT; :: according to FIN_TOPO:def_13 ::_thesis: ( y in U_FT x implies x in U_FT y )
assume  y in U_FT x ; ::_thesis: x in U_FT y
then  U_FT x meets {y} by ZFMISC_1:48;
then  x in {y} ^b ;
then  x in {y} ^f by A8;
then  ex z being Element of FT st
( z in {y} & x in U_FT z ) by Th11;
hence  x in U_FT y by TARSKI:def_1; ::_thesis: verum
end;

definition
let FT be non empty RelStr ;
let IT be Subset of FT;
attrIT is open  means :Def14: :: FIN_TOPO:def 14
IT = IT ^i ;
attrIT is closed  means :Def15: :: FIN_TOPO:def 15
IT = IT ^b ;
attrIT is connected  means :Def16: :: FIN_TOPO:def 16
 for B, C being Subset of FT st IT = B \/ C & B <> {} & C <> {} & B misses C holds
B ^b meets C;
end;

:: deftheorem Def14 defines open FIN_TOPO:def_14_:_
 for FT being non empty RelStr
for IT being Subset of FT holds
( IT is open iff IT = IT ^i );

:: deftheorem Def15 defines closed FIN_TOPO:def_15_:_
 for FT being non empty RelStr
for IT being Subset of FT holds
( IT is closed iff IT = IT ^b );

:: deftheorem Def16 defines connected FIN_TOPO:def_16_:_
 for FT being non empty RelStr
for IT being Subset of FT holds
( IT is connected iff for B, C being Subset of FT st IT = B \/ C & B <> {} & C <> {} & B misses C holds
B ^b meets C );

definition
let FT be non empty RelStr ;
let A be Subset of FT;
funcA ^fb  ->  Subset of FT equals :: FIN_TOPO:def 17
 meet  {  F where F is Subset of FT : ( A c= F & F is closed )  }  ;
coherence
 meet  {  F where F is Subset of FT : ( A c= F & F is closed )  }  is Subset of FT
proof
set FF =  {  F where F is Subset of FT : ( A c= F & F is closed )  }  ;
  {  F where F is Subset of FT : ( A c= F & F is closed )  }  c= bool the carrier of FT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F where F is Subset of FT : ( A c= F & F is closed )  }  or x in bool the carrier of FT )
assume  x in  {  F where F is Subset of FT : ( A c= F & F is closed )  }  ; ::_thesis: x in bool the carrier of FT
then  ex F being Subset of FT st
( x = F & A c= F & F is closed ) ;
hence  x in bool the carrier of FT ; ::_thesis: verum
end;
then reconsider FF =  {  F where F is Subset of FT : ( A c= F & F is closed )  }  as Subset-Family of FT ;
 meet FF is Subset of FT ;
hence  meet  {  F where F is Subset of FT : ( A c= F & F is closed )  }  is Subset of FT ; ::_thesis: verum
end;
funcA ^fi  ->  Subset of FT equals :: FIN_TOPO:def 18
 union  {  F where F is Subset of FT : ( A c= F & F is open )  }  ;
coherence
 union  {  F where F is Subset of FT : ( A c= F & F is open )  }  is Subset of FT
proof
set FF =  {  F where F is Subset of FT : ( A c= F & F is open )  }  ;
  {  F where F is Subset of FT : ( A c= F & F is open )  }  c= bool the carrier of FT
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F where F is Subset of FT : ( A c= F & F is open )  }  or x in bool the carrier of FT )
assume  x in  {  F where F is Subset of FT : ( A c= F & F is open )  }  ; ::_thesis: x in bool the carrier of FT
then  ex F being Subset of FT st
( x = F & A c= F & F is open ) ;
hence  x in bool the carrier of FT ; ::_thesis: verum
end;
then reconsider FF =  {  F where F is Subset of FT : ( A c= F & F is open )  }  as Subset-Family of FT ;
 union FF is Subset of FT ;
hence  union  {  F where F is Subset of FT : ( A c= F & F is open )  }  is Subset of FT ; ::_thesis: verum
end;
end;

:: deftheorem  defines ^fb FIN_TOPO:def_17_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^fb = meet  {  F where F is Subset of FT : ( A c= F & F is closed )  }  ;

:: deftheorem  defines ^fi FIN_TOPO:def_18_:_
 for FT being non empty RelStr
for A being Subset of FT holds A ^fi = union  {  F where F is Subset of FT : ( A c= F & F is open )  }  ;

theorem Th13: :: FIN_TOPO:13
for FT being non empty filled RelStr
for A being Subset of FT holds A c= A ^b
proof
let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT holds A c= A ^b
let A be Subset of FT; ::_thesis: A c= A ^b
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A ^b )
assume A1: x in A ; ::_thesis: x in A ^b
then reconsider y = x as Element of FT ;
 y in U_FT y by Def4;
then  U_FT y meets A by A1, XBOOLE_0:3;
hence  x in A ^b ; ::_thesis: verum
end;

theorem Th14: :: FIN_TOPO:14
for FT being non empty RelStr
for A, B being Subset of FT st A c= B holds
A ^b c= B ^b
proof
let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st A c= B holds
A ^b c= B ^b
let A, B be Subset of FT; ::_thesis: ( A c= B implies A ^b c= B ^b )
assume A1: A c= B ; ::_thesis: A ^b c= B ^b
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^b or x in B ^b )
assume A2: x in A ^b ; ::_thesis: x in B ^b
then reconsider y = x as Element of FT ;
 U_FT y meets A by A2, Th8;
then  ex w being set st
( w in U_FT y & w in A ) by XBOOLE_0:3;
then  U_FT y meets B by A1, XBOOLE_0:3;
hence  x in B ^b ; ::_thesis: verum
end;

theorem :: FIN_TOPO:15
for FT being non empty finite filled RelStr
for A being Subset of FT holds
( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )
proof
let FT be non empty finite filled RelStr ; ::_thesis: for A being Subset of FT holds
( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )
let A be Subset of FT; ::_thesis: ( A is connected iff for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )
thus  ( A is connected implies for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) ) ::_thesis: ( ( for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) ) implies A is connected )
proof
deffunc H1( Subset of FT) ->  Element of K32( the carrier of FT) = ($1 ^b) /\ A;
assume A1: A is connected ; ::_thesis: for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
let x be Element of FT; ::_thesis: ( x in A implies ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) )
assume  x in A ; ::_thesis: ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
then A2: {x} c= A by ZFMISC_1:31;
A3: for B being Subset of FT st B c= A holds
( B c= H1(B) & H1(B) c= A )
proof
let B be Subset of FT; ::_thesis: ( B c= A implies ( B c= H1(B) & H1(B) c= A ) )
assume A4: B c= A ; ::_thesis: ( B c= H1(B) & H1(B) c= A )
 B c= B ^b by Th13;
hence  B c= (B ^b) /\ A by A4, XBOOLE_1:19; ::_thesis: H1(B) c= A
thus  H1(B) c= A by XBOOLE_1:17; ::_thesis: verum
end;
A5: A is finite ;
consider S being FinSequence of bool the carrier of FT such that
A6: len S > 0 and
A7: S /. 1 = {x} and
A8: for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = H1(S /. i) and
A9: H1(S /. (len S)) = S /. (len S) and
A10: for i, j being Element of NAT st i > 0 & i < j & j <= len S holds
( S /. i c= A & S /. i c< S /. j ) from FIN_TOPO:sch_1(A5, A2, A3);
consider k being Nat such that
A11: len S = k + 1 by A6, NAT_1:6;
set B = S /. (len S);
set C = A \ (S /. (len S));
A12: S /. (len S) misses A \ (S /. (len S)) by XBOOLE_1:79;
defpred S1[ Element of NAT ] means ( $1 < len S implies S /. ($1 + 1) <> {} );
A13: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A14: S1[i] ; ::_thesis: S1[i + 1]
thus  S1[i + 1] ::_thesis: verum
proof
assume A15: i + 1 < len S ; ::_thesis: S /. ((i + 1) + 1) <> {}
then  ( i + 1 < (i + 1) + 1 & (i + 1) + 1 <= len S ) by NAT_1:13;
then  S /. (i + 1) c< S /. ((i + 1) + 1) by A10;
then  S /. (i + 1) c= S /. ((i + 1) + 1) by XBOOLE_0:def_8;
hence  S /. ((i + 1) + 1) <> {} by A14, A15, NAT_1:13; ::_thesis: verum
end;
end;
A16: S1[ 0 ] by A7;
A17: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A16, A13);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 k < len S by A11, NAT_1:13;
then A18: S /. (len S) <> {} by A17, A11;
take  S ; ::_thesis: ( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
thus  len S > 0 by A6; ::_thesis: ( S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
thus  S /. 1 = {x} by A7; ::_thesis: ( ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) )
thus  for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A by A8; ::_thesis: A c= S /. (len S)
assume  not A c= S /. (len S) ; ::_thesis: contradiction
then A19: A \ (S /. (len S)) <> {} by XBOOLE_1:37;
((S /. (len S)) ^b) /\ (A \ (S /. (len S))) = ((S /. (len S)) ^b) /\ (A /\ (A \ (S /. (len S)))) by XBOOLE_1:28, XBOOLE_1:36
.= (S /. (len S)) /\ (A \ (S /. (len S))) by A9, XBOOLE_1:16
.= {} by A12, XBOOLE_0:def_7 ;
then A20: ( S /. (len S) misses A \ (S /. (len S)) & (S /. (len S)) ^b misses A \ (S /. (len S)) ) by XBOOLE_0:def_7, XBOOLE_1:79;
(S /. (len S)) \/ (A \ (S /. (len S))) = (S /. (len S)) \/ A by XBOOLE_1:39
.= A by A9, XBOOLE_1:12, XBOOLE_1:17 ;
hence  contradiction by A1, A19, A18, A20, Def16; ::_thesis: verum
end;
assume A21: for x being Element of FT st x in A holds
ex S being FinSequence of bool the carrier of FT st
( len S > 0 & S /. 1 = {x} & ( for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A ) & A c= S /. (len S) ) ; ::_thesis: A is connected
given B, C being Subset of FT such that A22: A = B \/ C and
A23: B <> {} and
A24: C <> {} and
A25: B misses C and
A26: B ^b misses C ; :: according to FIN_TOPO:def_16 ::_thesis: contradiction
set x = the Element of B;
 the Element of B in A by A22, A23, XBOOLE_0:def_3;
then consider S being FinSequence of bool the carrier of FT such that
A27: len S > 0 and
A28: S /. 1 = { the Element of B} and
A29: for i being Element of NAT st i > 0 & i < len S holds
S /. (i + 1) = ((S /. i) ^b) /\ A and
A30: A c= S /. (len S) by A21;
consider k being Nat such that
A31: len S = k + 1 by A27, NAT_1:6;
defpred S1[ Element of NAT ] means ( $1 < len S implies S /. ($1 + 1) c= B );
 (B ^b) /\ C = {} by A26, XBOOLE_0:def_7;
then A32: (B ^b) /\ A = ((B ^b) /\ B) \/ {} by A22, XBOOLE_1:23
.= B by Th13, XBOOLE_1:28 ;
A33: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A34: S1[i] ; ::_thesis: S1[i + 1]
thus  S1[i + 1] ::_thesis: verum
proof
assume A35: i + 1 < len S ; ::_thesis: S /. ((i + 1) + 1) c= B
then  (S /. (i + 1)) ^b c= B ^b by A34, Th14, NAT_1:13;
then  ((S /. (i + 1)) ^b) /\ A c= (B ^b) /\ A by XBOOLE_1:26;
hence  S /. ((i + 1) + 1) c= B by A32, A29, A35; ::_thesis: verum
end;
end;
A36: S1[ 0 ] by A23, A28, ZFMISC_1:31;
A37: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A36, A33);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 k < len S by A31, NAT_1:13;
then A38: S /. (len S) c= B by A37, A31;
A39: B c= A by A22, XBOOLE_1:7;
then  S /. (len S) c= A by A38, XBOOLE_1:1;
then  S /. (len S) = A by A30, XBOOLE_0:def_10;
then A40: A = B by A39, A38, XBOOLE_0:def_10;
 B /\ C = {} by A25, XBOOLE_0:def_7;
hence  contradiction by A22, A24, A40, XBOOLE_1:7, XBOOLE_1:28; ::_thesis: verum
end;

theorem Th16: :: FIN_TOPO:16
for FT being non empty RelStr
for A being Subset of FT holds ((A `) ^i) ` = A ^b
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds ((A `) ^i) ` = A ^b
let A be Subset of FT; ::_thesis: ((A `) ^i) ` = A ^b
 for x being set holds
( x in ((A `) ^i) ` iff x in A ^b )
proof
let x be set ; ::_thesis: ( x in ((A `) ^i) ` iff x in A ^b )
thus  ( x in ((A `) ^i) ` implies x in A ^b ) ::_thesis: ( x in A ^b implies x in ((A `) ^i) ` )
proof
assume A1: x in ((A `) ^i) ` ; ::_thesis: x in A ^b
then reconsider y = x as Element of FT ;
 not y in (A `) ^i by A1, XBOOLE_0:def_5;
then  not U_FT y c= A ` ;
then consider z being set  such that
A2: z in U_FT y and
A3: not z in A ` by TARSKI:def_3;
 z in A by A2, A3, SUBSET_1:29;
then  U_FT y meets A by A2, XBOOLE_0:3;
hence  x in A ^b ; ::_thesis: verum
end;
assume A4: x in A ^b ; ::_thesis: x in ((A `) ^i) `
then reconsider y = x as Element of FT ;
 U_FT y meets A by A4, Th8;
then  ex z being set st
( z in U_FT y & z in A ) by XBOOLE_0:3;
then  not U_FT y c= A ` by XBOOLE_0:def_5;
then  not y in (A `) ^i by Th7;
hence  x in ((A `) ^i) ` by SUBSET_1:29; ::_thesis: verum
end;
hence  ((A `) ^i) ` = A ^b by TARSKI:1; ::_thesis: verum
end;

theorem Th17: :: FIN_TOPO:17
for FT being non empty RelStr
for A being Subset of FT holds ((A `) ^b) ` = A ^i
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds ((A `) ^b) ` = A ^i
let A be Subset of FT; ::_thesis: ((A `) ^b) ` = A ^i
 for x being set holds
( x in ((A `) ^b) ` iff x in A ^i )
proof
let x be set ; ::_thesis: ( x in ((A `) ^b) ` iff x in A ^i )
thus  ( x in ((A `) ^b) ` implies x in A ^i ) ::_thesis: ( x in A ^i implies x in ((A `) ^b) ` )
proof
assume A1: x in ((A `) ^b) ` ; ::_thesis: x in A ^i
then reconsider y = x as Element of FT ;
 not y in (A `) ^b by A1, XBOOLE_0:def_5;
then  U_FT y misses A ` ;
then  (U_FT y) /\ (A `) = {} by XBOOLE_0:def_7;
then  (U_FT y) \ A = {} by SUBSET_1:13;
then  U_FT y c= A by XBOOLE_1:37;
hence  x in A ^i ; ::_thesis: verum
end;
assume A2: x in A ^i ; ::_thesis: x in ((A `) ^b) `
then reconsider y = x as Element of FT ;
 U_FT y c= A by A2, Th7;
then  (U_FT y) \ A = {} by XBOOLE_1:37;
then  (U_FT y) /\ (A `) = {} by SUBSET_1:13;
then  U_FT y misses A ` by XBOOLE_0:def_7;
then  not y in (A `) ^b by Th8;
hence  x in ((A `) ^b) ` by SUBSET_1:29; ::_thesis: verum
end;
hence  ((A `) ^b) ` = A ^i by TARSKI:1; ::_thesis: verum
end;

theorem :: FIN_TOPO:18
for FT being non empty RelStr
for A being Subset of FT holds A ^delta = (A ^b) /\ ((A `) ^b)
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^delta = (A ^b) /\ ((A `) ^b)
let A be Subset of FT; ::_thesis: A ^delta = (A ^b) /\ ((A `) ^b)
 for x being set holds
( x in A ^delta iff x in (A ^b) /\ ((A `) ^b) )
proof
let x be set ; ::_thesis: ( x in A ^delta iff x in (A ^b) /\ ((A `) ^b) )
thus  ( x in A ^delta implies x in (A ^b) /\ ((A `) ^b) ) ::_thesis: ( x in (A ^b) /\ ((A `) ^b) implies x in A ^delta )
proof
assume A1: x in A ^delta ; ::_thesis: x in (A ^b) /\ ((A `) ^b)
then reconsider y = x as Element of FT ;
 U_FT y meets A ` by A1, Th5;
then A2: x in (A `) ^b ;
 U_FT y meets A by A1, Th5;
then  x in A ^b ;
hence  x in (A ^b) /\ ((A `) ^b) by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A3: x in (A ^b) /\ ((A `) ^b) ; ::_thesis: x in A ^delta
then reconsider y = x as Element of FT ;
 x in (A `) ^b by A3, XBOOLE_0:def_4;
then A4: U_FT y meets A ` by Th8;
 x in A ^b by A3, XBOOLE_0:def_4;
then  U_FT y meets A by Th8;
hence  x in A ^delta by A4; ::_thesis: verum
end;
hence  A ^delta = (A ^b) /\ ((A `) ^b) by TARSKI:1; ::_thesis: verum
end;

theorem :: FIN_TOPO:19
for FT being non empty RelStr
for A being Subset of FT holds (A `) ^delta = A ^delta
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds (A `) ^delta = A ^delta
let A be Subset of FT; ::_thesis: (A `) ^delta = A ^delta
 for x being set holds
( x in (A `) ^delta iff x in A ^delta )
proof
let x be set ; ::_thesis: ( x in (A `) ^delta iff x in A ^delta )
thus  ( x in (A `) ^delta implies x in A ^delta ) ::_thesis: ( x in A ^delta implies x in (A `) ^delta )
proof
assume A1: x in (A `) ^delta ; ::_thesis: x in A ^delta
then reconsider y = x as Element of FT ;
 ( U_FT y meets A ` & U_FT y meets (A `) ` ) by A1, Th5;
hence  x in A ^delta ; ::_thesis: verum
end;
assume A2: x in A ^delta ; ::_thesis: x in (A `) ^delta
then reconsider y = x as Element of FT ;
 ( U_FT y meets (A `) ` & U_FT y meets A ` ) by A2, Th5;
hence  x in (A `) ^delta ; ::_thesis: verum
end;
hence  (A `) ^delta = A ^delta by TARSKI:1; ::_thesis: verum
end;

theorem :: FIN_TOPO:20
for FT being non empty RelStr
for x being Element of FT
for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b
proof
let FT be non empty RelStr ; ::_thesis: for x being Element of FT
for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b
let x be Element of FT; ::_thesis: for A being Subset of FT st x in A ^s holds
not x in (A \ {x}) ^b
let A be Subset of FT; ::_thesis: ( x in A ^s implies not x in (A \ {x}) ^b )
assume  x in A ^s ; ::_thesis: not x in (A \ {x}) ^b
then  A misses (U_FT x) \ {x} by Th9;
then  A /\ ((U_FT x) \ {x}) = {} by XBOOLE_0:def_7;
then A1: (A /\ (U_FT x)) \ {x} = {} by XBOOLE_1:49;
now__::_thesis:_A_\_{x}_misses_U_FT_x
percases ( A /\ (U_FT x) = {} or A /\ (U_FT x) = {x} ) by A1, ZFMISC_1:58;
suppose A /\ (U_FT x) = {} ; ::_thesis: A \ {x} misses U_FT x
then  A misses U_FT x by XBOOLE_0:def_7;
hence  A \ {x} misses U_FT x by XBOOLE_1:36, XBOOLE_1:63; ::_thesis: verum
end;
suppose A /\ (U_FT x) = {x} ; ::_thesis: A \ {x} misses U_FT x
then  ((U_FT x) /\ A) \ {x} = {} by XBOOLE_1:37;
then  (U_FT x) /\ (A \ {x}) = {} by XBOOLE_1:49;
hence  A \ {x} misses U_FT x by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence  not x in (A \ {x}) ^b by Th8; ::_thesis: verum
end;

theorem :: FIN_TOPO:21
for FT being non empty RelStr
for A being Subset of FT st A ^s <> {} & card A <> 1 holds
not A is connected
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A ^s <> {} & card A <> 1 holds
not A is connected
let A be Subset of FT; ::_thesis: ( A ^s <> {} & card A <> 1 implies not A is connected )
assume that
A1: A ^s <> {} and
A2: card A <> 1 ; ::_thesis: not A is connected
consider z being Element of FT such that
A3: z in A ^s by A1, SUBSET_1:4;
set C = {z};
set B = A \ {z};
 ( card {z} = 1 & A <> {} ) by A3, Th9, CARD_1:30;
then A4: A \ {z} <> {} by A2, ZFMISC_1:58;
 z in A by A3, Th9;
then  {z} is Subset of A by SUBSET_1:41;
then A5: A = (A \ {z}) \/ {z} by XBOOLE_1:45;
A6: (U_FT z) \ {z} misses A by A3, Th9;
A7: (A \ {z}) ^b misses {z}
proof
assume  (A \ {z}) ^b meets {z} ; ::_thesis: contradiction
then consider x being set  such that
A8: x in (A \ {z}) ^b and
A9: x in {z} by XBOOLE_0:3;
reconsider x = x as Element of FT by A8;
A10: x = z by A9, TARSKI:def_1;
 U_FT x meets A \ {z} by A8, Th8;
then consider y being set  such that
A11: y in U_FT x and
A12: y in A \ {z} by XBOOLE_0:3;
 not x in A \ {z} by A9, XBOOLE_0:def_5;
then  y in (U_FT x) \ {x} by A11, A12, ZFMISC_1:56;
then  (U_FT z) \ {z} meets A \ {z} by A12, A10, XBOOLE_0:3;
then A13: ex w being set st w in ((U_FT z) \ {z}) /\ (A \ {z}) by XBOOLE_0:4;
 ((U_FT z) \ {z}) /\ (A \ {z}) c= ((U_FT z) \ {z}) /\ A by XBOOLE_1:26, XBOOLE_1:36;
hence  contradiction by A6, A13, XBOOLE_0:4; ::_thesis: verum
end;
 A \ {z} misses {z} by XBOOLE_1:79;
hence  not A is connected by A5, A4, A7, Def16; ::_thesis: verum
end;

theorem :: FIN_TOPO:22
for FT being non empty filled RelStr
for A being Subset of FT holds A ^i c= A
proof
let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT holds A ^i c= A
let A be Subset of FT; ::_thesis: A ^i c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^i or x in A )
assume A1: x in A ^i ; ::_thesis: x in A
then reconsider y = x as Element of FT ;
A2: y in U_FT y by Def4;
 U_FT y c= A by A1, Th7;
hence  x in A by A2; ::_thesis: verum
end;

theorem :: FIN_TOPO:23
for FT being non empty RelStr
for A being Subset of FT st A is open holds
A ` is closed
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A is open holds
A ` is closed
let A be Subset of FT; ::_thesis: ( A is open implies A ` is closed )
assume  A is open ; ::_thesis: A ` is closed
then A1: A = A ^i by Def14;
 A ^i = ((A `) ^b) ` by Th17;
hence  A ` is closed by A1, Def15; ::_thesis: verum
end;

theorem :: FIN_TOPO:24
for FT being non empty RelStr
for A being Subset of FT st A is closed holds
A ` is open
proof
let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A is closed holds
A ` is open
let A be Subset of FT; ::_thesis: ( A is closed implies A ` is open )
assume  A is closed ; ::_thesis: A ` is open
then A1: A = A ^b by Def15;
 A ^b = ((A `) ^i) ` by Th16;
hence  A ` is open by A1, Def14; ::_thesis: verum
end;