:: 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;