:: FINTOPO6 semantic presentation begin registration let FT be non empty RelStr ; cluster empty -> connected for Element of K32( the carrier of FT); coherence for b1 being Subset of FT st b1 is empty holds b1 is connected proof let S be Subset of FT; ::_thesis: ( S is empty implies S is connected ) assume A1: S is empty ; ::_thesis: S is connected let B, C be Subset of FT; :: according to FIN_TOPO:def_16 ::_thesis: ( not S = B \/ C or B = {} or C = {} or not B misses C or not B ^b misses C ) assume that A2: ( S = B \/ C & B <> {} ) and C <> {} and B misses C ; ::_thesis: not B ^b misses C thus not B ^b misses C by A1, A2; ::_thesis: verum end; end; theorem Th1: :: FINTOPO6:1 for FT being non empty RelStr for A, B being Subset of FT holds (A \/ B) ^b = (A ^b) \/ (B ^b) proof let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT holds (A \/ B) ^b = (A ^b) \/ (B ^b) let A, B be Subset of FT; ::_thesis: (A \/ B) ^b = (A ^b) \/ (B ^b) A1: (A \/ B) ^b c= (A ^b) \/ (B ^b) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A \/ B) ^b or x in (A ^b) \/ (B ^b) ) assume x in (A \/ B) ^b ; ::_thesis: x in (A ^b) \/ (B ^b) then consider y being Element of FT such that A2: x = y and A3: U_FT y meets A \/ B ; ( U_FT y meets A or U_FT y meets B ) by A3, XBOOLE_1:70; then ( x in { u where u is Element of FT : U_FT u meets A } or x in B ^b ) by A2; hence x in (A ^b) \/ (B ^b) by XBOOLE_0:def_3; ::_thesis: verum end; ( A ^b c= (A \/ B) ^b & B ^b c= (A \/ B) ^b ) by FIN_TOPO:14, XBOOLE_1:7; then (A ^b) \/ (B ^b) c= (A \/ B) ^b by XBOOLE_1:8; hence (A \/ B) ^b = (A ^b) \/ (B ^b) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th2: :: FINTOPO6:2 for FT being non empty RelStr holds ({} FT) ^b = {} proof let FT be non empty RelStr ; ::_thesis: ({} FT) ^b = {} assume not ({} FT) ^b = {} ; ::_thesis: contradiction then consider x being set such that A1: x in ({} FT) ^b by XBOOLE_0:def_1; ex y being Element of FT st ( x = y & U_FT y meets {} FT ) by A1; hence contradiction by XBOOLE_1:65; ::_thesis: verum end; registration let FT be non empty RelStr ; cluster({} FT) ^b -> empty ; coherence ({} FT) ^b is empty by Th2; end; theorem Th3: :: FINTOPO6:3 for FT being non empty RelStr for A being Subset of FT st ( for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds ( B ^b meets C & B meets C ^b ) ) holds A is connected proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st ( for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds ( B ^b meets C & B meets C ^b ) ) holds A is connected let A be Subset of FT; ::_thesis: ( ( for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds ( B ^b meets C & B meets C ^b ) ) implies A is connected ) assume for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds ( B ^b meets C & B meets C ^b ) ; ::_thesis: A is connected then for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds B ^b meets C ; hence A is connected by FIN_TOPO:def_16; ::_thesis: verum end; definition let FT be non empty RelStr ; attrFT is connected means :Def1: :: FINTOPO6:def 1 [#] FT is connected ; end; :: deftheorem Def1 defines connected FINTOPO6:def_1_:_ for FT being non empty RelStr holds ( FT is connected iff [#] FT is connected ); theorem Th4: :: FINTOPO6:4 for FT being non empty RelStr for A being Subset of FT st A is connected holds for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A is connected holds for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT let A be Subset of FT; ::_thesis: ( A is connected implies for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT ) assume A1: A is connected ; ::_thesis: for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT let A2, B2 be Subset of FT; ::_thesis: ( A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT implies B2 = {} FT ) assume that A2: ( A = A2 \/ B2 & A2 misses B2 ) and A3: A2,B2 are_separated ; ::_thesis: ( A2 = {} FT or B2 = {} FT ) A2 ^b misses B2 by A3, FINTOPO4:def_1; hence ( A2 = {} FT or B2 = {} FT ) by A1, A2, FIN_TOPO:def_16; ::_thesis: verum end; theorem Th5: :: FINTOPO6:5 for FT being non empty RelStr st FT is connected holds for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds B = {} FT proof let FT be non empty RelStr ; ::_thesis: ( FT is connected implies for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds B = {} FT ) assume FT is connected ; ::_thesis: for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds B = {} FT then A1: [#] FT is connected by Def1; let A, B be Subset of FT; ::_thesis: ( [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT implies B = {} FT ) assume that A2: ( [#] FT = A \/ B & A misses B ) and A3: A,B are_separated ; ::_thesis: ( A = {} FT or B = {} FT ) A ^b misses B by A3, FINTOPO4:def_1; hence ( A = {} FT or B = {} FT ) by A1, A2, FIN_TOPO:def_16; ::_thesis: verum end; theorem Th6: :: FINTOPO6:6 for FT being non empty RelStr for A, B being Subset of FT st FT is symmetric & A ^b misses B holds A misses B ^b proof let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric & A ^b misses B holds A misses B ^b let A, B be Subset of FT; ::_thesis: ( FT is symmetric & A ^b misses B implies A misses B ^b ) assume that A1: FT is symmetric and A2: A ^b misses B ; ::_thesis: A misses B ^b assume A meets B ^b ; ::_thesis: contradiction then consider x being set such that A3: x in A and A4: x in B ^b by XBOOLE_0:3; consider y being Element of FT such that A5: x = y and A6: U_FT y meets B by A4; consider z being set such that A7: z in U_FT y and A8: z in B by A6, XBOOLE_0:3; reconsider z2 = z as Element of FT by A7; y in U_FT z2 by A1, A7, FIN_TOPO:def_13; then U_FT z2 meets A by A3, A5, XBOOLE_0:3; then A9: z in A ^b ; (A ^b) /\ B = {} by A2, XBOOLE_0:def_7; hence contradiction by A8, A9, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th7: :: FINTOPO6:7 for FT being non empty RelStr for A being Subset of FT st FT is symmetric & ( for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT ) holds A is connected proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is symmetric & ( for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT ) holds A is connected let A be Subset of FT; ::_thesis: ( FT is symmetric & ( for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT ) implies A is connected ) assume A1: FT is symmetric ; ::_thesis: ( ex A2, B2 being Subset of FT st ( A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT & not B2 = {} FT ) or A is connected ) assume A2: for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds B2 = {} FT ; ::_thesis: A is connected for B, C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses C holds ( B ^b meets C & B meets C ^b ) proof let B, C be Subset of FT; ::_thesis: ( A = B \/ C & B <> {} & C <> {} & B misses C implies ( B ^b meets C & B meets C ^b ) ) assume ( A = B \/ C & B <> {} & C <> {} & B misses C ) ; ::_thesis: ( B ^b meets C & B meets C ^b ) then not B,C are_separated by A2; then ( not B ^b misses C or not B misses C ^b ) by FINTOPO4:def_1; hence ( B ^b meets C & B meets C ^b ) by A1, Th6; ::_thesis: verum end; hence A is connected by Th3; ::_thesis: verum end; definition let T be RelStr ; mode SubSpace of T -> RelStr means :Def2: :: FINTOPO6:def 2 ( the carrier of it c= the carrier of T & ( for x being Element of it st x in the carrier of it holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of it ) ); existence ex b1 being RelStr st ( the carrier of b1 c= the carrier of T & ( for x being Element of b1 st x in the carrier of b1 holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b1 ) ) proof for x being Element of T st x in the carrier of T holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of T by XBOOLE_1:28; hence ex b1 being RelStr st ( the carrier of b1 c= the carrier of T & ( for x being Element of b1 st x in the carrier of b1 holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b1 ) ) ; ::_thesis: verum end; end; :: deftheorem Def2 defines SubSpace FINTOPO6:def_2_:_ for T, b2 being RelStr holds ( b2 is SubSpace of T iff ( the carrier of b2 c= the carrier of T & ( for x being Element of b2 st x in the carrier of b2 holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of b2 ) ) ); Lm1: for T being RelStr holds RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T proof let T be RelStr ; ::_thesis: RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T set S = RelStr(# the carrier of T, the InternalRel of T #); for x being Element of RelStr(# the carrier of T, the InternalRel of T #) st x in the carrier of RelStr(# the carrier of T, the InternalRel of T #) holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of T by XBOOLE_1:28; hence RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T by Def2; ::_thesis: verum end; registration let T be RelStr ; cluster strict for SubSpace of T; existence ex b1 being SubSpace of T st b1 is strict proof RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T by Lm1; hence ex b1 being SubSpace of T st b1 is strict ; ::_thesis: verum end; end; registration let T be non empty RelStr ; cluster non empty strict for SubSpace of T; existence ex b1 being SubSpace of T st ( b1 is strict & not b1 is empty ) proof ( RelStr(# the carrier of T, the InternalRel of T #) is SubSpace of T & not RelStr(# the carrier of T, the InternalRel of T #) is empty ) by Lm1; hence ex b1 being SubSpace of T st ( b1 is strict & not b1 is empty ) ; ::_thesis: verum end; end; definition let T be non empty RelStr ; let P be non empty Subset of T; funcT | P -> non empty strict SubSpace of T means :Def3: :: FINTOPO6:def 3 [#] it = P; existence ex b1 being non empty strict SubSpace of T st [#] b1 = P proof deffunc H1( set ) -> Element of K32( the carrier of T) = (Im ( the InternalRel of T,$1)) /\ P; A1: for x being Element of T st x in P holds H1(x) c= P by XBOOLE_1:17; consider G being Relation of P such that A2: for y being Element of T st y in P holds Im (G,y) = H1(y) from RELSET_1:sch_3(A1); set FS = RelStr(# P,G #); for x being Element of RelStr(# P,G #) st x in the carrier of RelStr(# P,G #) holds U_FT x = (Im ( the InternalRel of T,x)) /\ the carrier of RelStr(# P,G #) by A2; then ( [#] RelStr(# P,G #) = the carrier of RelStr(# P,G #) & RelStr(# P,G #) is non empty strict SubSpace of T ) by Def2; hence ex b1 being non empty strict SubSpace of T st [#] b1 = P ; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict SubSpace of T st [#] b1 = P & [#] b2 = P holds b1 = b2 proof let Z1, Z2 be non empty strict SubSpace of T; ::_thesis: ( [#] Z1 = P & [#] Z2 = P implies Z1 = Z2 ) assume that A3: [#] Z1 = P and A4: [#] Z2 = P ; ::_thesis: Z1 = Z2 reconsider R1 = the InternalRel of Z1, R2 = the InternalRel of Z2 as Relation of P by A3, A4; for z being set st z in P holds Im (R1,z) = Im (R2,z) proof let z be set ; ::_thesis: ( z in P implies Im (R1,z) = Im (R2,z) ) assume A5: z in P ; ::_thesis: Im (R1,z) = Im (R2,z) then reconsider z1 = z as Element of Z1 by A3; reconsider z2 = z as Element of Z2 by A4, A5; thus Im (R1,z) = U_FT z1 .= (Im ( the InternalRel of T,z1)) /\ the carrier of Z1 by Def2 .= U_FT z2 by A3, A4, Def2 .= Im (R2,z) ; ::_thesis: verum end; hence Z1 = Z2 by A3, A4, RELSET_1:31; ::_thesis: verum end; end; :: deftheorem Def3 defines | FINTOPO6:def_3_:_ for T being non empty RelStr for P being non empty Subset of T for b3 being non empty strict SubSpace of T holds ( b3 = T | P iff [#] b3 = P ); theorem Th8: :: FINTOPO6:8 for FT being non empty RelStr for X being non empty SubSpace of FT st FT is filled holds X is filled proof let FT be non empty RelStr ; ::_thesis: for X being non empty SubSpace of FT st FT is filled holds X is filled let X be non empty SubSpace of FT; ::_thesis: ( FT is filled implies X is filled ) assume A1: FT is filled ; ::_thesis: X is filled let x be Element of X; :: according to FIN_TOPO:def_4 ::_thesis: x in U_FT x the carrier of X c= the carrier of FT by Def2; then reconsider x2 = x as Element of FT by TARSKI:def_3; A2: U_FT x = (U_FT x2) /\ ([#] X) by Def2; x2 in U_FT x2 by A1, FIN_TOPO:def_4; hence x in U_FT x by A2, XBOOLE_0:def_4; ::_thesis: verum end; registration let FT be non empty filled RelStr ; cluster non empty -> non empty filled for SubSpace of FT; coherence for b1 being non empty SubSpace of FT holds b1 is filled by Th8; end; theorem :: FINTOPO6:9 for FT being non empty RelStr for X being non empty SubSpace of FT st FT is symmetric holds X is symmetric proof let FT be non empty RelStr ; ::_thesis: for X being non empty SubSpace of FT st FT is symmetric holds X is symmetric let X be non empty SubSpace of FT; ::_thesis: ( FT is symmetric implies X is symmetric ) assume A1: FT is symmetric ; ::_thesis: X is symmetric for x, y being Element of X st y in U_FT x holds x in U_FT y proof let x, y be Element of X; ::_thesis: ( y in U_FT x implies x in U_FT y ) assume A2: y in U_FT x ; ::_thesis: x in U_FT y the carrier of X c= the carrier of FT by Def2; then reconsider x2 = x, y2 = y as Element of FT by TARSKI:def_3; A3: ( U_FT x = (U_FT x2) /\ ([#] X) & U_FT y = (U_FT y2) /\ ([#] X) ) by Def2; ( y2 in U_FT x2 implies x2 in U_FT y2 ) by A1, FIN_TOPO:def_13; hence x in U_FT y by A2, A3, XBOOLE_0:def_4; ::_thesis: verum end; hence X is symmetric by FIN_TOPO:def_13; ::_thesis: verum end; theorem Th10: :: FINTOPO6:10 for FT being non empty RelStr for X9 being SubSpace of FT for A being Subset of X9 holds A is Subset of FT proof let FT be non empty RelStr ; ::_thesis: for X9 being SubSpace of FT for A being Subset of X9 holds A is Subset of FT let X9 be SubSpace of FT; ::_thesis: for A being Subset of X9 holds A is Subset of FT let A be Subset of X9; ::_thesis: A is Subset of FT the carrier of X9 c= the carrier of FT by Def2; hence A is Subset of FT by XBOOLE_1:1; ::_thesis: verum end; theorem :: FINTOPO6:11 for FT being non empty RelStr for P being Subset of FT holds ( P is closed iff P ` is open ) proof let FT be non empty RelStr ; ::_thesis: for P being Subset of FT holds ( P is closed iff P ` is open ) let P be Subset of FT; ::_thesis: ( P is closed iff P ` is open ) ( P ` is open implies (P `) ` is closed ) by FIN_TOPO:23; hence ( P is closed iff P ` is open ) by FIN_TOPO:24; ::_thesis: verum end; theorem :: FINTOPO6:12 for FT being non empty RelStr for A being Subset of FT holds ( A is open iff ( ( for z being Element of FT st U_FT z c= A holds z in A ) & ( for x being Element of FT st x in A holds U_FT x c= A ) ) ) proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds ( A is open iff ( ( for z being Element of FT st U_FT z c= A holds z in A ) & ( for x being Element of FT st x in A holds U_FT x c= A ) ) ) let A be Subset of FT; ::_thesis: ( A is open iff ( ( for z being Element of FT st U_FT z c= A holds z in A ) & ( for x being Element of FT st x in A holds U_FT x c= A ) ) ) hereby ::_thesis: ( ( for z being Element of FT st U_FT z c= A holds z in A ) & ( for x being Element of FT st x in A holds U_FT x c= A ) implies A is open ) assume A is open ; ::_thesis: ( ( for z being Element of FT st U_FT z c= A holds z in A ) & ( for x being Element of FT st x in A holds U_FT x c= A ) ) then A1: A = A ^i by FIN_TOPO:def_14; hence for z being Element of FT st U_FT z c= A holds z in A ; ::_thesis: for x being Element of FT st x in A holds U_FT x c= A for x being Element of FT st x in A holds U_FT x c= A proof let x be Element of FT; ::_thesis: ( x in A implies U_FT x c= A ) assume x in A ; ::_thesis: U_FT x c= A then ex y being Element of FT st ( x = y & U_FT y c= A ) by A1; hence U_FT x c= A ; ::_thesis: verum end; hence for x being Element of FT st x in A holds U_FT x c= A ; ::_thesis: verum end; assume that A2: for z being Element of FT st U_FT z c= A holds z in A and A3: for x being Element of FT st x in A holds U_FT x c= A ; ::_thesis: A is open A4: A c= { y where y is Element of FT : U_FT y c= A } proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in A or u in { y where y is Element of FT : U_FT y c= A } ) assume A5: u in A ; ::_thesis: u in { y where y is Element of FT : U_FT y c= A } then reconsider y2 = u as Element of FT ; U_FT y2 c= A by A3, A5; hence u in { y where y is Element of FT : U_FT y c= A } ; ::_thesis: verum end; { y where y is Element of FT : U_FT y c= A } c= A proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { y where y is Element of FT : U_FT y c= A } or u in A ) assume u in { y where y is Element of FT : U_FT y c= A } ; ::_thesis: u in A then ex y being Element of FT st ( y = u & U_FT y c= A ) ; hence u in A by A2; ::_thesis: verum end; then A = A ^i by A4, XBOOLE_0:def_10; hence A is open by FIN_TOPO:def_14; ::_thesis: verum end; theorem Th13: :: FINTOPO6:13 for FT being non empty RelStr for X9 being non empty SubSpace of FT for A being Subset of FT for A1 being Subset of X9 st A = A1 holds A1 ^b = (A ^b) /\ ([#] X9) proof let FT be non empty RelStr ; ::_thesis: for X9 being non empty SubSpace of FT for A being Subset of FT for A1 being Subset of X9 st A = A1 holds A1 ^b = (A ^b) /\ ([#] X9) let X9 be non empty SubSpace of FT; ::_thesis: for A being Subset of FT for A1 being Subset of X9 st A = A1 holds A1 ^b = (A ^b) /\ ([#] X9) let A be Subset of FT; ::_thesis: for A1 being Subset of X9 st A = A1 holds A1 ^b = (A ^b) /\ ([#] X9) let A1 be Subset of X9; ::_thesis: ( A = A1 implies A1 ^b = (A ^b) /\ ([#] X9) ) assume A1: A = A1 ; ::_thesis: A1 ^b = (A ^b) /\ ([#] X9) A2: (A ^b) /\ ([#] X9) c= A1 ^b proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in (A ^b) /\ ([#] X9) or u in A1 ^b ) assume A3: u in (A ^b) /\ ([#] X9) ; ::_thesis: u in A1 ^b then u in A ^b by XBOOLE_0:def_4; then consider y2 being Element of FT such that A4: u = y2 and A5: U_FT y2 meets A ; reconsider y3 = y2 as Element of X9 by A3, A4; consider z being set such that A6: z in U_FT y2 and A7: z in A by A5, XBOOLE_0:3; U_FT y3 = (U_FT y2) /\ ([#] X9) by Def2; then z in U_FT y3 by A1, A6, A7, XBOOLE_0:def_4; then U_FT y3 meets A1 by A1, A7, XBOOLE_0:3; hence u in A1 ^b by A4; ::_thesis: verum end; A1 ^b c= (A ^b) /\ ([#] X9) proof reconsider Y = X9 as non empty RelStr ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A1 ^b or x in (A ^b) /\ ([#] X9) ) assume x in A1 ^b ; ::_thesis: x in (A ^b) /\ ([#] X9) then consider y being Element of Y such that A8: y = x and A9: U_FT y meets A1 ; ( y in the carrier of X9 & the carrier of Y c= the carrier of FT ) by Def2; then reconsider z = y as Element of FT ; U_FT y = (Im ( the InternalRel of FT,y)) /\ the carrier of X9 by Def2; then U_FT z meets A by A1, A9, XBOOLE_1:74; then z in { u where u is Element of FT : U_FT u meets A } ; hence x in (A ^b) /\ ([#] X9) by A8, XBOOLE_0:def_4; ::_thesis: verum end; hence A1 ^b = (A ^b) /\ ([#] X9) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: FINTOPO6:14 for FT being non empty RelStr for X9 being non empty SubSpace of FT for P1, Q1 being Subset of FT for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds P1,Q1 are_separated proof let FT be non empty RelStr ; ::_thesis: for X9 being non empty SubSpace of FT for P1, Q1 being Subset of FT for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds P1,Q1 are_separated let X9 be non empty SubSpace of FT; ::_thesis: for P1, Q1 being Subset of FT for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds P1,Q1 are_separated let P1, Q1 be Subset of FT; ::_thesis: for P, Q being Subset of X9 st P = P1 & Q = Q1 & P,Q are_separated holds P1,Q1 are_separated let P, Q be Subset of X9; ::_thesis: ( P = P1 & Q = Q1 & P,Q are_separated implies P1,Q1 are_separated ) assume A1: ( P = P1 & Q = Q1 ) ; ::_thesis: ( not P,Q are_separated or P1,Q1 are_separated ) reconsider P2 = P, Q2 = Q as Subset of FT by Th10; assume A2: P,Q are_separated ; ::_thesis: P1,Q1 are_separated then P ^b misses Q by FINTOPO4:def_1; then A3: (P ^b) /\ Q = {} by XBOOLE_0:def_7; P misses Q ^b by A2, FINTOPO4:def_1; then A4: P /\ (Q ^b) = {} by XBOOLE_0:def_7; P /\ (Q ^b) = P /\ (([#] X9) /\ (Q2 ^b)) by Th13 .= (P /\ ([#] X9)) /\ (Q2 ^b) by XBOOLE_1:16 .= P2 /\ (Q2 ^b) by XBOOLE_1:28 ; then A5: P2 misses Q2 ^b by A4, XBOOLE_0:def_7; (P ^b) /\ Q = ((P2 ^b) /\ ([#] X9)) /\ Q by Th13 .= (P2 ^b) /\ (Q /\ ([#] X9)) by XBOOLE_1:16 .= (P2 ^b) /\ Q2 by XBOOLE_1:28 ; then P2 ^b misses Q2 by A3, XBOOLE_0:def_7; hence P1,Q1 are_separated by A1, A5, FINTOPO4:def_1; ::_thesis: verum end; theorem :: FINTOPO6:15 for FT being non empty RelStr for X9 being non empty SubSpace of FT for P, Q being Subset of FT for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds P1,Q1 are_separated proof let FT be non empty RelStr ; ::_thesis: for X9 being non empty SubSpace of FT for P, Q being Subset of FT for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds P1,Q1 are_separated let X9 be non empty SubSpace of FT; ::_thesis: for P, Q being Subset of FT for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds P1,Q1 are_separated let P, Q be Subset of FT; ::_thesis: for P1, Q1 being Subset of X9 st P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated holds P1,Q1 are_separated let P1, Q1 be Subset of X9; ::_thesis: ( P = P1 & Q = Q1 & P \/ Q c= [#] X9 & P,Q are_separated implies P1,Q1 are_separated ) assume that A1: ( P = P1 & Q = Q1 ) and A2: P \/ Q c= [#] X9 ; ::_thesis: ( not P,Q are_separated or P1,Q1 are_separated ) ( P c= P \/ Q & Q c= P \/ Q ) by XBOOLE_1:7; then reconsider P2 = P, Q2 = Q as Subset of X9 by A2, XBOOLE_1:1; assume A3: P,Q are_separated ; ::_thesis: P1,Q1 are_separated then P misses Q ^b by FINTOPO4:def_1; then A4: P /\ (Q ^b) = {} by XBOOLE_0:def_7; P2 /\ (Q2 ^b) = P2 /\ (([#] X9) /\ (Q ^b)) by Th13 .= (P2 /\ ([#] X9)) /\ (Q ^b) by XBOOLE_1:16 .= P /\ (Q ^b) by XBOOLE_1:28 ; then A5: P2 misses Q2 ^b by A4, XBOOLE_0:def_7; P2 ^b = (P ^b) /\ ([#] X9) by Th13; then A6: (P2 ^b) /\ Q2 = (P ^b) /\ (Q2 /\ ([#] X9)) by XBOOLE_1:16 .= (P ^b) /\ Q by XBOOLE_1:28 ; P ^b misses Q by A3, FINTOPO4:def_1; then (P ^b) /\ Q = {} by XBOOLE_0:def_7; then P2 ^b misses Q2 by A6, XBOOLE_0:def_7; hence P1,Q1 are_separated by A1, A5, FINTOPO4:def_1; ::_thesis: verum end; theorem Th16: :: FINTOPO6:16 for FT being non empty RelStr for A being non empty Subset of FT holds ( A is connected iff FT | A is connected ) proof let FT be non empty RelStr ; ::_thesis: for A being non empty Subset of FT holds ( A is connected iff FT | A is connected ) let A be non empty Subset of FT; ::_thesis: ( A is connected iff FT | A is connected ) A1: [#] (FT | A) = A by Def3; thus ( A is connected implies FT | A is connected ) ::_thesis: ( FT | A is connected implies A is connected ) proof assume A2: A is connected ; ::_thesis: FT | A is connected for B2, C2 being Subset of (FT | A) st [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 holds B2 ^b meets C2 proof let B2, C2 be Subset of (FT | A); ::_thesis: ( [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 implies B2 ^b meets C2 ) A3: ([#] (FT | A)) /\ C2 = C2 by XBOOLE_1:28; the carrier of (FT | A) = [#] (FT | A) .= A by Def3 ; then reconsider B3 = B2, C3 = C2 as Subset of FT by XBOOLE_1:1; assume ( [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 ) ; ::_thesis: B2 ^b meets C2 then A4: B3 ^b meets C3 by A1, A2, FIN_TOPO:def_16; (B2 ^b) /\ C2 = ((B3 ^b) /\ ([#] (FT | A))) /\ C2 by Th13 .= (B3 ^b) /\ C3 by A3, XBOOLE_1:16 ; then (B2 ^b) /\ C2 <> {} by A4, XBOOLE_0:def_7; hence B2 ^b meets C2 by XBOOLE_0:def_7; ::_thesis: verum end; then [#] (FT | A) is connected by FIN_TOPO:def_16; hence FT | A is connected by Def1; ::_thesis: verum end; assume FT | A is connected ; ::_thesis: A is connected then A5: [#] (FT | A) is connected by Def1; let B, C be Subset of FT; :: according to FIN_TOPO:def_16 ::_thesis: ( not A = B \/ C or B = {} or C = {} or not B misses C or not B ^b misses C ) assume that A6: A = B \/ C and A7: ( B <> {} & C <> {} & B misses C ) ; ::_thesis: not B ^b misses C A8: [#] (FT | A) = A by Def3; then reconsider B2 = B as Subset of (FT | A) by A6, XBOOLE_1:7; reconsider C2 = C as Subset of (FT | A) by A6, A8, XBOOLE_1:7; ( ([#] (FT | A)) /\ C2 = C2 & B2 ^b = (B ^b) /\ ([#] (FT | A)) ) by Th13, XBOOLE_1:28; then A9: (B ^b) /\ C = (B2 ^b) /\ C2 by XBOOLE_1:16; B2 ^b meets C2 by A5, A6, A7, A8, FIN_TOPO:def_16; hence (B ^b) /\ C <> {} by A9, XBOOLE_0:def_7; :: according to XBOOLE_0:def_7 ::_thesis: verum end; theorem :: FINTOPO6:17 for FT being non empty filled RelStr for A being non empty Subset of FT st FT is symmetric holds ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds Q = {} FT ) proof let FT be non empty filled RelStr ; ::_thesis: for A being non empty Subset of FT st FT is symmetric holds ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds Q = {} FT ) let A be non empty Subset of FT; ::_thesis: ( FT is symmetric implies ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds Q = {} FT ) ) assume A1: FT is symmetric ; ::_thesis: ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds Q = {} FT ) now__::_thesis:_(_not_A_is_connected_implies_ex_P1,_Q1_being_Subset_of_FT_st_ (_A_=_P1_\/_Q1_&_P1_misses_Q1_&_P1,Q1_are_separated_&_P1_<>_{}_FT_&_Q1_<>_{}_FT_)_) assume not A is connected ; ::_thesis: ex P1, Q1 being Subset of FT st ( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT ) then not FT | A is connected by Th16; then not [#] (FT | A) is connected by Def1; then consider P, Q being Subset of (FT | A) such that A2: [#] (FT | A) = P \/ Q and A3: ( P <> {} & Q <> {} ) and A4: P misses Q and A5: P ^b misses Q by FIN_TOPO:def_16; reconsider P1 = P, Q1 = Q as Subset of FT by Th10; take P1 = P1; ::_thesis: ex Q1 being Subset of FT st ( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT ) take Q1 = Q1; ::_thesis: ( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT ) thus ( A = P1 \/ Q1 & P1 misses Q1 ) by A2, A4, Def3; ::_thesis: ( P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT ) A6: P ^b = (P1 ^b) /\ ([#] (FT | A)) by Th13; ([#] (FT | A)) /\ Q1 = Q1 by XBOOLE_1:28; then (P1 ^b) /\ Q1 = ((P1 ^b) /\ ([#] (FT | A))) /\ Q by XBOOLE_1:16 .= {} by A5, A6, XBOOLE_0:def_7 ; then P1 ^b misses Q1 by XBOOLE_0:def_7; hence ( P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT ) by A1, A3, FINTOPO4:10; ::_thesis: verum end; hence ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds Q = {} FT ) by Th4; ::_thesis: verum end; theorem :: FINTOPO6:18 for FT being non empty RelStr for A being Subset of FT st FT is filled & FT is connected & A <> {} & A ` <> {} holds A ^delta <> {} proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is filled & FT is connected & A <> {} & A ` <> {} holds A ^delta <> {} let A be Subset of FT; ::_thesis: ( FT is filled & FT is connected & A <> {} & A ` <> {} implies A ^delta <> {} ) assume that A1: ( FT is filled & FT is connected ) and A2: ( A <> {} & A ` <> {} ) ; ::_thesis: A ^delta <> {} A3: now__::_thesis:_(_A_^b_meets_A_`_implies_ex_z_being_Element_of_FT_st_ (_U_FT_z_meets_A_&_U_FT_z_meets_A_`_)_) assume A ^b meets A ` ; ::_thesis: ex z being Element of FT st ( U_FT z meets A & U_FT z meets A ` ) then consider x being set such that A4: x in A ^b and A5: x in A ` by XBOOLE_0:3; reconsider x = x as Element of FT by A4; x in U_FT x by A1, FIN_TOPO:def_4; then A6: U_FT x meets A ` by A5, XBOOLE_0:3; U_FT x meets A by A4, FIN_TOPO:8; hence ex z being Element of FT st ( U_FT z meets A & U_FT z meets A ` ) by A6; ::_thesis: verum end; A7: now__::_thesis:_(_A_meets_(A_`)_^b_implies_ex_z_being_Element_of_FT_st_ (_U_FT_z_meets_A_&_U_FT_z_meets_A_`_)_) assume A meets (A `) ^b ; ::_thesis: ex z being Element of FT st ( U_FT z meets A & U_FT z meets A ` ) then consider x being set such that A8: x in (A `) ^b and A9: x in A by XBOOLE_0:3; reconsider x = x as Element of FT by A8; x in U_FT x by A1, FIN_TOPO:def_4; then A10: U_FT x meets A by A9, XBOOLE_0:3; U_FT x meets A ` by A8, FIN_TOPO:8; hence ex z being Element of FT st ( U_FT z meets A & U_FT z meets A ` ) by A10; ::_thesis: verum end; ( {} = {} FT & A \/ (A `) = [#] FT ) by XBOOLE_1:45; then not A,A ` are_separated by A1, A2, Th5, XBOOLE_1:79; hence A ^delta <> {} by A3, A7, FINTOPO4:def_1, FIN_TOPO:5; ::_thesis: verum end; theorem :: FINTOPO6:19 for FT being non empty RelStr for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds A ^deltai <> {} proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds A ^deltai <> {} let A be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} implies A ^deltai <> {} ) assume that A1: ( FT is filled & FT is symmetric ) and A2: ( FT is connected & A <> {} & A ` <> {} ) ; ::_thesis: A ^deltai <> {} A3: now__::_thesis:_(_A_^b_meets_A_`_implies_A_^deltai_<>_{}_) assume A ^b meets A ` ; ::_thesis: A ^deltai <> {} then consider x being set such that A4: x in A ^b and A5: x in A ` by XBOOLE_0:3; reconsider x = x as Element of FT by A4; U_FT x meets A by A4, FIN_TOPO:8; then consider y being set such that A6: y in U_FT x and A7: y in A by XBOOLE_0:3; reconsider y = y as Element of FT by A6; y in U_FT y by A1, FIN_TOPO:def_4; then A8: U_FT y meets A by A7, XBOOLE_0:3; x in U_FT y by A1, A6, FIN_TOPO:def_13; then U_FT y meets A ` by A5, XBOOLE_0:3; then y in A ^delta by A8; hence A ^deltai <> {} by A7, XBOOLE_0:def_4; ::_thesis: verum end; A9: now__::_thesis:_(_A_meets_(A_`)_^b_implies_A_^deltai_<>_{}_) assume A meets (A `) ^b ; ::_thesis: A ^deltai <> {} then consider x being set such that A10: x in (A `) ^b and A11: x in A by XBOOLE_0:3; reconsider x = x as Element of FT by A10; x in U_FT x by A1, FIN_TOPO:def_4; then A12: U_FT x meets A by A11, XBOOLE_0:3; U_FT x meets A ` by A10, FIN_TOPO:8; then x in A ^delta by A12; hence A ^deltai <> {} by A11, XBOOLE_0:def_4; ::_thesis: verum end; ( {} = {} FT & A \/ (A `) = [#] FT ) by XBOOLE_1:45; then not A,A ` are_separated by A2, Th5, XBOOLE_1:79; hence A ^deltai <> {} by A3, A9, FINTOPO4:def_1; ::_thesis: verum end; theorem :: FINTOPO6:20 for FT being non empty RelStr for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds A ^deltao <> {} proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} holds A ^deltao <> {} let A be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & FT is connected & A <> {} & A ` <> {} implies A ^deltao <> {} ) assume that A1: ( FT is filled & FT is symmetric ) and A2: ( FT is connected & A <> {} & A ` <> {} ) ; ::_thesis: A ^deltao <> {} A3: now__::_thesis:_(_A_meets_(A_`)_^b_implies_A_^deltao_<>_{}_) assume A meets (A `) ^b ; ::_thesis: A ^deltao <> {} then consider x being set such that A4: x in (A `) ^b and A5: x in A by XBOOLE_0:3; reconsider x = x as Element of FT by A4; U_FT x meets A ` by A4, FIN_TOPO:8; then consider y being set such that A6: y in U_FT x and A7: y in A ` by XBOOLE_0:3; reconsider y = y as Element of FT by A6; y in U_FT y by A1, FIN_TOPO:def_4; then A8: U_FT y meets A ` by A7, XBOOLE_0:3; x in U_FT y by A1, A6, FIN_TOPO:def_13; then U_FT y meets A by A5, XBOOLE_0:3; then y in A ^delta by A8; hence A ^deltao <> {} by A7, XBOOLE_0:def_4; ::_thesis: verum end; A9: now__::_thesis:_(_A_^b_meets_A_`_implies_A_^deltao_<>_{}_) assume A ^b meets A ` ; ::_thesis: A ^deltao <> {} then consider x being set such that A10: x in A ^b and A11: x in A ` by XBOOLE_0:3; reconsider x = x as Element of FT by A10; x in U_FT x by A1, FIN_TOPO:def_4; then A12: U_FT x meets A ` by A11, XBOOLE_0:3; U_FT x meets A by A10, FIN_TOPO:8; then x in A ^delta by A12; hence A ^deltao <> {} by A11, XBOOLE_0:def_4; ::_thesis: verum end; ( {} = {} FT & A \/ (A `) = [#] FT ) by XBOOLE_1:45; then not A,A ` are_separated by A2, Th5, XBOOLE_1:79; hence A ^deltao <> {} by A9, A3, FINTOPO4:def_1; ::_thesis: verum end; theorem :: FINTOPO6:21 for FT being non empty RelStr for A being Subset of FT holds A ^deltai misses A ^deltao proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^deltai misses A ^deltao let A be Subset of FT; ::_thesis: A ^deltai misses A ^deltao A misses A ` by XBOOLE_1:79; then A1: A /\ (A `) = {} by XBOOLE_0:def_7; thus (A ^deltai) /\ (A ^deltao) = (A /\ ((A ^delta) /\ (A `))) /\ (A ^delta) by XBOOLE_1:16 .= ((A /\ (A `)) /\ (A ^delta)) /\ (A ^delta) by XBOOLE_1:16 .= {} by A1 ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; theorem :: FINTOPO6:22 for FT being non empty filled RelStr for A being Subset of FT holds A ^deltao = (A ^b) \ A proof let FT be non empty filled RelStr ; ::_thesis: for A being Subset of FT holds A ^deltao = (A ^b) \ A let A be Subset of FT; ::_thesis: A ^deltao = (A ^b) \ A A1: (A `) /\ ((A `) ^b) = A ` by FIN_TOPO:13, XBOOLE_1:28; thus A ^deltao = (A `) /\ ((A ^b) /\ ((A `) ^b)) by FIN_TOPO:18 .= (A ^b) /\ ((A `) /\ ((A `) ^b)) by XBOOLE_1:16 .= (A ^b) \ A by A1, SUBSET_1:13 ; ::_thesis: verum end; theorem :: FINTOPO6:23 for FT being non empty RelStr for A, B being Subset of FT st A,B are_separated holds A ^deltao misses B proof let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st A,B are_separated holds A ^deltao misses B let A, B be Subset of FT; ::_thesis: ( A,B are_separated implies A ^deltao misses B ) assume A,B are_separated ; ::_thesis: A ^deltao misses B then A1: A ^b misses B by FINTOPO4:def_1; thus (A ^deltao) /\ B = (A `) /\ ((A ^delta) /\ B) by XBOOLE_1:16 .= (A `) /\ (((A ^b) /\ ((A `) ^b)) /\ B) by FIN_TOPO:18 .= (A `) /\ (((A `) ^b) /\ ((A ^b) /\ B)) by XBOOLE_1:16 .= (A `) /\ (((A `) ^b) /\ {}) by A1, XBOOLE_0:def_7 .= {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; theorem :: FINTOPO6:24 for FT being non empty RelStr for A, B being Subset of FT st FT is filled & A misses B & A ^deltao misses B & B ^deltao misses A holds A,B are_separated proof let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is filled & A misses B & A ^deltao misses B & B ^deltao misses A holds A,B are_separated let A, B be Subset of FT; ::_thesis: ( FT is filled & A misses B & A ^deltao misses B & B ^deltao misses A implies A,B are_separated ) assume that A1: FT is filled and A2: A /\ B = {} and A3: (A ^deltao) /\ B = {} and A4: (B ^deltao) /\ A = {} ; :: according to XBOOLE_0:def_7 ::_thesis: A,B are_separated (B `) /\ ((B ^delta) /\ A) = {} by A4, XBOOLE_1:16; then (B `) /\ (((B ^b) /\ ((B `) ^b)) /\ A) = {} by FIN_TOPO:18; then (B `) /\ (((B `) ^b) /\ ((B ^b) /\ A)) = {} by XBOOLE_1:16; then A5: ((B `) /\ ((B `) ^b)) /\ ((B ^b) /\ A) = {} by XBOOLE_1:16; (B `) /\ ((B `) ^b) = B ` by A1, FIN_TOPO:13, XBOOLE_1:28; then B ` misses (B ^b) /\ A by A5, XBOOLE_0:def_7; then (B ^b) /\ A c= B by SUBSET_1:24; then ((B ^b) /\ A) /\ A c= B /\ A by XBOOLE_1:26; then (B ^b) /\ (A /\ A) c= B /\ A by XBOOLE_1:16; then (B ^b) /\ A = {} by A2, XBOOLE_1:3; then A6: A misses B ^b by XBOOLE_0:def_7; (A `) /\ ((A ^delta) /\ B) = {} by A3, XBOOLE_1:16; then (A `) /\ (((A ^b) /\ ((A `) ^b)) /\ B) = {} by FIN_TOPO:18; then (A `) /\ (((A `) ^b) /\ ((A ^b) /\ B)) = {} by XBOOLE_1:16; then A7: ((A `) /\ ((A `) ^b)) /\ ((A ^b) /\ B) = {} by XBOOLE_1:16; (A `) /\ ((A `) ^b) = A ` by A1, FIN_TOPO:13, XBOOLE_1:28; then A ` misses (A ^b) /\ B by A7, XBOOLE_0:def_7; then (A ^b) /\ B c= A by SUBSET_1:24; then ((A ^b) /\ B) /\ B c= A /\ B by XBOOLE_1:26; then (A ^b) /\ (B /\ B) c= A /\ B by XBOOLE_1:16; then (A ^b) /\ B = {} by A2, XBOOLE_1:3; then A ^b misses B by XBOOLE_0:def_7; hence A,B are_separated by A6, FINTOPO4:def_1; ::_thesis: verum end; theorem Th25: :: FINTOPO6:25 for FT being non empty RelStr for x being Point of FT holds {x} is connected proof let FT be non empty RelStr ; ::_thesis: for x being Point of FT holds {x} is connected let x be Point of FT; ::_thesis: {x} is connected assume not {x} is connected ; ::_thesis: contradiction then consider P, Q being Subset of FT such that A1: {x} = P \/ Q and A2: P <> {} and A3: Q <> {} and A4: P misses Q and ( not P ^b meets Q or not P meets Q ^b ) by Th3; P <> Q proof assume not P <> Q ; ::_thesis: contradiction then P /\ Q = P ; hence contradiction by A2, A4, XBOOLE_0:def_7; ::_thesis: verum end; hence contradiction by A1, A2, A3, ZFMISC_1:38; ::_thesis: verum end; registration let FT be non empty RelStr ; let x be Point of FT; cluster{x} -> connected for Subset of FT; coherence for b1 being Subset of FT st b1 = {x} holds b1 is connected by Th25; end; definition let FT be non empty RelStr ; let A be Subset of FT; predA is_a_component_of FT means :Def4: :: FINTOPO6:def 4 ( A is connected & ( for B being Subset of FT st B is connected & A c= B holds A = B ) ); end; :: deftheorem Def4 defines is_a_component_of FINTOPO6:def_4_:_ for FT being non empty RelStr for A being Subset of FT holds ( A is_a_component_of FT iff ( A is connected & ( for B being Subset of FT st B is connected & A c= B holds A = B ) ) ); theorem :: FINTOPO6:26 for FT being non empty RelStr for A being Subset of FT st A is_a_component_of FT holds A <> {} FT proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A is_a_component_of FT holds A <> {} FT let A be Subset of FT; ::_thesis: ( A is_a_component_of FT implies A <> {} FT ) set x = the Point of FT; {} c= { the Point of FT} by XBOOLE_1:2; hence ( A is_a_component_of FT implies A <> {} FT ) by Def4; ::_thesis: verum end; theorem Th27: :: FINTOPO6:27 for FT being non empty RelStr for A, B being Subset of FT st A is closed & B is closed & A misses B holds A,B are_separated proof let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st A is closed & B is closed & A misses B holds A,B are_separated let A, B be Subset of FT; ::_thesis: ( A is closed & B is closed & A misses B implies A,B are_separated ) assume that A1: A is closed and A2: B is closed and A3: A misses B ; ::_thesis: A,B are_separated A4: A /\ B = {} by A3, XBOOLE_0:def_7; then A /\ (B ^b) = {} by A2, FIN_TOPO:def_15; then A5: A misses B ^b by XBOOLE_0:def_7; (A ^b) /\ B = {} by A1, A4, FIN_TOPO:def_15; then A ^b misses B by XBOOLE_0:def_7; hence A,B are_separated by A5, FINTOPO4:def_1; ::_thesis: verum end; theorem Th28: :: FINTOPO6:28 for FT being non empty RelStr for A, B being Subset of FT st FT is filled & [#] FT = A \/ B & A,B are_separated holds ( A is open & A is closed ) proof let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is filled & [#] FT = A \/ B & A,B are_separated holds ( A is open & A is closed ) let A, B be Subset of FT; ::_thesis: ( FT is filled & [#] FT = A \/ B & A,B are_separated implies ( A is open & A is closed ) ) assume that A1: FT is filled and A2: [#] FT = A \/ B and A3: A,B are_separated ; ::_thesis: ( A is open & A is closed ) A4: B c= B ^b by A1, FIN_TOPO:13; now__::_thesis:_(_A_misses_B_^b_implies_B_^b_=_B_) assume A misses B ^b ; ::_thesis: B ^b = B then B ^b c= B by A2, XBOOLE_1:73; hence B ^b = B by A4, XBOOLE_0:def_10; ::_thesis: verum end; then A5: B is closed by A3, FINTOPO4:def_1, FIN_TOPO:def_15; A6: A c= A ^b by A1, FIN_TOPO:13; A7: now__::_thesis:_(_A_^b_misses_B_implies_A_^b_=_A_) assume A ^b misses B ; ::_thesis: A ^b = A then A ^b c= A by A2, XBOOLE_1:73; hence A ^b = A by A6, XBOOLE_0:def_10; ::_thesis: verum end; B ` = A by A1, A2, A3, FINTOPO4:6, PRE_TOPC:5; hence ( A is open & A is closed ) by A3, A7, A5, FINTOPO4:def_1, FIN_TOPO:24, FIN_TOPO:def_15; ::_thesis: verum end; theorem Th29: :: FINTOPO6:29 for FT being non empty RelStr for A, B, A1, B1 being Subset of FT st A,B are_separated & A1 c= A & B1 c= B holds A1,B1 are_separated proof let FT be non empty RelStr ; ::_thesis: for A, B, A1, B1 being Subset of FT st A,B are_separated & A1 c= A & B1 c= B holds A1,B1 are_separated let A, B, A1, B1 be Subset of FT; ::_thesis: ( A,B are_separated & A1 c= A & B1 c= B implies A1,B1 are_separated ) assume that A1: A,B are_separated and A2: A1 c= A and A3: B1 c= B ; ::_thesis: A1,B1 are_separated A misses B ^b by A1, FINTOPO4:def_1; then A4: A /\ (B ^b) = {} by XBOOLE_0:def_7; B1 ^b c= B ^b by A3, FIN_TOPO:14; then A1 /\ (B1 ^b) = {} FT by A2, A4, XBOOLE_1:3, XBOOLE_1:27; then A5: A1 misses B1 ^b by XBOOLE_0:def_7; A ^b misses B by A1, FINTOPO4:def_1; then A6: (A ^b) /\ B = {} by XBOOLE_0:def_7; A1 ^b c= A ^b by A2, FIN_TOPO:14; then (A1 ^b) /\ B1 = {} FT by A3, A6, XBOOLE_1:3, XBOOLE_1:27; then A1 ^b misses B1 by XBOOLE_0:def_7; hence A1,B1 are_separated by A5, FINTOPO4:def_1; ::_thesis: verum end; theorem Th30: :: FINTOPO6:30 for FT being non empty RelStr for A, B, C being Subset of FT st A,B are_separated & A,C are_separated holds A,B \/ C are_separated proof let FT be non empty RelStr ; ::_thesis: for A, B, C being Subset of FT st A,B are_separated & A,C are_separated holds A,B \/ C are_separated let A, B, C be Subset of FT; ::_thesis: ( A,B are_separated & A,C are_separated implies A,B \/ C are_separated ) assume that A1: A,B are_separated and A2: A,C are_separated ; ::_thesis: A,B \/ C are_separated A3: A ^b misses C by A2, FINTOPO4:def_1; A ^b misses B by A1, FINTOPO4:def_1; then A4: (A ^b) /\ B = {} by XBOOLE_0:def_7; (A ^b) /\ (B \/ C) = ((A ^b) /\ B) \/ ((A ^b) /\ C) by XBOOLE_1:23 .= {} by A3, A4, XBOOLE_0:def_7 ; then A5: A ^b misses B \/ C by XBOOLE_0:def_7; A misses B ^b by A1, FINTOPO4:def_1; then A6: A /\ (B ^b) = {} by XBOOLE_0:def_7; A7: A misses C ^b by A2, FINTOPO4:def_1; A /\ ((B \/ C) ^b) = A /\ ((B ^b) \/ (C ^b)) by Th1 .= (A /\ (B ^b)) \/ (A /\ (C ^b)) by XBOOLE_1:23 .= {} by A7, A6, XBOOLE_0:def_7 ; then A misses (B \/ C) ^b by XBOOLE_0:def_7; hence A,B \/ C are_separated by A5, FINTOPO4:def_1; ::_thesis: verum end; theorem :: FINTOPO6:31 for FT being non empty RelStr st FT is filled & FT is symmetric & ( for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds A meets B ) holds FT is connected proof let FT be non empty RelStr ; ::_thesis: ( FT is filled & FT is symmetric & ( for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds A meets B ) implies FT is connected ) assume A1: ( FT is filled & FT is symmetric ) ; ::_thesis: ( ex A, B being Subset of FT st ( [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed & not A meets B ) or FT is connected ) assume A2: for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds A meets B ; ::_thesis: FT is connected assume not FT is connected ; ::_thesis: contradiction then not [#] FT is connected by Def1; then consider P, Q being Subset of FT such that A3: [#] FT = P \/ Q and A4: P misses Q and A5: P,Q are_separated and A6: ( P <> {} FT & Q <> {} FT ) by A1, Th7; ( P is closed & Q is closed ) by A1, A3, A5, Th28; hence contradiction by A2, A3, A4, A6; ::_thesis: verum end; theorem :: FINTOPO6:32 for FT being non empty RelStr st FT is connected holds for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds A meets B proof let FT be non empty RelStr ; ::_thesis: ( FT is connected implies for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds A meets B ) assume A1: [#] FT is connected ; :: according to FINTOPO6:def_1 ::_thesis: for A, B being Subset of FT st [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed holds A meets B given A, B being Subset of FT such that A2: ( [#] FT = A \/ B & A <> {} FT & B <> {} FT & A is closed & B is closed & A misses B ) ; ::_thesis: contradiction thus contradiction by A1, A2, Th4, Th27; ::_thesis: verum end; theorem Th33: :: FINTOPO6:33 for FT being non empty RelStr for A, B, C being Subset of FT st FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B holds A c= C proof let FT be non empty RelStr ; ::_thesis: for A, B, C being Subset of FT st FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B holds A c= C let A, B, C be Subset of FT; ::_thesis: ( FT is filled & A is connected & A c= B \/ C & B,C are_separated & not A c= B implies A c= C ) assume that A1: FT is filled and A2: A is connected and A3: A c= B \/ C and A4: B,C are_separated ; ::_thesis: ( A c= B or A c= C ) A5: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23 .= A by A3, XBOOLE_1:28 ; assume that A6: not A c= B and A7: not A c= C ; ::_thesis: contradiction A meets B by A3, A7, XBOOLE_1:73; then A8: A /\ B <> {} by XBOOLE_0:def_7; A meets C by A3, A6, XBOOLE_1:73; then A9: A /\ C <> {} by XBOOLE_0:def_7; A10: ( A /\ B c= B & A /\ C c= C ) by XBOOLE_1:17; then ( {} FT = {} & A /\ B misses A /\ C ) by A1, A4, Th29, FINTOPO4:6; hence contradiction by A2, A4, A8, A9, A10, A5, Th4, Th29; ::_thesis: verum end; theorem Th34: :: FINTOPO6:34 for FT being non empty RelStr for A, B being Subset of FT st FT is symmetric & A is connected & B is connected & not A,B are_separated holds A \/ B is connected proof let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric & A is connected & B is connected & not A,B are_separated holds A \/ B is connected let A, B be Subset of FT; ::_thesis: ( FT is symmetric & A is connected & B is connected & not A,B are_separated implies A \/ B is connected ) assume that A1: FT is symmetric and A2: A is connected and A3: B is connected and A4: not A,B are_separated ; ::_thesis: A \/ B is connected given P, Q being Subset of FT such that A5: A \/ B = P \/ Q and A6: P <> {} and A7: Q <> {} and A8: P misses Q and A9: P ^b misses Q ; :: according to FIN_TOPO:def_16 ::_thesis: contradiction set P2 = A /\ P; set Q2 = A /\ Q; A10: A /\ P misses A /\ Q by A8, XBOOLE_1:76; A11: Q ^b misses P by A1, A9, Th6; A12: now__::_thesis:_(_A_c=_Q_implies_not_B_c=_P_) assume that A13: A c= Q and A14: B c= P ; ::_thesis: contradiction percases ( A ^b meets B or A meets B ^b ) by A4, FINTOPO4:def_1; suppose A ^b meets B ; ::_thesis: contradiction then Q ^b meets B by A13, FIN_TOPO:14, XBOOLE_1:63; hence contradiction by A11, A14, XBOOLE_1:63; ::_thesis: verum end; suppose A meets B ^b ; ::_thesis: contradiction then not A ^b misses B by A1, Th6; then Q ^b meets B by A13, FIN_TOPO:14, XBOOLE_1:63; hence contradiction by A11, A14, XBOOLE_1:63; ::_thesis: verum end; end; end; A15: now__::_thesis:_not_A_/\_P_=_{} assume A16: A /\ P = {} ; ::_thesis: contradiction then A17: A /\ Q = (A /\ P) \/ (A /\ Q) .= A /\ (P \/ Q) by XBOOLE_1:23 .= A by A5, XBOOLE_1:21 ; A18: now__::_thesis:_not_B_/\_Q_=_{} assume B /\ Q = {} ; ::_thesis: contradiction then B /\ P = (B /\ Q) \/ (B /\ P) .= B /\ (Q \/ P) by XBOOLE_1:23 .= B by A5, XBOOLE_1:21 ; hence contradiction by A12, A17, XBOOLE_1:18; ::_thesis: verum end; set P3 = B /\ P; set Q3 = B /\ Q; A19: (B /\ P) \/ (B /\ Q) = B /\ (P \/ Q) by XBOOLE_1:23 .= B by A5, XBOOLE_1:21 ; A20: B /\ P misses B /\ Q by A8, XBOOLE_1:76; ( (B /\ P) ^b c= P ^b & B /\ Q c= Q ) by FIN_TOPO:14, XBOOLE_1:17; then A21: (B /\ P) ^b misses B /\ Q by A9, XBOOLE_1:64; B /\ P = (A /\ P) \/ (B /\ P) by A16 .= (A \/ B) /\ P by XBOOLE_1:23 .= P by A5, XBOOLE_1:21 ; hence contradiction by A3, A6, A18, A19, A20, A21, FIN_TOPO:def_16; ::_thesis: verum end; A22: now__::_thesis:_(_A_c=_P_implies_not_B_c=_Q_) assume that A23: A c= P and A24: B c= Q ; ::_thesis: contradiction A25: A ^b c= P ^b by A23, FIN_TOPO:14; percases ( A ^b meets B or A meets B ^b ) by A4, FINTOPO4:def_1; suppose A ^b meets B ; ::_thesis: contradiction hence contradiction by A9, A24, A25, XBOOLE_1:64; ::_thesis: verum end; suppose A meets B ^b ; ::_thesis: contradiction then not A ^b misses B by A1, Th6; hence contradiction by A9, A24, A25, XBOOLE_1:64; ::_thesis: verum end; end; end; A26: now__::_thesis:_not_A_/\_Q_=_{} assume A27: A /\ Q = {} ; ::_thesis: contradiction then A28: A /\ P = (A /\ Q) \/ (A /\ P) .= A /\ (Q \/ P) by XBOOLE_1:23 .= A by A5, XBOOLE_1:21 ; A29: now__::_thesis:_not_B_/\_P_=_{} assume B /\ P = {} ; ::_thesis: contradiction then B /\ Q = (B /\ P) \/ (B /\ Q) .= B /\ (P \/ Q) by XBOOLE_1:23 .= B by A5, XBOOLE_1:21 ; hence contradiction by A22, A28, XBOOLE_1:18; ::_thesis: verum end; set P3 = B /\ Q; set Q3 = B /\ P; A30: (B /\ P) \/ (B /\ Q) = B /\ (P \/ Q) by XBOOLE_1:23 .= B by A5, XBOOLE_1:21 ; A31: B /\ Q misses B /\ P by A8, XBOOLE_1:76; ( (B /\ Q) ^b c= Q ^b & B /\ P c= P ) by FIN_TOPO:14, XBOOLE_1:17; then A32: (B /\ Q) ^b misses B /\ P by A11, XBOOLE_1:64; B /\ Q = (A /\ Q) \/ (B /\ Q) by A27 .= (A \/ B) /\ Q by XBOOLE_1:23 .= Q by A5, XBOOLE_1:21 ; hence contradiction by A3, A7, A29, A30, A31, A32, FIN_TOPO:def_16; ::_thesis: verum end; ( (A /\ P) ^b c= P ^b & A /\ Q c= Q ) by FIN_TOPO:14, XBOOLE_1:17; then A33: (A /\ P) ^b misses A /\ Q by A9, XBOOLE_1:64; (A /\ P) \/ (A /\ Q) = A /\ (P \/ Q) by XBOOLE_1:23 .= A by A5, XBOOLE_1:21 ; hence contradiction by A2, A15, A26, A10, A33, FIN_TOPO:def_16; ::_thesis: verum end; theorem Th35: :: FINTOPO6:35 for FT being non empty RelStr for A, C being Subset of FT st FT is symmetric & C is connected & C c= A & A c= C ^b holds A is connected proof let FT be non empty RelStr ; ::_thesis: for A, C being Subset of FT st FT is symmetric & C is connected & C c= A & A c= C ^b holds A is connected let A, C be Subset of FT; ::_thesis: ( FT is symmetric & C is connected & C c= A & A c= C ^b implies A is connected ) assume that A1: FT is symmetric and A2: C is connected and A3: C c= A and A4: A c= C ^b ; ::_thesis: A is connected let P2, Q2 be Subset of FT; :: according to FIN_TOPO:def_16 ::_thesis: ( not A = P2 \/ Q2 or P2 = {} or Q2 = {} or not P2 misses Q2 or not P2 ^b misses Q2 ) assume that A5: A = P2 \/ Q2 and A6: P2 <> {} and A7: Q2 <> {} and A8: P2 misses Q2 ; ::_thesis: not P2 ^b misses Q2 assume A9: P2 ^b misses Q2 ; ::_thesis: contradiction set x2 = the Element of Q2; A10: the Element of Q2 in Q2 by A7; Q2 c= Q2 \/ P2 by XBOOLE_1:7; then Q2 c= C ^b by A4, A5, XBOOLE_1:1; then the Element of Q2 in C ^b by A10; then consider z2 being Element of FT such that A11: z2 = the Element of Q2 and A12: U_FT z2 meets C ; set y3 = the Element of (U_FT z2) /\ C; A13: (U_FT z2) /\ C <> {} by A12, XBOOLE_0:def_7; then the Element of (U_FT z2) /\ C in (U_FT z2) /\ C ; then reconsider y4 = the Element of (U_FT z2) /\ C as Element of FT ; the Element of (U_FT z2) /\ C in U_FT z2 by A13, XBOOLE_0:def_4; then z2 in U_FT y4 by A1, FIN_TOPO:def_13; then z2 in (U_FT y4) /\ Q2 by A7, A11, XBOOLE_0:def_4; then A14: U_FT y4 meets Q2 by XBOOLE_0:def_7; set P3 = P2 /\ C; set Q3 = Q2 /\ C; A15: C = A /\ C by A3, XBOOLE_1:28 .= (P2 /\ C) \/ (Q2 /\ C) by A5, XBOOLE_1:23 ; set x = the Element of P2; A16: the Element of P2 in P2 by A6; P2 c= P2 \/ Q2 by XBOOLE_1:7; then P2 c= C ^b by A4, A5, XBOOLE_1:1; then the Element of P2 in C ^b by A16; then consider z being Element of FT such that A17: z = the Element of P2 and A18: U_FT z meets C ; set y = the Element of (U_FT z) /\ C; A19: (U_FT z) /\ C <> {} by A18, XBOOLE_0:def_7; then the Element of (U_FT z) /\ C in (U_FT z) /\ C ; then reconsider y2 = the Element of (U_FT z) /\ C as Element of FT ; the Element of (U_FT z) /\ C in U_FT z by A19, XBOOLE_0:def_4; then z in U_FT y2 by A1, FIN_TOPO:def_13; then z in (U_FT y2) /\ P2 by A6, A17, XBOOLE_0:def_4; then U_FT y2 meets P2 by XBOOLE_0:def_7; then A20: y2 in P2 ^b ; A21: y4 in C by A13, XBOOLE_0:def_4; A22: now__::_thesis:_not_Q2_/\_C_=_{} assume Q2 /\ C = {} ; ::_thesis: contradiction then A23: y4 in P2 by A21, A15, XBOOLE_0:def_4; consider w being Element of FT such that A24: w = y4 and A25: U_FT w meets Q2 by A14; consider s being set such that A26: s in U_FT w and A27: s in Q2 by A25, XBOOLE_0:3; reconsider s2 = s as Element of FT by A26; w in U_FT s2 by A1, A26, FIN_TOPO:def_13; then U_FT s2 meets P2 by A23, A24, XBOOLE_0:3; then s2 in P2 ^b ; hence contradiction by A9, A27, XBOOLE_0:3; ::_thesis: verum end; A28: P2 /\ C c= P2 by XBOOLE_1:17; A29: y2 in C by A19, XBOOLE_0:def_4; A30: now__::_thesis:_not_P2_/\_C_=_{} assume P2 /\ C = {} ; ::_thesis: contradiction then y2 in Q2 by A29, A15, XBOOLE_0:def_4; then y2 in (P2 ^b) /\ Q2 by A20, XBOOLE_0:def_4; hence contradiction by A9, XBOOLE_0:def_7; ::_thesis: verum end; P2 /\ C misses Q2 by A8, XBOOLE_1:17, XBOOLE_1:63; then P2 /\ C misses Q2 /\ C by XBOOLE_1:17, XBOOLE_1:63; then (P2 /\ C) ^b meets Q2 /\ C by A2, A15, A30, A22, FIN_TOPO:def_16; then P2 ^b meets Q2 /\ C by A28, FIN_TOPO:14, XBOOLE_1:63; hence contradiction by A9, XBOOLE_1:17, XBOOLE_1:63; ::_thesis: verum end; theorem Th36: :: FINTOPO6:36 for FT being non empty RelStr for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds C ^b is connected proof let FT be non empty RelStr ; ::_thesis: for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds C ^b is connected let C be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & C is connected implies C ^b is connected ) assume that A1: ( FT is filled & FT is symmetric ) and A2: C is connected ; ::_thesis: C ^b is connected C c= C ^b by A1, FIN_TOPO:13; hence C ^b is connected by A1, A2, Th35; ::_thesis: verum end; theorem Th37: :: FINTOPO6:37 for FT being non empty RelStr for A, B, C being Subset of FT st FT is filled & FT is symmetric & FT is connected & A is connected & ([#] FT) \ A = B \/ C & B,C are_separated holds A \/ B is connected proof let FT be non empty RelStr ; ::_thesis: for A, B, C being Subset of FT st FT is filled & FT is symmetric & FT is connected & A is connected & ([#] FT) \ A = B \/ C & B,C are_separated holds A \/ B is connected let A, B, C be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & FT is connected & A is connected & ([#] FT) \ A = B \/ C & B,C are_separated implies A \/ B is connected ) assume that A1: ( FT is filled & FT is symmetric ) and A2: FT is connected and A3: A is connected and A4: ([#] FT) \ A = B \/ C and A5: B,C are_separated ; ::_thesis: A \/ B is connected A6: [#] FT is connected by A2, Def1; now__::_thesis:_for_P,_Q_being_Subset_of_FT_st_A_\/_B_=_P_\/_Q_&_P_misses_Q_&_P,Q_are_separated_&_not_P_=_{}_FT_holds_ Q_=_{}_FT let P, Q be Subset of FT; ::_thesis: ( A \/ B = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT implies Q = {} FT ) assume that A7: A \/ B = P \/ Q and P misses Q and A8: P,Q are_separated ; ::_thesis: ( P = {} FT or Q = {} FT ) A9: [#] FT = A \/ (B \/ C) by A4, XBOOLE_1:45 .= (P \/ Q) \/ C by A7, XBOOLE_1:4 ; A10: now__::_thesis:_(_not_A_c=_Q_or_P_=_{}_FT_or_Q_=_{}_FT_) A11: [#] FT = P \/ (Q \/ C) by A9, XBOOLE_1:4; assume A c= Q ; ::_thesis: ( P = {} FT or Q = {} FT ) then P misses A by A1, A8, Th29, FINTOPO4:6; then P c= B by A7, XBOOLE_1:7, XBOOLE_1:73; then A12: P,C are_separated by A5, Th29; then P misses Q \/ C by A1, A8, Th30, FINTOPO4:6; hence ( P = {} FT or Q = {} FT ) by A6, A8, A12, A11, Th4, Th30; ::_thesis: verum end; now__::_thesis:_(_not_A_c=_P_or_P_=_{}_FT_or_Q_=_{}_FT_) A13: [#] FT = Q \/ (P \/ C) by A9, XBOOLE_1:4; assume A c= P ; ::_thesis: ( P = {} FT or Q = {} FT ) then Q misses A by A1, A8, Th29, FINTOPO4:6; then Q c= B by A7, XBOOLE_1:7, XBOOLE_1:73; then A14: Q,C are_separated by A5, Th29; then Q misses P \/ C by A1, A8, Th30, FINTOPO4:6; hence ( P = {} FT or Q = {} FT ) by A6, A8, A14, A13, Th4, Th30; ::_thesis: verum end; hence ( P = {} FT or Q = {} FT ) by A1, A3, A7, A8, A10, Th33, XBOOLE_1:7; ::_thesis: verum end; hence A \/ B is connected by A1, Th7; ::_thesis: verum end; theorem Th38: :: FINTOPO6:38 for FT being non empty RelStr for X9 being non empty SubSpace of FT for A being Subset of FT for B being Subset of X9 st A = B holds ( A is connected iff B is connected ) proof let FT be non empty RelStr ; ::_thesis: for X9 being non empty SubSpace of FT for A being Subset of FT for B being Subset of X9 st A = B holds ( A is connected iff B is connected ) let X9 be non empty SubSpace of FT; ::_thesis: for A being Subset of FT for B being Subset of X9 st A = B holds ( A is connected iff B is connected ) let A8 be Subset of FT; ::_thesis: for B being Subset of X9 st A8 = B holds ( A8 is connected iff B is connected ) let B8 be Subset of X9; ::_thesis: ( A8 = B8 implies ( A8 is connected iff B8 is connected ) ) assume A1: A8 = B8 ; ::_thesis: ( A8 is connected iff B8 is connected ) percases ( A8 = {} or A8 <> {} ) ; suppose A8 = {} ; ::_thesis: ( A8 is connected iff B8 is connected ) hence ( A8 is connected iff B8 is connected ) by A1; ::_thesis: verum end; supposeA2: A8 <> {} ; ::_thesis: ( A8 is connected iff B8 is connected ) then reconsider A = A8 as non empty Subset of FT ; reconsider B = B8 as non empty Subset of X9 by A1, A2; reconsider X = X9 as non empty RelStr ; A3: now__::_thesis:_(_not_A8_is_connected_implies_not_B8_is_connected_) assume not A8 is connected ; ::_thesis: not B8 is connected then consider P, Q being Subset of FT such that A4: A8 = P \/ Q and A5: ( P <> {} & Q <> {} & P misses Q ) and A6: P ^b misses Q by FIN_TOPO:def_16; Q c= A8 by A4, XBOOLE_1:7; then reconsider Q9 = Q as Subset of X by A1, XBOOLE_1:1; P c= A8 by A4, XBOOLE_1:7; then reconsider P9 = P as Subset of X by A1, XBOOLE_1:1; A7: Q9 c= the carrier of X ; P9 ^b = (P ^b) /\ ([#] X) by Th13; then (P9 ^b) /\ Q9 = (P ^b) /\ (([#] X) /\ Q) by XBOOLE_1:16 .= (P ^b) /\ Q by A7, XBOOLE_1:28 .= {} by A6, XBOOLE_0:def_7 ; then P9 ^b misses Q9 by XBOOLE_0:def_7; hence not B8 is connected by A1, A4, A5, FIN_TOPO:def_16; ::_thesis: verum end; now__::_thesis:_(_not_B_is_connected_implies_not_A_is_connected_) assume not B is connected ; ::_thesis: not A is connected then consider P, Q being Subset of X9 such that A8: ( B8 = P \/ Q & P <> {} & Q <> {} & P misses Q ) and A9: P ^b misses Q by FIN_TOPO:def_16; the carrier of X c= the carrier of FT by Def2; then reconsider Q9 = Q as Subset of FT by XBOOLE_1:1; the carrier of X c= the carrier of FT by Def2; then reconsider P9 = P as Subset of FT by XBOOLE_1:1; A10: P ^b = (P9 ^b) /\ ([#] X) by Th13; (P9 ^b) /\ Q9 = (P9 ^b) /\ (([#] X) /\ Q) by XBOOLE_1:28 .= (P ^b) /\ Q by A10, XBOOLE_1:16 .= {} by A9, XBOOLE_0:def_7 ; then P9 ^b misses Q9 by XBOOLE_0:def_7; hence not A is connected by A1, A8, FIN_TOPO:def_16; ::_thesis: verum end; hence ( A8 is connected iff B8 is connected ) by A3; ::_thesis: verum end; end; end; theorem :: FINTOPO6:39 for FT being non empty RelStr for A being Subset of FT st FT is filled & FT is symmetric & A is_a_component_of FT holds A is closed proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is filled & FT is symmetric & A is_a_component_of FT holds A is closed let A be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & A is_a_component_of FT implies A is closed ) assume that A1: ( FT is filled & FT is symmetric ) and A2: A is_a_component_of FT ; ::_thesis: A is closed A is connected by A2, Def4; then A3: A ^b is connected by A1, Th36; A c= A ^b by A1, FIN_TOPO:13; hence A = A ^b by A2, A3, Def4; :: according to FIN_TOPO:def_15 ::_thesis: verum end; theorem Th40: :: FINTOPO6:40 for FT being non empty RelStr for A, B being Subset of FT st FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds A,B are_separated proof let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds A,B are_separated let A, B be Subset of FT; ::_thesis: ( FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B implies A,B are_separated ) assume that A1: FT is symmetric and A2: A is_a_component_of FT and A3: B is_a_component_of FT ; ::_thesis: ( A = B or A,B are_separated ) A4: A is connected by A2, Def4; A5: A c= A \/ B by XBOOLE_1:7; assume that A6: A <> B and A7: not A,B are_separated ; ::_thesis: contradiction B is connected by A3, Def4; then A \/ B is connected by A1, A7, A4, Th34; then ( B c= A \/ B & A = A \/ B ) by A2, A5, Def4, XBOOLE_1:7; hence contradiction by A3, A6, A4, Def4; ::_thesis: verum end; theorem :: FINTOPO6:41 for FT being non empty RelStr for A, B being Subset of FT st FT is filled & FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds A misses B by Th40, FINTOPO4:6; theorem :: FINTOPO6:42 for FT being non empty RelStr for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds for S being Subset of FT holds ( not S is_a_component_of FT or C misses S or C c= S ) proof let FT be non empty RelStr ; ::_thesis: for C being Subset of FT st FT is filled & FT is symmetric & C is connected holds for S being Subset of FT holds ( not S is_a_component_of FT or C misses S or C c= S ) let C be Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & C is connected implies for S being Subset of FT holds ( not S is_a_component_of FT or C misses S or C c= S ) ) assume A1: ( FT is filled & FT is symmetric & C is connected ) ; ::_thesis: for S being Subset of FT holds ( not S is_a_component_of FT or C misses S or C c= S ) let S be Subset of FT; ::_thesis: ( not S is_a_component_of FT or C misses S or C c= S ) assume A2: S is_a_component_of FT ; ::_thesis: ( C misses S or C c= S ) A3: S c= C \/ S by XBOOLE_1:7; assume A4: C meets S ; ::_thesis: C c= S S is connected by A2, Def4; then C \/ S is connected by A1, A4, Th34, FINTOPO4:6; then S = C \/ S by A2, A3, Def4; hence C c= S by XBOOLE_1:7; ::_thesis: verum end; definition let FT be non empty RelStr ; let A be non empty Subset of FT; let B be Subset of FT; predB is_a_component_of A means :Def5: :: FINTOPO6:def 5 ex B1 being Subset of (FT | A) st ( B1 = B & B1 is_a_component_of FT | A ); end; :: deftheorem Def5 defines is_a_component_of FINTOPO6:def_5_:_ for FT being non empty RelStr for A being non empty Subset of FT for B being Subset of FT holds ( B is_a_component_of A iff ex B1 being Subset of (FT | A) st ( B1 = B & B1 is_a_component_of FT | A ) ); theorem :: FINTOPO6:43 for FT being non empty RelStr for A, C being Subset of FT for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds ([#] FT) \ C is connected proof let FT be non empty RelStr ; ::_thesis: for A, C being Subset of FT for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds ([#] FT) \ C is connected let A, C be Subset of FT; ::_thesis: for D being non empty Subset of FT st FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D holds ([#] FT) \ C is connected let D be non empty Subset of FT; ::_thesis: ( FT is filled & FT is symmetric & D = ([#] FT) \ A & FT is connected & A is connected & C is_a_component_of D implies ([#] FT) \ C is connected ) assume that A1: ( FT is filled & FT is symmetric ) and A2: D = ([#] FT) \ A and A3: FT is connected and A4: A is connected and A5: C is_a_component_of D ; ::_thesis: ([#] FT) \ C is connected consider C1 being Subset of (FT | D) such that A6: C1 = C and A7: C1 is_a_component_of FT | D by A5, Def5; reconsider C2 = C1 as Subset of FT by A6; C1 c= [#] (FT | D) ; then C1 c= ([#] FT) \ A by A2, Def3; then A8: (([#] FT) \ A) ` c= C2 ` by SUBSET_1:12; then A9: A c= C2 ` by PRE_TOPC:3; A10: A c= ([#] FT) \ C2 by A8, PRE_TOPC:3; A11: C1 is connected by A7, Def4; now__::_thesis:_for_P,_Q_being_Subset_of_FT_st_([#]_FT)_\_C_=_P_\/_Q_&_P_misses_Q_&_P,Q_are_separated_&_not_P_=_{}_FT_holds_ Q_=_{}_FT A misses C1 by A9, SUBSET_1:23; then A12: A /\ C1 = {} by XBOOLE_0:def_7; let P, Q be Subset of FT; ::_thesis: ( ([#] FT) \ C = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT implies Q = {} FT ) assume that A13: ([#] FT) \ C = P \/ Q and A14: P misses Q and A15: P,Q are_separated ; ::_thesis: ( P = {} FT or Q = {} FT ) A16: C is connected by A6, A11, Th38; A17: now__::_thesis:_(_A_c=_Q_implies_P_=_{}_FT_) assume A18: A c= Q ; ::_thesis: P = {} FT P c= Q ` by A14, SUBSET_1:23; then ( Q misses Q ` & A /\ P c= Q /\ (Q `) ) by A18, XBOOLE_1:27, XBOOLE_1:79; then A19: A /\ P c= {} by XBOOLE_0:def_7; (C \/ P) /\ A = (A /\ C) \/ (A /\ P) by XBOOLE_1:23 .= {} by A6, A12, A19, XBOOLE_1:3 ; then C \/ P misses A by XBOOLE_0:def_7; then C \/ P c= A ` by SUBSET_1:23; then C \/ P c= [#] (FT | D) by A2, Def3; then reconsider C1P1 = C \/ P as Subset of (FT | D) ; C \/ P is connected by A1, A3, A13, A15, A16, Th37; then A20: C1P1 is connected by Th38; C c= C1 \/ P by A6, XBOOLE_1:7; then C1P1 = C1 by A6, A7, A20, Def4; then A21: P c= C by A6, XBOOLE_1:7; P c= ([#] FT) \ C by A13, XBOOLE_1:7; then ( C misses C ` & P c= C /\ (([#] FT) \ C) ) by A21, XBOOLE_1:19, XBOOLE_1:79; then P c= {} by XBOOLE_0:def_7; hence P = {} FT by XBOOLE_1:3; ::_thesis: verum end; A22: P misses P ` by XBOOLE_1:79; A23: Q c= ([#] FT) \ C by A13, XBOOLE_1:7; now__::_thesis:_(_A_c=_P_implies_Q_=_{}_FT_) assume A24: A c= P ; ::_thesis: Q = {} FT Q c= P ` by A14, SUBSET_1:23; then A /\ Q c= P /\ (P `) by A24, XBOOLE_1:27; then A25: A /\ Q c= {} by A22, XBOOLE_0:def_7; (C \/ Q) /\ A = (A /\ C) \/ (A /\ Q) by XBOOLE_1:23 .= {} by A6, A12, A25, XBOOLE_1:3 ; then C \/ Q misses A by XBOOLE_0:def_7; then C \/ Q c= A ` by SUBSET_1:23; then C \/ Q c= [#] (FT | D) by A2, Def3; then reconsider C1Q1 = C \/ Q as Subset of (FT | D) ; C \/ Q is connected by A1, A3, A13, A15, A16, Th37; then A26: C1Q1 is connected by Th38; C1 c= C1 \/ Q by XBOOLE_1:7; then C1Q1 = C1 by A6, A7, A26, Def4; then Q c= C by A6, XBOOLE_1:7; then ( C misses C ` & Q c= C /\ (([#] FT) \ C) ) by A23, XBOOLE_1:19, XBOOLE_1:79; then Q c= {} by XBOOLE_0:def_7; hence Q = {} FT by XBOOLE_1:3; ::_thesis: verum end; hence ( P = {} FT or Q = {} FT ) by A1, A4, A6, A10, A13, A15, A17, Th33; ::_thesis: verum end; hence ([#] FT) \ C is connected by A1, Th7; ::_thesis: verum end; begin definition let FT be non empty RelStr ; let f be FinSequence of FT; attrf is continuous means :Def6: :: FINTOPO6:def 6 ( 1 <= len f & ( for i being Nat for x1 being Element of FT st 1 <= i & i < len f & x1 = f . i holds f . (i + 1) in U_FT x1 ) ); end; :: deftheorem Def6 defines continuous FINTOPO6:def_6_:_ for FT being non empty RelStr for f being FinSequence of FT holds ( f is continuous iff ( 1 <= len f & ( for i being Nat for x1 being Element of FT st 1 <= i & i < len f & x1 = f . i holds f . (i + 1) in U_FT x1 ) ) ); Lm2: for FT being non empty RelStr for x being Element of FT holds <*x*> is continuous proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT holds <*x*> is continuous let x be Element of FT; ::_thesis: <*x*> is continuous thus 1 <= len <*x*> by FINSEQ_1:39; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat for x1 being Element of FT st 1 <= i & i < len <*x*> & x1 = <*x*> . i holds <*x*> . (i + 1) in U_FT x1 thus for i being Nat for x1 being Element of FT st 1 <= i & i < len <*x*> & x1 = <*x*> . i holds <*x*> . (i + 1) in U_FT x1 by FINSEQ_1:39; ::_thesis: verum end; registration let FT be non empty RelStr ; let x be Element of FT; cluster<*x*> -> continuous for FinSequence of FT; coherence for b1 being FinSequence of FT st b1 = <*x*> holds b1 is continuous by Lm2; end; theorem Th44: :: FINTOPO6:44 for FT being non empty RelStr for f being FinSequence of FT for x, y being Element of FT st f is continuous & y = f . (len f) & x in U_FT y holds f ^ <*x*> is continuous proof let FT be non empty RelStr ; ::_thesis: for f being FinSequence of FT for x, y being Element of FT st f is continuous & y = f . (len f) & x in U_FT y holds f ^ <*x*> is continuous let f be FinSequence of FT; ::_thesis: for x, y being Element of FT st f is continuous & y = f . (len f) & x in U_FT y holds f ^ <*x*> is continuous let x, y be Element of FT; ::_thesis: ( f is continuous & y = f . (len f) & x in U_FT y implies f ^ <*x*> is continuous ) assume that A1: f is continuous and A2: y = f . (len f) and A3: x in U_FT y ; ::_thesis: f ^ <*x*> is continuous reconsider g = f ^ <*x*> as FinSequence of FT ; A4: dom f = Seg (len f) by FINSEQ_1:def_3; A5: len <*x*> = 1 by FINSEQ_1:39; A6: for i being Nat for x1 being Element of FT st 1 <= i & i < len g & x1 = g . i holds g . (i + 1) in U_FT x1 proof let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len g & x1 = g . i holds g . (i + 1) in U_FT x1 let x1 be Element of FT; ::_thesis: ( 1 <= i & i < len g & x1 = g . i implies g . (i + 1) in U_FT x1 ) assume that A7: 1 <= i and A8: i < len g and A9: x1 = g . i ; ::_thesis: g . (i + 1) in U_FT x1 ( i + 1 <= len g & 1 < i + 1 ) by A7, A8, NAT_1:13; then i + 1 in dom g by FINSEQ_3:25; then g . (i + 1) = g /. (i + 1) by PARTFUN1:def_6; then reconsider x2 = g . (i + 1) as Element of FT ; now__::_thesis:_x2_in_U_FT_x1 percases ( i < len f or i >= len f ) ; supposeA10: i < len f ; ::_thesis: x2 in U_FT x1 A11: 1 <= i + 1 by NAT_1:11; i + 1 <= len f by A10, NAT_1:13; then i + 1 in dom f by A11, FINSEQ_3:25; then A12: g . (i + 1) = f . (i + 1) by FINSEQ_1:def_7; i in dom f by A4, A7, A10, FINSEQ_1:1; then g . i = f . i by FINSEQ_1:def_7; hence x2 in U_FT x1 by A1, A7, A9, A10, A12, Def6; ::_thesis: verum end; supposeA13: i >= len f ; ::_thesis: x2 in U_FT x1 len g = (len f) + 1 by A5, FINSEQ_1:22; then A14: i <= len f by A8, NAT_1:13; then A15: i = len f by A13, XXREAL_0:1; i in dom f by A4, A7, A14, FINSEQ_1:1; then x1 = y by A2, A9, A15, FINSEQ_1:def_7; hence x2 in U_FT x1 by A3, A15, FINSEQ_1:42; ::_thesis: verum end; end; end; hence g . (i + 1) in U_FT x1 ; ::_thesis: verum end; len (f ^ <*x*>) = (len f) + (len <*x*>) by FINSEQ_1:22 .= (len f) + 1 by FINSEQ_1:39 ; then len (f ^ <*x*>) >= 1 by NAT_1:11; hence f ^ <*x*> is continuous by A6, Def6; ::_thesis: verum end; theorem Th45: :: FINTOPO6:45 for FT being non empty RelStr for f, g being FinSequence of FT st f is continuous & g is continuous & g . 1 in U_FT (f /. (len f)) holds f ^ g is continuous proof let FT be non empty RelStr ; ::_thesis: for f, g being FinSequence of FT st f is continuous & g is continuous & g . 1 in U_FT (f /. (len f)) holds f ^ g is continuous let f, g be FinSequence of FT; ::_thesis: ( f is continuous & g is continuous & g . 1 in U_FT (f /. (len f)) implies f ^ g is continuous ) assume that A1: f is continuous and A2: g is continuous and A3: g . 1 in U_FT (f /. (len f)) ; ::_thesis: f ^ g is continuous A4: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; len g >= 1 by A2, Def6; then len (f ^ g) >= 0 + 1 by A4, XREAL_1:7; hence len (f ^ g) >= 1 ; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat for x1 being Element of FT st 1 <= i & i < len (f ^ g) & x1 = (f ^ g) . i holds (f ^ g) . (i + 1) in U_FT x1 let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len (f ^ g) & x1 = (f ^ g) . i holds (f ^ g) . (i + 1) in U_FT x1 let x1 be Element of FT; ::_thesis: ( 1 <= i & i < len (f ^ g) & x1 = (f ^ g) . i implies (f ^ g) . (i + 1) in U_FT x1 ) set g2 = f ^ g; A5: dom f = Seg (len f) by FINSEQ_1:def_3; A6: len f >= 1 by A1, Def6; assume that A7: 1 <= i and A8: i < len (f ^ g) and A9: x1 = (f ^ g) . i ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1 ( i + 1 <= len (f ^ g) & 1 < i + 1 ) by A7, A8, NAT_1:13; then i + 1 in dom (f ^ g) by FINSEQ_3:25; then (f ^ g) . (i + 1) = (f ^ g) /. (i + 1) by PARTFUN1:def_6; then reconsider x2 = (f ^ g) . (i + 1) as Element of FT ; percases ( i < len f or i >= len f ) ; supposeA10: i < len f ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1 A11: 1 <= i + 1 by NAT_1:11; i + 1 <= len f by A10, NAT_1:13; then i + 1 in dom f by A11, FINSEQ_3:25; then A12: (f ^ g) . (i + 1) = f . (i + 1) by FINSEQ_1:def_7; i in dom f by A5, A7, A10, FINSEQ_1:1; then (f ^ g) . i = f . i by FINSEQ_1:def_7; hence (f ^ g) . (i + 1) in U_FT x1 by A1, A7, A9, A10, A12, Def6; ::_thesis: verum end; supposeA13: i >= len f ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1 then A14: i + 1 > len f by NAT_1:13; A15: i < (len f) + (len g) by A8, FINSEQ_1:22; A16: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; then A17: i + 1 <= (len f) + (len g) by A8, NAT_1:13; percases ( i = len f or i > len f ) by A13, XXREAL_0:1; supposeA18: i = len f ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1 A19: len f in dom f by A6, FINSEQ_3:25; then A20: x1 = f . (len f) by A9, A18, FINSEQ_1:def_7 .= f /. (len f) by A19, PARTFUN1:def_6 ; x2 = g . ((i + 1) - (len f)) by A14, A16, A17, FINSEQ_1:24 .= g . 1 by A18 ; hence (f ^ g) . (i + 1) in U_FT x1 by A3, A20; ::_thesis: verum end; supposeA21: i > len f ; ::_thesis: (f ^ g) . (i + 1) in U_FT x1 set j = i -' (len f); A22: i - (len f) > 0 by A21, XREAL_1:50; then A23: i -' (len f) = i - (len f) by XREAL_0:def_2; then (i -' (len f)) + 1 = (i + 1) - (len f) ; then A24: x2 = g . ((i -' (len f)) + 1) by A14, A16, A17, FINSEQ_1:24; A25: i - (len f) < len g by A15, XREAL_1:19; i >= (len f) + 1 by A21, NAT_1:13; then A26: x1 = g . (i -' (len f)) by A9, A15, A23, FINSEQ_1:23; i -' (len f) >= 0 + 1 by A22, A23, NAT_1:13; hence (f ^ g) . (i + 1) in U_FT x1 by A2, A23, A24, A26, A25, Def6; ::_thesis: verum end; end; end; end; end; definition let FT be non empty RelStr ; let A be Subset of FT; attrA is arcwise_connected means :Def7: :: FINTOPO6:def 7 for x1, x2 being Element of FT st x1 in A & x2 in A holds ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ); end; :: deftheorem Def7 defines arcwise_connected FINTOPO6:def_7_:_ for FT being non empty RelStr for A being Subset of FT holds ( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ); registration let FT be non empty RelStr ; cluster empty -> arcwise_connected for Element of K32( the carrier of FT); coherence for b1 being Subset of FT st b1 is empty holds b1 is arcwise_connected proof let S be Subset of FT; ::_thesis: ( S is empty implies S is arcwise_connected ) assume S is empty ; ::_thesis: S is arcwise_connected hence for x1, x2 being Element of FT st x1 in S & x2 in S holds ex f being FinSequence of FT st ( f is continuous & rng f c= S & f . 1 = x1 & f . (len f) = x2 ) ; :: according to FINTOPO6:def_7 ::_thesis: verum end; end; Lm3: for FT being non empty RelStr for x being Element of FT holds {x} is arcwise_connected proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT holds {x} is arcwise_connected let x be Element of FT; ::_thesis: {x} is arcwise_connected set A = {x}; A1: rng <*x*> c= {x} by FINSEQ_1:39; A2: <*x*> . 1 = x by FINSEQ_1:40; then A3: <*x*> . (len <*x*>) = x by FINSEQ_1:40; for x1, x2 being Element of FT st x1 in {x} & x2 in {x} holds ex f being FinSequence of FT st ( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) proof let x1, x2 be Element of FT; ::_thesis: ( x1 in {x} & x2 in {x} implies ex f being FinSequence of FT st ( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) ) assume ( x1 in {x} & x2 in {x} ) ; ::_thesis: ex f being FinSequence of FT st ( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) then ( x1 = x & x2 = x ) by TARSKI:def_1; hence ex f being FinSequence of FT st ( f is continuous & rng f c= {x} & f . 1 = x1 & f . (len f) = x2 ) by A2, A3, A1; ::_thesis: verum end; hence {x} is arcwise_connected by Def7; ::_thesis: verum end; registration let FT be non empty RelStr ; let x be Element of FT; cluster{x} -> arcwise_connected for Subset of FT; coherence for b1 being Subset of FT st b1 = {x} holds b1 is arcwise_connected by Lm3; end; theorem :: FINTOPO6:46 for FT being non empty RelStr for A being Subset of FT st FT is symmetric holds ( A is connected iff A is arcwise_connected ) proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st FT is symmetric holds ( A is connected iff A is arcwise_connected ) let A be Subset of FT; ::_thesis: ( FT is symmetric implies ( A is connected iff A is arcwise_connected ) ) assume A1: FT is symmetric ; ::_thesis: ( A is connected iff A is arcwise_connected ) now__::_thesis:_(_not_A_is_arcwise_connected_implies_not_A_is_connected_) assume not A is arcwise_connected ; ::_thesis: not A is connected then consider x1, x2 being Element of FT such that A2: x1 in A and A3: x2 in A and A4: for f being FinSequence of FT holds ( not f is continuous or not rng f c= A or not f . 1 = x1 or not f . (len f) = x2 ) by Def7; A5: { z where z is Element of FT : ( z in A & ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { z where z is Element of FT : ( z in A & ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } or x in A ) assume x in { z where z is Element of FT : ( z in A & ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } ; ::_thesis: x in A then ex z being Element of FT st ( x = z & z in A & ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) ; hence x in A ; ::_thesis: verum end; then reconsider G = { z where z is Element of FT : ( z in A & ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) } as Subset of FT by XBOOLE_1:1; A6: G misses A \ G by XBOOLE_1:79; A7: now__::_thesis:_not_G_^b_meets_A_\_G assume G ^b meets A \ G ; ::_thesis: contradiction then consider u being set such that A8: u in G ^b and A9: u in A \ G by XBOOLE_0:3; A10: not u in G by A9, XBOOLE_0:def_5; consider x being Element of FT such that A11: u = x and A12: U_FT x meets G by A8; consider y being set such that A13: y in U_FT x and A14: y in G by A12, XBOOLE_0:3; consider z2 being Element of FT such that A15: y = z2 and z2 in A and A16: ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z2 ) by A14; consider f being FinSequence of FT such that A17: f is continuous and A18: rng f c= A and A19: f . 1 = x1 and A20: f . (len f) = z2 by A16; reconsider g = f ^ <*x*> as FinSequence of FT ; A21: rng g = (rng f) \/ (rng <*x*>) by FINSEQ_1:31 .= (rng f) \/ {x} by FINSEQ_1:38 ; A22: u in A by A9, XBOOLE_0:def_5; then {x} c= A by A11, ZFMISC_1:31; then A23: rng g c= A by A18, A21, XBOOLE_1:8; 1 <= len f by A17, Def6; then 1 in dom f by FINSEQ_3:25; then A24: ( g . ((len f) + 1) = x & g . 1 = x1 ) by A19, FINSEQ_1:42, FINSEQ_1:def_7; x in U_FT z2 by A1, A13, A15, FIN_TOPO:def_13; then A25: g is continuous by A17, A20, Th44; len g = (len f) + (len <*x*>) by FINSEQ_1:22 .= (len f) + 1 by FINSEQ_1:39 ; hence contradiction by A22, A10, A11, A25, A24, A23; ::_thesis: verum end; A26: now__::_thesis:_not_G_=_{} {x1} c= A by A2, ZFMISC_1:31; then A27: rng <*x1*> c= A by FINSEQ_1:38; assume A28: G = {} ; ::_thesis: contradiction A29: <*x1*> . 1 = x1 by FINSEQ_1:40; then <*x1*> . (len <*x1*>) = x1 by FINSEQ_1:39; then x1 in G by A2, A27, A29; hence contradiction by A28; ::_thesis: verum end; A30: now__::_thesis:_not_A_\_G_=_{} assume A \ G = {} ; ::_thesis: contradiction then A c= G by XBOOLE_1:37; then G = A by A5, XBOOLE_0:def_10; then ex z being Element of FT st ( z = x2 & z in A & ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = z ) ) by A3; hence contradiction by A4; ::_thesis: verum end; A = G \/ (A \ G) by A5, XBOOLE_1:45; hence not A is connected by A30, A26, A6, A7, FIN_TOPO:def_16; ::_thesis: verum end; hence ( A is connected implies A is arcwise_connected ) ; ::_thesis: ( A is arcwise_connected implies A is connected ) now__::_thesis:_(_not_A_is_connected_implies_(_not_A_is_arcwise_connected_&_not_A_is_arcwise_connected_)_) assume not A is connected ; ::_thesis: ( not A is arcwise_connected & not A is arcwise_connected ) then consider P, Q being Subset of FT such that A31: A = P \/ Q and A32: P <> {} and A33: Q <> {} and A34: P misses Q and A35: P ^b misses Q by FIN_TOPO:def_16; set q0 = the Element of Q; the Element of Q in Q by A33; then reconsider q1 = the Element of Q as Element of FT ; set p0 = the Element of P; the Element of P in P by A32; then reconsider p1 = the Element of P as Element of FT ; A36: ( p1 in A & q1 in A ) by A31, A32, A33, XBOOLE_0:def_3; hereby ::_thesis: not A is arcwise_connected assume A is arcwise_connected ; ::_thesis: contradiction then consider f being FinSequence of FT such that A37: f is continuous and A38: rng f c= A and A39: f . 1 = p1 and A40: f . (len f) = q1 by A36, Def7; defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f & f . $1 in P ); len f >= 1 by A37, Def6; then A41: ex k being Nat st S1[k] by A32, A39; A42: for k being Nat st S1[k] holds k <= len f ; consider i0 being Nat such that A43: ( S1[i0] & ( for n being Nat st S1[n] holds n <= i0 ) ) from NAT_1:sch_6(A42, A41); i0 <> len f by A33, A34, A40, A43, XBOOLE_0:3; then A44: i0 < len f by A43, XXREAL_0:1; then A45: i0 + 1 <= len f by NAT_1:13; reconsider u0 = f . i0 as Element of FT by A43; A46: 1 < i0 + 1 by A43, NAT_1:13; then i0 + 1 in dom f by A45, FINSEQ_3:25; then A47: f . (i0 + 1) in rng f by FUNCT_1:def_3; then reconsider z0 = f . (i0 + 1) as Element of FT ; z0 in U_FT u0 by A37, A43, A44, Def6; then f . i0 in U_FT z0 by A1, FIN_TOPO:def_13; then U_FT z0 meets P by A43, XBOOLE_0:3; then A48: z0 in P ^b ; now__::_thesis:_not_f_._(i0_+_1)_in_P assume f . (i0 + 1) in P ; ::_thesis: contradiction then i0 + 1 <= i0 by A43, A45, A46; hence contradiction by NAT_1:13; ::_thesis: verum end; then f . (i0 + 1) in Q by A31, A38, A47, XBOOLE_0:def_3; hence contradiction by A35, A48, XBOOLE_0:3; ::_thesis: verum end; hence not A is arcwise_connected ; ::_thesis: verum end; hence ( A is arcwise_connected implies A is connected ) ; ::_thesis: verum end; theorem Th47: :: FINTOPO6:47 for FT being non empty RelStr for g being FinSequence of FT for k being Nat st g is continuous & 1 <= k holds g | k is continuous proof let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT for k being Nat st g is continuous & 1 <= k holds g | k is continuous let g be FinSequence of FT; ::_thesis: for k being Nat st g is continuous & 1 <= k holds g | k is continuous let k be Nat; ::_thesis: ( g is continuous & 1 <= k implies g | k is continuous ) assume that A1: g is continuous and A2: 1 <= k ; ::_thesis: g | k is continuous percases ( len g <= k or k <= len g ) ; suppose len g <= k ; ::_thesis: g | k is continuous hence g | k is continuous by A1, FINSEQ_1:58; ::_thesis: verum end; supposeA3: k <= len g ; ::_thesis: g | k is continuous hence len (g | k) >= 1 by A2, FINSEQ_1:59; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat for x1 being Element of FT st 1 <= i & i < len (g | k) & x1 = (g | k) . i holds (g | k) . (i + 1) in U_FT x1 let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len (g | k) & x1 = (g | k) . i holds (g | k) . (i + 1) in U_FT x1 let x11 be Element of FT; ::_thesis: ( 1 <= i & i < len (g | k) & x11 = (g | k) . i implies (g | k) . (i + 1) in U_FT x11 ) assume that A4: 1 <= i and A5: i < len (g | k) and A6: x11 = (g | k) . i ; ::_thesis: (g | k) . (i + 1) in U_FT x11 A7: len (g | k) = k by A3, FINSEQ_1:59; then A8: (g | k) . i = g . i by A5, FINSEQ_3:112; i + 1 <= k by A7, A5, NAT_1:13; then A9: (g | k) . (i + 1) = g . (i + 1) by FINSEQ_3:112; i < len g by A3, A7, A5, XXREAL_0:2; hence (g | k) . (i + 1) in U_FT x11 by A1, A4, A6, A8, A9, Def6; ::_thesis: verum end; end; end; theorem Th48: :: FINTOPO6:48 for FT being non empty RelStr for g being FinSequence of FT for k being Element of NAT st g is continuous & k < len g holds g /^ k is continuous proof let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT for k being Element of NAT st g is continuous & k < len g holds g /^ k is continuous let g be FinSequence of FT; ::_thesis: for k being Element of NAT st g is continuous & k < len g holds g /^ k is continuous let k be Element of NAT ; ::_thesis: ( g is continuous & k < len g implies g /^ k is continuous ) assume that A1: g is continuous and A2: k < len g ; ::_thesis: g /^ k is continuous A3: (len g) - k > 0 by A2, XREAL_1:50; then A4: (len g) - k = (len g) -' k by XREAL_0:def_2; A5: len (g /^ k) = (len g) - k by A2, RFINSEQ:def_1; A6: for i being Nat for x11 being Element of FT st 1 <= i & i < len (g /^ k) & x11 = (g /^ k) . i holds (g /^ k) . (i + 1) in U_FT x11 proof let i be Nat; ::_thesis: for x11 being Element of FT st 1 <= i & i < len (g /^ k) & x11 = (g /^ k) . i holds (g /^ k) . (i + 1) in U_FT x11 let x11 be Element of FT; ::_thesis: ( 1 <= i & i < len (g /^ k) & x11 = (g /^ k) . i implies (g /^ k) . (i + 1) in U_FT x11 ) assume that A7: 1 <= i and A8: i < len (g /^ k) and A9: x11 = (g /^ k) . i ; ::_thesis: (g /^ k) . (i + 1) in U_FT x11 A10: 1 <= 1 + i by NAT_1:11; i in dom (g /^ k) by A7, A8, FINSEQ_3:25; then A11: (g /^ k) . i = g . (i + k) by A2, RFINSEQ:def_1; i <= i + k by NAT_1:11; then A12: ( (i + 1) + k = (i + k) + 1 & 1 <= i + k ) by A7, XXREAL_0:2; i + 1 <= (len g) -' k by A5, A4, A8, NAT_1:13; then i + 1 in dom (g /^ k) by A5, A4, A10, FINSEQ_3:25; then A13: (g /^ k) . (i + 1) = g . ((i + 1) + k) by A2, RFINSEQ:def_1; i + k < ((len g) - k) + k by A5, A8, XREAL_1:6; hence (g /^ k) . (i + 1) in U_FT x11 by A1, A9, A11, A13, A12, Def6; ::_thesis: verum end; (len g) -' k >= 0 + 1 by A3, A4, NAT_1:13; hence g /^ k is continuous by A5, A4, A6, Def6; ::_thesis: verum end; definition let FT be non empty RelStr ; let g be FinSequence of FT; let A be Subset of FT; let x1, x2 be Element of FT; predg is_minimum_path_in A,x1,x2 means :Def8: :: FINTOPO6:def 8 ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ); end; :: deftheorem Def8 defines is_minimum_path_in FINTOPO6:def_8_:_ for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT holds ( g is_minimum_path_in A,x1,x2 iff ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) ); theorem :: FINTOPO6:49 for FT being non empty RelStr for A being Subset of FT for x being Element of FT st x in A holds <*x*> is_minimum_path_in A,x,x proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT for x being Element of FT st x in A holds <*x*> is_minimum_path_in A,x,x let A be Subset of FT; ::_thesis: for x being Element of FT st x in A holds <*x*> is_minimum_path_in A,x,x let x be Element of FT; ::_thesis: ( x in A implies <*x*> is_minimum_path_in A,x,x ) assume A1: x in A ; ::_thesis: <*x*> is_minimum_path_in A,x,x thus <*x*> is continuous ; :: according to FINTOPO6:def_8 ::_thesis: ( rng <*x*> c= A & <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds len <*x*> <= len h ) ) {x} c= A by A1, ZFMISC_1:31; hence rng <*x*> c= A by FINSEQ_1:38; ::_thesis: ( <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds len <*x*> <= len h ) ) len <*x*> = 1 by FINSEQ_1:40; hence ( <*x*> . 1 = x & <*x*> . (len <*x*>) = x & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x & h . (len h) = x holds len <*x*> <= len h ) ) by Def6, FINSEQ_1:40; ::_thesis: verum end; Lm4: for FT being non empty RelStr for f being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds ex g being FinSequence of FT st ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) proof let FT be non empty RelStr ; ::_thesis: for f being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds ex g being FinSequence of FT st ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) let f be FinSequence of FT; ::_thesis: for A being Subset of FT for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds ex g being FinSequence of FT st ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 holds ex g being FinSequence of FT st ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) let x1, x2 be Element of FT; ::_thesis: ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 implies ex g being FinSequence of FT st ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) ) defpred S1[ Nat] means ex g being FinSequence of FT st ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & $1 = len g ); assume ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ; ::_thesis: ex g being FinSequence of FT st ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) then A1: ex k being Nat st S1[k] ; ex k being Nat st ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A1); then consider k0 being Nat such that A2: S1[k0] and A3: for n being Nat st S1[n] holds k0 <= n ; consider g0 being FinSequence of FT such that A4: ( g0 is continuous & rng g0 c= A & g0 . 1 = x1 & g0 . (len g0) = x2 ) and A5: k0 = len g0 by A2; for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g0 <= len h by A3, A5; hence ex g being FinSequence of FT st ( g is continuous & rng g c= A & g . 1 = x1 & g . (len g) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h ) ) by A4; ::_thesis: verum end; theorem :: FINTOPO6:50 for FT being non empty RelStr for A being Subset of FT holds ( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds ( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) let A be Subset of FT; ::_thesis: ( A is arcwise_connected iff for x1, x2 being Element of FT st x1 in A & x2 in A holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) thus ( A is arcwise_connected implies for x1, x2 being Element of FT st x1 in A & x2 in A holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) ::_thesis: ( ( for x1, x2 being Element of FT st x1 in A & x2 in A holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) implies A is arcwise_connected ) proof assume A1: A is arcwise_connected ; ::_thesis: for x1, x2 being Element of FT st x1 in A & x2 in A holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 thus for x1, x2 being Element of FT st x1 in A & x2 in A holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ::_thesis: verum proof let x1, x2 be Element of FT; ::_thesis: ( x1 in A & x2 in A implies ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) assume ( x1 in A & x2 in A ) ; ::_thesis: ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 then ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) by A1, Def7; then consider g2 being FinSequence of FT such that A2: ( g2 is continuous & rng g2 c= A & g2 . 1 = x1 & g2 . (len g2) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g2 <= len h ) ) by Lm4; g2 is_minimum_path_in A,x1,x2 by A2, Def8; hence ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; ::_thesis: verum end; end; assume A3: for x1, x2 being Element of FT st x1 in A & x2 in A holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; ::_thesis: A is arcwise_connected for x1, x2 being Element of FT st x1 in A & x2 in A holds ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) proof let x1, x2 be Element of FT; ::_thesis: ( x1 in A & x2 in A implies ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ) assume ( x1 in A & x2 in A ) ; ::_thesis: ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) then consider g being FinSequence of FT such that A4: g is_minimum_path_in A,x1,x2 by A3; A5: ( g . 1 = x1 & g . (len g) = x2 ) by A4, Def8; ( g is continuous & rng g c= A ) by A4, Def8; hence ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) by A5; ::_thesis: verum end; hence A is arcwise_connected by Def7; ::_thesis: verum end; theorem :: FINTOPO6:51 for FT being non empty RelStr for A being Subset of FT for x1, x2 being Element of FT st ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT for x1, x2 being Element of FT st ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) holds ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 let x1, x2 be Element of FT; ::_thesis: ( ex f being FinSequence of FT st ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) implies ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ) given f being FinSequence of FT such that A1: ( f is continuous & rng f c= A & f . 1 = x1 & f . (len f) = x2 ) ; ::_thesis: ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 consider g2 being FinSequence of FT such that A2: ( g2 is continuous & rng g2 c= A & g2 . 1 = x1 & g2 . (len g2) = x2 & ( for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g2 <= len h ) ) by A1, Lm4; g2 is_minimum_path_in A,x1,x2 by A2, Def8; hence ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2 ; ::_thesis: verum end; theorem Th52: :: FINTOPO6:52 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) proof let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) let g be FinSequence of FT; ::_thesis: for A being Subset of FT for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) let x1, x2 be Element of FT; ::_thesis: for k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g holds ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) let k be Element of NAT ; ::_thesis: ( g is_minimum_path_in A,x1,x2 & 1 <= k & k <= len g implies ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) ) assume that A1: g is_minimum_path_in A,x1,x2 and A2: 1 <= k and A3: k <= len g ; ::_thesis: ( g | k is continuous & rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) A4: k in dom g by A2, A3, FINSEQ_3:25; g is continuous by A1, Def8; hence g | k is continuous by A2, Th47; ::_thesis: ( rng (g | k) c= A & (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) A5: rng (g | k) c= rng g by FINSEQ_5:19; rng g c= A by A1, Def8; hence rng (g | k) c= A by A5, XBOOLE_1:1; ::_thesis: ( (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) g . 1 = x1 by A1, Def8; hence (g | k) . 1 = x1 by A2, FINSEQ_3:112; ::_thesis: (g | k) . (len (g | k)) = g /. k len (g | k) = k by A3, FINSEQ_1:59; hence (g | k) . (len (g | k)) = g . k by FINSEQ_3:112 .= g /. k by A4, PARTFUN1:def_6 ; ::_thesis: verum end; theorem Th53: :: FINTOPO6:53 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) proof let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) let g be FinSequence of FT; ::_thesis: for A being Subset of FT for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) let x1, x2 be Element of FT; ::_thesis: for k being Element of NAT st g is_minimum_path_in A,x1,x2 & k < len g holds ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) let k be Element of NAT ; ::_thesis: ( g is_minimum_path_in A,x1,x2 & k < len g implies ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) ) assume that A1: g is_minimum_path_in A,x1,x2 and A2: k < len g ; ::_thesis: ( g /^ k is continuous & rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) A3: len (g /^ k) = (len g) - k by A2, RFINSEQ:def_1; g is continuous by A1, Def8; hence g /^ k is continuous by A2, Th48; ::_thesis: ( rng (g /^ k) c= A & (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) A4: rng (g /^ k) c= rng g by FINSEQ_5:33; rng g c= A by A1, Def8; hence rng (g /^ k) c= A by A4, XBOOLE_1:1; ::_thesis: ( (g /^ k) . 1 = g /. (1 + k) & (g /^ k) . (len (g /^ k)) = x2 ) A5: len (g /^ k) = (len g) - k by A2, RFINSEQ:def_1; ( 1 <= 1 + k & k + 1 <= len g ) by A2, NAT_1:11, NAT_1:13; then A6: 1 + k in dom g by FINSEQ_3:25; A7: (len g) - k > 0 by A2, XREAL_1:50; then (len g) -' k = (len g) - k by XREAL_0:def_2; then (len g) - k >= 0 + 1 by A7, NAT_1:13; then 1 in dom (g /^ k) by A5, FINSEQ_3:25; hence (g /^ k) . 1 = g . (1 + k) by A2, RFINSEQ:def_1 .= g /. (1 + k) by A6, PARTFUN1:def_6 ; ::_thesis: (g /^ k) . (len (g /^ k)) = x2 A8: (len g) - k > 0 by A2, XREAL_1:50; then A9: (len g) - k = (len g) -' k by XREAL_0:def_2; then (len g) -' k >= 0 + 1 by A8, NAT_1:13; then (len g) -' k in dom (g /^ k) by A5, A9, FINSEQ_3:25; hence (g /^ k) . (len (g /^ k)) = g . (((len g) -' k) + k) by A2, A9, A3, RFINSEQ:def_1 .= x2 by A1, A9, Def8 ; ::_thesis: verum end; theorem :: FINTOPO6:54 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds for k being Nat st 1 <= k & k <= len g holds g | k is_minimum_path_in A,x1,g /. k proof let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds for k being Nat st 1 <= k & k <= len g holds g | k is_minimum_path_in A,x1,g /. k let g be FinSequence of FT; ::_thesis: for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds for k being Nat st 1 <= k & k <= len g holds g | k is_minimum_path_in A,x1,g /. k let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds for k being Nat st 1 <= k & k <= len g holds g | k is_minimum_path_in A,x1,g /. k let x1, x2 be Element of FT; ::_thesis: ( g is_minimum_path_in A,x1,x2 implies for k being Nat st 1 <= k & k <= len g holds g | k is_minimum_path_in A,x1,g /. k ) assume A1: g is_minimum_path_in A,x1,x2 ; ::_thesis: for k being Nat st 1 <= k & k <= len g holds g | k is_minimum_path_in A,x1,g /. k then A2: rng g c= A by Def8; A3: g is continuous by A1, Def8; then A4: 1 <= len g by Def6; A5: g . (len g) = x2 by A1, Def8; let k be Nat; ::_thesis: ( 1 <= k & k <= len g implies g | k is_minimum_path_in A,x1,g /. k ) assume that A6: 1 <= k and A7: k <= len g ; ::_thesis: g | k is_minimum_path_in A,x1,g /. k reconsider k = k as Element of NAT by ORDINAL1:def_12; A8: ( (g | k) . 1 = x1 & (g | k) . (len (g | k)) = g /. k ) by A1, A6, A7, Th52; A9: ( g | k is continuous & rng (g | k) c= A ) by A1, A6, A7, Th52; now__::_thesis:_g_|_k_is_minimum_path_in_A,x1,g_/._k percases ( k < len g or k = len g ) by A7, XXREAL_0:1; supposeA10: k < len g ; ::_thesis: g | k is_minimum_path_in A,x1,g /. k now__::_thesis:_g_|_k_is_minimum_path_in_A,x1,g_/._k k in dom g by A6, A7, FINSEQ_3:25; then A11: g /. k = g . k by PARTFUN1:def_6; k + 1 <= len g by A10, NAT_1:13; then A12: (g /^ k) . 1 = g . (k + 1) by FINSEQ_6:114; rng (g /^ k) c= rng g by FINSEQ_5:33; then A13: rng (g /^ k) c= A by A2, XBOOLE_1:1; assume not g | k is_minimum_path_in A,x1,g /. k ; ::_thesis: contradiction then consider h being FinSequence of FT such that A14: h is continuous and A15: rng h c= A and A16: h . 1 = x1 and A17: h . (len h) = g /. k and A18: len (g | k) > len h by A9, A8, Def8; reconsider s = h ^ (g /^ k) as FinSequence of FT ; A19: len s = (len h) + (len (g /^ k)) by FINSEQ_1:22; rng s = (rng h) \/ (rng (g /^ k)) by FINSEQ_1:31; then A20: rng s c= A by A15, A13, XBOOLE_1:8; A21: g /^ k is continuous by A1, A10, Th53; then 1 <= len (g /^ k) by Def6; then len (g /^ k) in dom (g /^ k) by FINSEQ_3:25; then A22: s . (len s) = (g /^ k) . (len (g /^ k)) by A19, FINSEQ_1:def_7 .= x2 by A5, A10, JORDAN4:6 ; A23: 1 <= len h by A14, Def6; then 1 in dom h by FINSEQ_3:25; then A24: s . 1 = x1 by A16, FINSEQ_1:def_7; len h in dom h by A23, FINSEQ_3:25; then h . (len h) = h /. (len h) by PARTFUN1:def_6; then (g /^ k) . 1 in U_FT (h /. (len h)) by A3, A6, A10, A17, A12, A11, Def6; then A25: s is continuous by A14, A21, Th45; g = (g | k) ^ (g /^ k) by RFINSEQ:8; then len g = (len (g | k)) + (len (g /^ k)) by FINSEQ_1:22; then len s < len g by A18, A19, XREAL_1:8; hence contradiction by A1, A25, A20, A24, A22, Def8; ::_thesis: verum end; hence g | k is_minimum_path_in A,x1,g /. k ; ::_thesis: verum end; supposeA26: k = len g ; ::_thesis: g | k is_minimum_path_in A,x1,g /. k A27: len g in dom g by A4, FINSEQ_3:25; g | k = g by A26, FINSEQ_1:58; hence g | k is_minimum_path_in A,x1,g /. k by A1, A5, A26, A27, PARTFUN1:def_6; ::_thesis: verum end; end; end; hence g | k is_minimum_path_in A,x1,g /. k ; ::_thesis: verum end; theorem :: FINTOPO6:55 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds g is one-to-one proof let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds g is one-to-one let g be FinSequence of FT; ::_thesis: for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds g is one-to-one let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 holds g is one-to-one let x1, x2 be Element of FT; ::_thesis: ( g is_minimum_path_in A,x1,x2 implies g is one-to-one ) assume A1: g is_minimum_path_in A,x1,x2 ; ::_thesis: g is one-to-one then A2: g is continuous by Def8; A3: for h being FinSequence of FT st h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = x2 holds len g <= len h by A1, Def8; A4: rng g c= A by A1, Def8; A5: g . 1 = x1 by A1, Def8; A6: g . (len g) = x2 by A1, Def8; assume not g is one-to-one ; ::_thesis: contradiction then consider y1, y2 being set such that A7: y1 in dom g and A8: y2 in dom g and A9: g . y1 = g . y2 and A10: y1 <> y2 by FUNCT_1:def_4; reconsider n1 = y1, n2 = y2 as Element of NAT by A7, A8; A11: dom g = Seg (len g) by FINSEQ_1:def_3; then A12: 1 <= n1 by A7, FINSEQ_1:1; A13: n2 <= len g by A8, A11, FINSEQ_1:1; A14: 1 <= n2 by A8, A11, FINSEQ_1:1; A15: n1 <= len g by A7, A11, FINSEQ_1:1; percases ( n1 > n2 or n2 > n1 ) by A10, XXREAL_0:1; supposeA16: n1 > n2 ; ::_thesis: contradiction set k = (len g) -' n1; set g2 = (g | n2) ^ (g /^ n1); A17: len (g /^ n1) = (len g) - n1 by A15, RFINSEQ:def_1; A18: (len g) - n1 >= 0 by A15, XREAL_1:48; then A19: (len g) -' n1 = (len g) - n1 by XREAL_0:def_2; A20: len (g | n2) = n2 by A13, FINSEQ_1:59; then A21: ((g | n2) ^ (g /^ n1)) . 1 = (g | n2) . 1 by A14, FINSEQ_1:64 .= g . 1 by A14, FINSEQ_3:112 ; A22: len ((g | n2) ^ (g /^ n1)) = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22 .= n2 + ((len g) - n1) by A15, A20, RFINSEQ:def_1 ; percases ( n1 < len g or n1 = len g ) by A15, XXREAL_0:1; suppose n1 < len g ; ::_thesis: contradiction then n1 + 1 <= len g by NAT_1:13; then A23: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13; then A24: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7; A25: (g | n2) ^ (g /^ n1) is continuous proof thus len ((g | n2) ^ (g /^ n1)) >= 1 by A22, A24; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1 let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1 let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & z1 = ((g | n2) ^ (g /^ n1)) . i implies ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 ) assume that A26: 1 <= i and A27: i < len ((g | n2) ^ (g /^ n1)) and A28: z1 = ((g | n2) ^ (g /^ n1)) . i ; ::_thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 A29: i + 1 <= len ((g | n2) ^ (g /^ n1)) by A27, NAT_1:13; reconsider i = i as Element of NAT by ORDINAL1:def_12; 1 < i + 1 by A26, NAT_1:13; then i + 1 in dom ((g | n2) ^ (g /^ n1)) by A29, FINSEQ_3:25; then ((g | n2) ^ (g /^ n1)) . (i + 1) = ((g | n2) ^ (g /^ n1)) /. (i + 1) by PARTFUN1:def_6; then reconsider z2 = ((g | n2) ^ (g /^ n1)) . (i + 1) as Element of FT ; now__::_thesis:_z2_in_U_FT_z1 percases ( i < n2 or i >= n2 ) ; supposeA30: i < n2 ; ::_thesis: z2 in U_FT z1 then A31: i + 1 <= n2 by NAT_1:13; i + 1 <= len (g | n2) by A20, A30, NAT_1:13; then A32: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12 .= g . (i + 1) by A31, FINSEQ_3:112 ; A33: i < len g by A13, A30, XXREAL_0:2; z1 = (g | n2) . i by A20, A26, A28, A30, FINSEQ_1:64 .= g . i by A30, FINSEQ_3:112 ; hence z2 in U_FT z1 by A2, A26, A33, A32, Def6; ::_thesis: verum end; supposeA34: i >= n2 ; ::_thesis: z2 in U_FT z1 i - n2 < (n2 + ((len g) - n1)) - n2 by A22, A27, XREAL_1:9; then A35: i -' n2 < (len g) - n1 by A34, XREAL_1:233; then A36: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6; A37: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A20, A34, XREAL_1:233 .= i ; A38: now__::_thesis:_z1_=_g_._((i_-'_n2)_+_n1) percases ( i > n2 or i = n2 ) by A34, XXREAL_0:1; suppose i > n2 ; ::_thesis: z1 = g . ((i -' n2) + n1) then A39: i - n2 > 0 by XREAL_1:50; then i -' n2 = i - n2 by XREAL_0:def_2; then A40: 0 + 1 <= i -' n2 by A39, NAT_1:13; then A41: i -' n2 in dom (g /^ n1) by A17, A35, FINSEQ_3:25; thus z1 = (g /^ n1) . (i -' n2) by A17, A28, A35, A37, A40, FINSEQ_1:65 .= g . ((i -' n2) + n1) by A15, A41, RFINSEQ:def_1 ; ::_thesis: verum end; supposeA42: i = n2 ; ::_thesis: z1 = g . ((i -' n2) + n1) hence z1 = (g | n2) . n2 by A20, A26, A28, FINSEQ_1:64 .= g . (0 + n1) by A9, FINSEQ_3:112 .= g . ((i -' n2) + n1) by A42, XREAL_1:232 ; ::_thesis: verum end; end; end; i -' n2 < (len g) -' n1 by A15, A35, XREAL_1:233; then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13; then A43: (i -' n2) + 1 <= len (g /^ n1) by A15, A17, XREAL_1:233; 1 <= (i -' n2) + 1 by NAT_1:12; then A44: (i -' n2) + 1 in dom (g /^ n1) by A43, FINSEQ_3:25; (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A20, A34, XREAL_1:233 .= i + 1 ; then A45: z2 = (g /^ n1) . ((i -' n2) + 1) by A43, FINSEQ_1:65, NAT_1:12 .= g . (((i -' n2) + 1) + n1) by A15, A44, RFINSEQ:def_1 .= g . (((i -' n2) + n1) + 1) ; 1 <= (i -' n2) + n1 by A12, NAT_1:12; hence z2 in U_FT z1 by A2, A38, A45, A36, Def6; ::_thesis: verum end; end; end; hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 ; ::_thesis: verum end; A46: rng (g /^ n1) c= rng g by FINSEQ_5:33; ( rng ((g | n2) ^ (g /^ n1)) = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19; then A47: rng ((g | n2) ^ (g /^ n1)) c= rng g by A46, XBOOLE_1:8; A48: ((len g) -' n1) + n1 = len g by A19; A49: (len g) -' n1 in dom (g /^ n1) by A19, A17, A23, FINSEQ_3:25; then ((g | n2) ^ (g /^ n1)) . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def_7 .= x2 by A6, A15, A49, A48, RFINSEQ:def_1 ; then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by A20, A22, A18, XREAL_0:def_2; then len g <= len ((g | n2) ^ (g /^ n1)) by A4, A5, A3, A21, A47, A25, XBOOLE_1:1; then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A22, XREAL_1:13; hence contradiction by A16, XREAL_1:10; ::_thesis: verum end; supposeA50: n1 = len g ; ::_thesis: contradiction A51: len (g /^ n1) = (len g) - n1 by A15, RFINSEQ:def_1; A52: (g | n2) ^ (g /^ n1) is continuous proof thus 1 <= len ((g | n2) ^ (g /^ n1)) by A8, A11, A22, A50, FINSEQ_1:1; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1 let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & x1 = ((g | n2) ^ (g /^ n1)) . i holds ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT x1 let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len ((g | n2) ^ (g /^ n1)) & z1 = ((g | n2) ^ (g /^ n1)) . i implies ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 ) assume that A53: 1 <= i and A54: i < len ((g | n2) ^ (g /^ n1)) and A55: z1 = ((g | n2) ^ (g /^ n1)) . i ; ::_thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 A56: i + 1 <= len ((g | n2) ^ (g /^ n1)) by A54, NAT_1:13; reconsider i = i as Element of NAT by ORDINAL1:def_12; 1 < i + 1 by A53, NAT_1:13; then i + 1 in dom ((g | n2) ^ (g /^ n1)) by A56, FINSEQ_3:25; then ((g | n2) ^ (g /^ n1)) . (i + 1) = ((g | n2) ^ (g /^ n1)) /. (i + 1) by PARTFUN1:def_6; then reconsider z2 = ((g | n2) ^ (g /^ n1)) . (i + 1) as Element of FT ; percases ( i < n2 or i >= n2 ) ; supposeA57: i < n2 ; ::_thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 then A58: i + 1 <= n2 by NAT_1:13; i + 1 <= len (g | n2) by A20, A57, NAT_1:13; then A59: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12 .= g . (i + 1) by A58, FINSEQ_3:112 ; A60: i < len g by A13, A57, XXREAL_0:2; z1 = (g | n2) . i by A20, A53, A55, A57, FINSEQ_1:64 .= g . i by A57, FINSEQ_3:112 ; hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A53, A60, A59, Def6; ::_thesis: verum end; supposeA61: i >= n2 ; ::_thesis: ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 i - n2 < (n2 + ((len g) - n1)) - n2 by A22, A54, XREAL_1:9; then A62: i -' n2 < (len g) - n1 by A61, XREAL_1:233; then A63: (i -' n2) + n1 < ((len g) - n1) + n1 by XREAL_1:6; A64: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A20, A61, XREAL_1:233 .= i ; A65: now__::_thesis:_z1_=_g_._((i_-'_n2)_+_n1) percases ( i > n2 or i = n2 ) by A61, XXREAL_0:1; suppose i > n2 ; ::_thesis: z1 = g . ((i -' n2) + n1) then A66: i - n2 > 0 by XREAL_1:50; then i -' n2 = i - n2 by XREAL_0:def_2; then A67: 0 + 1 <= i -' n2 by A66, NAT_1:13; then A68: i -' n2 in dom (g /^ n1) by A51, A62, FINSEQ_3:25; thus z1 = (g /^ n1) . (i -' n2) by A51, A55, A62, A64, A67, FINSEQ_1:65 .= g . ((i -' n2) + n1) by A15, A68, RFINSEQ:def_1 ; ::_thesis: verum end; supposeA69: i = n2 ; ::_thesis: z1 = g . ((i -' n2) + n1) hence z1 = (g | n2) . n2 by A20, A53, A55, FINSEQ_1:64 .= g . (0 + n1) by A9, FINSEQ_3:112 .= g . ((i -' n2) + n1) by A69, XREAL_1:232 ; ::_thesis: verum end; end; end; i -' n2 < (len g) -' n1 by A15, A62, XREAL_1:233; then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13; then A70: (i -' n2) + 1 <= len (g /^ n1) by A15, A51, XREAL_1:233; 1 <= (i -' n2) + 1 by NAT_1:12; then A71: (i -' n2) + 1 in dom (g /^ n1) by A70, FINSEQ_3:25; (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A20, A61, XREAL_1:233 .= i + 1 ; then A72: z2 = (g /^ n1) . ((i -' n2) + 1) by A70, FINSEQ_1:65, NAT_1:12 .= g . (((i -' n2) + 1) + n1) by A15, A71, RFINSEQ:def_1 .= g . (((i -' n2) + n1) + 1) ; 1 <= (i -' n2) + n1 by A12, NAT_1:12; hence ((g | n2) ^ (g /^ n1)) . (i + 1) in U_FT z1 by A2, A65, A72, A63, Def6; ::_thesis: verum end; end; end; A73: rng (g | n2) c= rng g by FINSEQ_5:19; A74: (g | n2) ^ (g /^ n1) = (g | n2) ^ {} by A50, REVROT_1:2 .= g | n2 by FINSEQ_1:34 ; then ((g | n2) ^ (g /^ n1)) . (len ((g | n2) ^ (g /^ n1))) = x2 by A6, A9, A20, A50, FINSEQ_3:112; then len g <= len ((g | n2) ^ (g /^ n1)) by A4, A5, A3, A21, A74, A73, A52, XBOOLE_1:1; then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A22, XREAL_1:13; hence contradiction by A16, XREAL_1:10; ::_thesis: verum end; end; end; supposeA75: n2 > n1 ; ::_thesis: contradiction set k = (len g) -' n2; set g2 = (g | n1) ^ (g /^ n2); A76: len (g /^ n2) = (len g) - n2 by A13, RFINSEQ:def_1; (len g) - n2 >= 0 by A13, XREAL_1:48; then A77: (len g) -' n2 = (len g) - n2 by XREAL_0:def_2; A78: len (g | n1) = n1 by A15, FINSEQ_1:59; then A79: ((g | n1) ^ (g /^ n2)) . 1 = (g | n1) . 1 by A12, FINSEQ_1:64 .= x1 by A5, A12, FINSEQ_3:112 ; A80: len ((g | n1) ^ (g /^ n2)) = (len (g | n1)) + (len (g /^ n2)) by FINSEQ_1:22 .= n1 + ((len g) - n2) by A13, A78, RFINSEQ:def_1 ; percases ( n2 < len g or n2 = len g ) by A13, XXREAL_0:1; suppose n2 < len g ; ::_thesis: contradiction then n2 + 1 <= len g by NAT_1:13; then A81: (n2 + 1) - n2 <= (len g) - n2 by XREAL_1:13; then A82: 0 + 1 <= n1 + ((len g) - n2) by XREAL_1:7; A83: (g | n1) ^ (g /^ n2) is continuous proof thus len ((g | n1) ^ (g /^ n2)) >= 1 by A80, A82; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1 let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1 let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & z1 = ((g | n1) ^ (g /^ n2)) . i implies ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 ) assume that A84: 1 <= i and A85: i < len ((g | n1) ^ (g /^ n2)) and A86: z1 = ((g | n1) ^ (g /^ n2)) . i ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 A87: i + 1 <= len ((g | n1) ^ (g /^ n2)) by A85, NAT_1:13; reconsider i = i as Element of NAT by ORDINAL1:def_12; 1 < i + 1 by A84, NAT_1:13; then i + 1 in dom ((g | n1) ^ (g /^ n2)) by A87, FINSEQ_3:25; then ((g | n1) ^ (g /^ n2)) . (i + 1) = ((g | n1) ^ (g /^ n2)) /. (i + 1) by PARTFUN1:def_6; then reconsider z2 = ((g | n1) ^ (g /^ n2)) . (i + 1) as Element of FT ; percases ( i < n1 or i >= n1 ) ; supposeA88: i < n1 ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 then A89: i + 1 <= n1 by NAT_1:13; i + 1 <= len (g | n1) by A78, A88, NAT_1:13; then A90: z2 = (g | n1) . (i + 1) by FINSEQ_1:64, NAT_1:12 .= g . (i + 1) by A89, FINSEQ_3:112 ; A91: i < len g by A15, A88, XXREAL_0:2; z1 = (g | n1) . i by A78, A84, A86, A88, FINSEQ_1:64 .= g . i by A88, FINSEQ_3:112 ; hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A84, A91, A90, Def6; ::_thesis: verum end; supposeA92: i >= n1 ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 i - n1 < (n1 + ((len g) - n2)) - n1 by A80, A85, XREAL_1:9; then A93: i -' n1 < (len g) - n2 by A92, XREAL_1:233; then A94: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6; A95: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by A78, A92, XREAL_1:233 .= i ; A96: now__::_thesis:_z1_=_g_._((i_-'_n1)_+_n2) percases ( i > n1 or i = n1 ) by A92, XXREAL_0:1; suppose i > n1 ; ::_thesis: z1 = g . ((i -' n1) + n2) then A97: i - n1 > 0 by XREAL_1:50; then i -' n1 = i - n1 by XREAL_0:def_2; then A98: 0 + 1 <= i -' n1 by A97, NAT_1:13; then A99: i -' n1 in dom (g /^ n2) by A76, A93, FINSEQ_3:25; thus z1 = (g /^ n2) . (i -' n1) by A76, A86, A93, A95, A98, FINSEQ_1:65 .= g . ((i -' n1) + n2) by A13, A99, RFINSEQ:def_1 ; ::_thesis: verum end; supposeA100: i = n1 ; ::_thesis: z1 = g . ((i -' n1) + n2) hence z1 = (g | n1) . n1 by A78, A84, A86, FINSEQ_1:64 .= g . (0 + n2) by A9, FINSEQ_3:112 .= g . ((i -' n1) + n2) by A100, XREAL_1:232 ; ::_thesis: verum end; end; end; i -' n1 < (len g) -' n2 by A13, A93, XREAL_1:233; then (i -' n1) + 1 <= (len g) -' n2 by NAT_1:13; then A101: (i -' n1) + 1 <= len (g /^ n2) by A13, A76, XREAL_1:233; 1 <= (i -' n1) + 1 by NAT_1:12; then A102: (i -' n1) + 1 in dom (g /^ n2) by A101, FINSEQ_3:25; (len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by A78, A92, XREAL_1:233 .= i + 1 ; then A103: z2 = (g /^ n2) . ((i -' n1) + 1) by A101, FINSEQ_1:65, NAT_1:12 .= g . (((i -' n1) + 1) + n2) by A13, A102, RFINSEQ:def_1 .= g . (((i -' n1) + n2) + 1) ; 1 <= (i -' n1) + n2 by A14, NAT_1:12; hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A96, A103, A94, Def6; ::_thesis: verum end; end; end; A104: rng (g /^ n2) c= rng g by FINSEQ_5:33; ( rng ((g | n1) ^ (g /^ n2)) = (rng (g | n1)) \/ (rng (g /^ n2)) & rng (g | n1) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19; then rng ((g | n1) ^ (g /^ n2)) c= rng g by A104, XBOOLE_1:8; then A105: rng ((g | n1) ^ (g /^ n2)) c= A by A4, XBOOLE_1:1; A106: ((len g) -' n2) + n2 = len g by A77; A107: (len g) -' n2 in dom (g /^ n2) by A77, A76, A81, FINSEQ_3:25; then ((g | n1) ^ (g /^ n2)) . ((len (g | n1)) + ((len g) -' n2)) = (g /^ n2) . ((len g) -' n2) by FINSEQ_1:def_7 .= x2 by A6, A13, A107, A106, RFINSEQ:def_1 ; then ((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by A15, A80, A77, FINSEQ_1:59; then len g <= len ((g | n1) ^ (g /^ n2)) by A1, A79, A105, A83, Def8; then (len g) - n1 <= (n1 + ((len g) - n2)) - n1 by A80, XREAL_1:13; hence contradiction by A75, XREAL_1:10; ::_thesis: verum end; supposeA108: n2 = len g ; ::_thesis: contradiction A109: len (g /^ n2) = (len g) - n2 by A13, RFINSEQ:def_1; A110: (g | n1) ^ (g /^ n2) is continuous proof thus len ((g | n1) ^ (g /^ n2)) >= 1 by A7, A11, A80, A108, FINSEQ_1:1; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1 let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & x1 = ((g | n1) ^ (g /^ n2)) . i holds ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT x1 let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len ((g | n1) ^ (g /^ n2)) & z1 = ((g | n1) ^ (g /^ n2)) . i implies ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 ) assume that A111: 1 <= i and A112: i < len ((g | n1) ^ (g /^ n2)) and A113: z1 = ((g | n1) ^ (g /^ n2)) . i ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 A114: i + 1 <= len ((g | n1) ^ (g /^ n2)) by A112, NAT_1:13; reconsider i = i as Element of NAT by ORDINAL1:def_12; 1 < i + 1 by A111, NAT_1:13; then i + 1 in dom ((g | n1) ^ (g /^ n2)) by A114, FINSEQ_3:25; then ((g | n1) ^ (g /^ n2)) . (i + 1) = ((g | n1) ^ (g /^ n2)) /. (i + 1) by PARTFUN1:def_6; then reconsider z2 = ((g | n1) ^ (g /^ n2)) . (i + 1) as Element of FT ; percases ( i < n1 or i >= n1 ) ; supposeA115: i < n1 ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 then A116: i + 1 <= n1 by NAT_1:13; i + 1 <= len (g | n1) by A78, A115, NAT_1:13; then A117: z2 = (g | n1) . (i + 1) by FINSEQ_1:64, NAT_1:12 .= g . (i + 1) by A116, FINSEQ_3:112 ; A118: i < len g by A15, A115, XXREAL_0:2; z1 = (g | n1) . i by A78, A111, A113, A115, FINSEQ_1:64 .= g . i by A115, FINSEQ_3:112 ; hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A111, A118, A117, Def6; ::_thesis: verum end; supposeA119: i >= n1 ; ::_thesis: ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 i - n1 < (n1 + ((len g) - n2)) - n1 by A80, A112, XREAL_1:9; then A120: i -' n1 < (len g) - n2 by A119, XREAL_1:233; then A121: (i -' n1) + n2 < ((len g) - n2) + n2 by XREAL_1:6; A122: (len (g | n1)) + (i -' n1) = n1 + (i - n1) by A78, A119, XREAL_1:233 .= i ; A123: now__::_thesis:_z1_=_g_._((i_-'_n1)_+_n2) percases ( i > n1 or i = n1 ) by A119, XXREAL_0:1; suppose i > n1 ; ::_thesis: z1 = g . ((i -' n1) + n2) then A124: i - n1 > 0 by XREAL_1:50; then i -' n1 = i - n1 by XREAL_0:def_2; then A125: 0 + 1 <= i -' n1 by A124, NAT_1:13; then A126: i -' n1 in dom (g /^ n2) by A109, A120, FINSEQ_3:25; thus z1 = (g /^ n2) . (i -' n1) by A109, A113, A120, A122, A125, FINSEQ_1:65 .= g . ((i -' n1) + n2) by A13, A126, RFINSEQ:def_1 ; ::_thesis: verum end; supposeA127: i = n1 ; ::_thesis: z1 = g . ((i -' n1) + n2) hence z1 = (g | n1) . n1 by A78, A111, A113, FINSEQ_1:64 .= g . (0 + n2) by A9, FINSEQ_3:112 .= g . ((i -' n1) + n2) by A127, XREAL_1:232 ; ::_thesis: verum end; end; end; i -' n1 < (len g) -' n2 by A13, A120, XREAL_1:233; then (i -' n1) + 1 <= (len g) -' n2 by NAT_1:13; then A128: (i -' n1) + 1 <= len (g /^ n2) by A13, A109, XREAL_1:233; 1 <= (i -' n1) + 1 by NAT_1:12; then A129: (i -' n1) + 1 in dom (g /^ n2) by A128, FINSEQ_3:25; (len (g | n1)) + ((i -' n1) + 1) = ((i - n1) + 1) + n1 by A78, A119, XREAL_1:233 .= i + 1 ; then A130: z2 = (g /^ n2) . ((i -' n1) + 1) by A128, FINSEQ_1:65, NAT_1:12 .= g . (((i -' n1) + 1) + n2) by A13, A129, RFINSEQ:def_1 .= g . (((i -' n1) + n2) + 1) ; 1 <= (i -' n1) + n2 by A14, NAT_1:12; hence ((g | n1) ^ (g /^ n2)) . (i + 1) in U_FT z1 by A2, A123, A130, A121, Def6; ::_thesis: verum end; end; end; A131: (g | n1) ^ (g /^ n2) = (g | n1) ^ {} by A108, REVROT_1:2 .= g | n1 by FINSEQ_1:34 ; rng (g | n1) c= rng g by FINSEQ_5:19; then A132: rng ((g | n1) ^ (g /^ n2)) c= A by A4, A131, XBOOLE_1:1; ((g | n1) ^ (g /^ n2)) . (len ((g | n1) ^ (g /^ n2))) = x2 by A6, A9, A78, A108, A131, FINSEQ_3:112; then len g <= len ((g | n1) ^ (g /^ n2)) by A1, A79, A132, A110, Def8; then (len g) - n1 <= (n1 + ((len g) - n2)) - n1 by A80, XREAL_1:13; hence contradiction by A75, XREAL_1:10; ::_thesis: verum end; end; end; end; end; definition let FT be non empty RelStr ; let f be FinSequence of FT; attrf is inv_continuous means :Def9: :: FINTOPO6:def 9 ( 1 <= len f & ( for i, j being Nat for y being Element of FT st 1 <= i & i <= len f & 1 <= j & j <= len f & y = f . i & i <> j & f . j in U_FT y & not i = j + 1 holds j = i + 1 ) ); end; :: deftheorem Def9 defines inv_continuous FINTOPO6:def_9_:_ for FT being non empty RelStr for f being FinSequence of FT holds ( f is inv_continuous iff ( 1 <= len f & ( for i, j being Nat for y being Element of FT st 1 <= i & i <= len f & 1 <= j & j <= len f & y = f . i & i <> j & f . j in U_FT y & not i = j + 1 holds j = i + 1 ) ) ); theorem Th56: :: FINTOPO6:56 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds g is inv_continuous proof let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds g is inv_continuous let g be FinSequence of FT; ::_thesis: for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds g is inv_continuous let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds g is inv_continuous let x1, x2 be Element of FT; ::_thesis: ( g is_minimum_path_in A,x1,x2 & FT is symmetric implies g is inv_continuous ) assume that A1: g is_minimum_path_in A,x1,x2 and A2: FT is symmetric ; ::_thesis: g is inv_continuous A3: g . 1 = x1 by A1, Def8; A4: g . (len g) = x2 by A1, Def8; A5: g is continuous by A1, Def8; hence 1 <= len g by Def6; :: according to FINTOPO6:def_9 ::_thesis: for i, j being Nat for y being Element of FT st 1 <= i & i <= len g & 1 <= j & j <= len g & y = g . i & i <> j & g . j in U_FT y & not i = j + 1 holds j = i + 1 let i2, j2 be Nat; ::_thesis: for y being Element of FT st 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 holds j2 = i2 + 1 let y be Element of FT; ::_thesis: ( 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 implies j2 = i2 + 1 ) assume that A6: 1 <= i2 and A7: i2 <= len g and A8: 1 <= j2 and A9: j2 <= len g and A10: y = g . i2 and A11: i2 <> j2 and A12: g . j2 in U_FT y ; ::_thesis: ( i2 = j2 + 1 or j2 = i2 + 1 ) A13: rng g c= A by A1, Def8; hereby ::_thesis: verum assume that A14: i2 <> j2 + 1 and A15: j2 <> i2 + 1 ; ::_thesis: contradiction percases ( i2 < j2 or j2 < i2 ) by A11, XXREAL_0:1; supposeA16: i2 < j2 ; ::_thesis: contradiction set n1 = j2 -' 1; set n2 = i2; reconsider n1 = j2 -' 1, n2 = i2 as Element of NAT by ORDINAL1:def_12; i2 + 1 <= j2 by A16, NAT_1:13; then i2 + 1 < j2 by A15, XXREAL_0:1; then i2 < j2 - 1 by XREAL_1:20; then A17: n1 > n2 by A8, XREAL_1:233; 1 < j2 by A6, A16, XXREAL_0:2; then 1 + 1 <= j2 by NAT_1:13; then 1 <= j2 - 1 by XREAL_1:19; then A18: 1 <= n1 by A8, XREAL_1:233; set k = (len g) -' n1; reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ; A19: len (g | n2) = n2 by A7, FINSEQ_1:59; A20: j2 -' 1 <= j2 by NAT_D:35; then A21: n1 <= len g by A9, XXREAL_0:2; then A22: len (g /^ n1) = (len g) - n1 by RFINSEQ:def_1; A23: (len g) - n1 >= 0 by A21, XREAL_1:48; then A24: (len g) -' n1 = (len g) - n1 by XREAL_0:def_2; A25: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22 .= n2 + ((len g) - n1) by A21, A19, RFINSEQ:def_1 ; A26: g2 . 1 = (g | n2) . 1 by A6, A19, FINSEQ_1:64 .= x1 by A3, A6, FINSEQ_3:112 ; now__::_thesis:_contradiction percases ( n1 < len g or n1 = len g ) by A21, XXREAL_0:1; suppose n1 < len g ; ::_thesis: contradiction then n1 + 1 <= len g by NAT_1:13; then A27: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13; then A28: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7; A29: g2 is continuous proof thus len g2 >= 1 by A25, A28; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds g2 . (i + 1) in U_FT x1 let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds g2 . (i + 1) in U_FT x1 let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 ) assume that A30: 1 <= i and A31: i < len g2 and A32: z1 = g2 . i ; ::_thesis: g2 . (i + 1) in U_FT z1 A33: i + 1 <= len g2 by A31, NAT_1:13; reconsider i = i as Element of NAT by ORDINAL1:def_12; 1 < i + 1 by A30, NAT_1:13; then i + 1 in dom g2 by A33, FINSEQ_3:25; then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def_6; then reconsider z2 = g2 . (i + 1) as Element of FT ; percases ( i < n2 or i >= n2 ) ; supposeA34: i < n2 ; ::_thesis: g2 . (i + 1) in U_FT z1 then A35: i + 1 <= n2 by NAT_1:13; i + 1 <= len (g | n2) by A19, A34, NAT_1:13; then A36: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12 .= g . (i + 1) by A35, FINSEQ_3:112 ; A37: i < len g by A7, A34, XXREAL_0:2; z1 = (g | n2) . i by A19, A30, A32, A34, FINSEQ_1:64 .= g . i by A34, FINSEQ_3:112 ; hence g2 . (i + 1) in U_FT z1 by A5, A30, A37, A36, Def6; ::_thesis: verum end; supposeA38: i >= n2 ; ::_thesis: g2 . (i + 1) in U_FT z1 i - n2 < (n2 + ((len g) - n1)) - n2 by A25, A31, XREAL_1:9; then A39: i -' n2 < (len g) - n1 by A38, XREAL_1:233; then i -' n2 < (len g) -' n1 by A9, A20, XREAL_1:233, XXREAL_0:2; then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13; then A40: (i -' n2) + 1 <= len (g /^ n1) by A9, A20, A22, XREAL_1:233, XXREAL_0:2; A41: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A19, A38, XREAL_1:233 .= i ; A42: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A19, A38, XREAL_1:233 .= i + 1 ; 1 <= (i -' n2) + 1 by NAT_1:12; then A43: (i -' n2) + 1 in dom (g /^ n1) by A40, FINSEQ_3:25; percases ( i > n2 or i = n2 ) by A38, XXREAL_0:1; suppose i > n2 ; ::_thesis: g2 . (i + 1) in U_FT z1 then A44: i - n2 > 0 by XREAL_1:50; then i -' n2 = i - n2 by XREAL_0:def_2; then A45: 0 + 1 <= i -' n2 by A44, NAT_1:13; then A46: i -' n2 in dom (g /^ n1) by A22, A39, FINSEQ_3:25; A47: z2 = (g /^ n1) . ((i -' n2) + 1) by A40, A42, FINSEQ_1:65, NAT_1:12 .= g . (((i -' n2) + 1) + n1) by A21, A43, RFINSEQ:def_1 .= g . (((i -' n2) + n1) + 1) ; A48: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by A18, A39, NAT_1:12, XREAL_1:6; z1 = (g /^ n1) . (i -' n2) by A22, A32, A39, A41, A45, FINSEQ_1:65 .= g . ((i -' n2) + n1) by A21, A46, RFINSEQ:def_1 ; hence g2 . (i + 1) in U_FT z1 by A5, A47, A48, Def6; ::_thesis: verum end; supposeA49: i = n2 ; ::_thesis: g2 . (i + 1) in U_FT z1 then A50: z1 = (g | n2) . n2 by A19, A30, A32, FINSEQ_1:64 .= y by A10, FINSEQ_3:112 ; z2 = (g /^ n1) . ((i -' n2) + 1) by A40, A42, FINSEQ_1:65, NAT_1:12 .= g . (((i -' n2) + 1) + n1) by A21, A43, RFINSEQ:def_1 .= g . (((i -' n2) + n1) + 1) .= g . ((0 + (j2 -' 1)) + 1) by A49, XREAL_1:232 .= g . ((j2 - 1) + 1) by A8, XREAL_1:233 ; hence g2 . (i + 1) in U_FT z1 by A12, A50; ::_thesis: verum end; end; end; end; end; A51: rng (g /^ n1) c= rng g by FINSEQ_5:33; ( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19; then rng g2 c= rng g by A51, XBOOLE_1:8; then A52: rng g2 c= A by A13, XBOOLE_1:1; A53: ((len g) -' n1) + n1 = len g by A24; A54: (len g) -' n1 in dom (g /^ n1) by A24, A22, A27, FINSEQ_3:25; then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def_7 .= x2 by A4, A21, A54, A53, RFINSEQ:def_1 ; then g2 . (len g2) = x2 by A19, A25, A23, XREAL_0:def_2; then len g <= len g2 by A1, A26, A52, A29, Def8; then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A25, XREAL_1:13; hence contradiction by A17, XREAL_1:10; ::_thesis: verum end; suppose n1 = len g ; ::_thesis: contradiction then j2 - 1 = len g by A8, XREAL_1:233; then j2 = (len g) + 1 ; hence contradiction by A9, NAT_1:13; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA55: j2 < i2 ; ::_thesis: contradiction reconsider n1 = i2 -' 1, n2 = j2 as Element of NAT by ORDINAL1:def_12; j2 + 1 <= i2 by A55, NAT_1:13; then j2 + 1 < i2 by A14, XXREAL_0:1; then j2 < i2 - 1 by XREAL_1:20; then A56: n1 > n2 by A6, XREAL_1:233; 1 < i2 by A8, A55, XXREAL_0:2; then 1 + 1 <= i2 by NAT_1:13; then 1 <= i2 - 1 by XREAL_1:19; then A57: 1 <= n1 by A6, XREAL_1:233; set k = (len g) -' n1; reconsider g2 = (g | n2) ^ (g /^ n1) as FinSequence of FT ; A58: len (g | n2) = n2 by A9, FINSEQ_1:59; A59: i2 -' 1 <= i2 by NAT_D:35; then A60: n1 <= len g by A7, XXREAL_0:2; then A61: len (g /^ n1) = (len g) - n1 by RFINSEQ:def_1; A62: (len g) - n1 >= 0 by A60, XREAL_1:48; then A63: (len g) -' n1 = (len g) - n1 by XREAL_0:def_2; A64: len g2 = (len (g | n2)) + (len (g /^ n1)) by FINSEQ_1:22 .= n2 + ((len g) - n1) by A60, A58, RFINSEQ:def_1 ; A65: g2 . 1 = (g | n2) . 1 by A8, A58, FINSEQ_1:64 .= x1 by A3, A8, FINSEQ_3:112 ; now__::_thesis:_contradiction percases ( n1 < len g or n1 = len g ) by A60, XXREAL_0:1; suppose n1 < len g ; ::_thesis: contradiction then n1 + 1 <= len g by NAT_1:13; then A66: (n1 + 1) - n1 <= (len g) - n1 by XREAL_1:13; then A67: 0 + 1 <= n2 + ((len g) - n1) by XREAL_1:7; A68: g2 is continuous proof thus len g2 >= 1 by A64, A67; :: according to FINTOPO6:def_6 ::_thesis: for i being Nat for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds g2 . (i + 1) in U_FT x1 let i be Nat; ::_thesis: for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds g2 . (i + 1) in U_FT x1 let z1 be Element of FT; ::_thesis: ( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 ) assume that A69: 1 <= i and A70: i < len g2 and A71: z1 = g2 . i ; ::_thesis: g2 . (i + 1) in U_FT z1 A72: i + 1 <= len g2 by A70, NAT_1:13; reconsider i = i as Element of NAT by ORDINAL1:def_12; 1 < i + 1 by A69, NAT_1:13; then i + 1 in dom g2 by A72, FINSEQ_3:25; then g2 . (i + 1) = g2 /. (i + 1) by PARTFUN1:def_6; then reconsider z2 = g2 . (i + 1) as Element of FT ; percases ( i < n2 or i >= n2 ) ; supposeA73: i < n2 ; ::_thesis: g2 . (i + 1) in U_FT z1 then A74: i + 1 <= n2 by NAT_1:13; i + 1 <= len (g | n2) by A58, A73, NAT_1:13; then A75: z2 = (g | n2) . (i + 1) by FINSEQ_1:64, NAT_1:12 .= g . (i + 1) by A74, FINSEQ_3:112 ; A76: i < len g by A9, A73, XXREAL_0:2; z1 = (g | n2) . i by A58, A69, A71, A73, FINSEQ_1:64 .= g . i by A73, FINSEQ_3:112 ; hence g2 . (i + 1) in U_FT z1 by A5, A69, A76, A75, Def6; ::_thesis: verum end; supposeA77: i >= n2 ; ::_thesis: g2 . (i + 1) in U_FT z1 i - n2 < (n2 + ((len g) - n1)) - n2 by A64, A70, XREAL_1:9; then A78: i -' n2 < (len g) - n1 by A77, XREAL_1:233; then i -' n2 < (len g) -' n1 by A7, A59, XREAL_1:233, XXREAL_0:2; then (i -' n2) + 1 <= (len g) -' n1 by NAT_1:13; then A79: (i -' n2) + 1 <= len (g /^ n1) by A7, A59, A61, XREAL_1:233, XXREAL_0:2; A80: (len (g | n2)) + (i -' n2) = n2 + (i - n2) by A58, A77, XREAL_1:233 .= i ; A81: (len (g | n2)) + ((i -' n2) + 1) = ((i - n2) + 1) + n2 by A58, A77, XREAL_1:233 .= i + 1 ; 1 <= (i -' n2) + 1 by NAT_1:12; then A82: (i -' n2) + 1 in dom (g /^ n1) by A79, FINSEQ_3:25; percases ( i > n2 or i = n2 ) by A77, XXREAL_0:1; suppose i > n2 ; ::_thesis: g2 . (i + 1) in U_FT z1 then A83: i - n2 > 0 by XREAL_1:50; then i -' n2 = i - n2 by XREAL_0:def_2; then A84: 0 + 1 <= i -' n2 by A83, NAT_1:13; then A85: i -' n2 in dom (g /^ n1) by A61, A78, FINSEQ_3:25; A86: z2 = (g /^ n1) . ((i -' n2) + 1) by A79, A81, FINSEQ_1:65, NAT_1:12 .= g . (((i -' n2) + 1) + n1) by A60, A82, RFINSEQ:def_1 .= g . (((i -' n2) + n1) + 1) ; A87: ( 1 <= (i -' n2) + n1 & (i -' n2) + n1 < ((len g) - n1) + n1 ) by A57, A78, NAT_1:12, XREAL_1:6; z1 = (g /^ n1) . (i -' n2) by A61, A71, A78, A80, A84, FINSEQ_1:65 .= g . ((i -' n2) + n1) by A60, A85, RFINSEQ:def_1 ; hence g2 . (i + 1) in U_FT z1 by A5, A86, A87, Def6; ::_thesis: verum end; supposeA88: i = n2 ; ::_thesis: g2 . (i + 1) in U_FT z1 then A89: z1 = (g | n2) . n2 by A58, A69, A71, FINSEQ_1:64 .= g . j2 by FINSEQ_3:112 ; z2 = (g /^ n1) . ((i -' n2) + 1) by A79, A81, FINSEQ_1:65, NAT_1:12 .= g . (((i -' n2) + 1) + n1) by A60, A82, RFINSEQ:def_1 .= g . (((i -' n2) + n1) + 1) .= g . ((0 + (i2 -' 1)) + 1) by A88, XREAL_1:232 .= g . ((i2 - 1) + 1) by A6, XREAL_1:233 .= y by A10 ; hence g2 . (i + 1) in U_FT z1 by A2, A12, A89, FIN_TOPO:def_13; ::_thesis: verum end; end; end; end; end; A90: rng (g /^ n1) c= rng g by FINSEQ_5:33; ( rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) & rng (g | n2) c= rng g ) by FINSEQ_1:31, FINSEQ_5:19; then rng g2 c= rng g by A90, XBOOLE_1:8; then A91: rng g2 c= A by A13, XBOOLE_1:1; A92: ((len g) -' n1) + n1 = len g by A63; A93: (len g) -' n1 in dom (g /^ n1) by A63, A61, A66, FINSEQ_3:25; then g2 . ((len (g | n2)) + ((len g) -' n1)) = (g /^ n1) . ((len g) -' n1) by FINSEQ_1:def_7 .= x2 by A4, A60, A93, A92, RFINSEQ:def_1 ; then g2 . (len g2) = x2 by A58, A64, A62, XREAL_0:def_2; then len g <= len g2 by A1, A65, A91, A68, Def8; then (len g) - n2 <= (n2 + ((len g) - n1)) - n2 by A64, XREAL_1:13; hence contradiction by A56, XREAL_1:10; ::_thesis: verum end; suppose n1 = len g ; ::_thesis: contradiction then i2 - 1 = len g by A6, XREAL_1:233; then i2 = (len g) + 1 ; hence contradiction by A7, NAT_1:13; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; end; theorem :: FINTOPO6:57 for FT being non empty RelStr for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds ( ( for i being Nat st 1 < i & i < len g holds (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) proof let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds ( ( for i being Nat st 1 < i & i < len g holds (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) let g be FinSequence of FT; ::_thesis: for A being Subset of FT for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds ( ( for i being Nat st 1 < i & i < len g holds (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) let A be Subset of FT; ::_thesis: for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 holds ( ( for i being Nat st 1 < i & i < len g holds (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) let x1, x2 be Element of FT; ::_thesis: ( g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & x1 <> x2 implies ( ( for i being Nat st 1 < i & i < len g holds (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) ) assume that A1: g is_minimum_path_in A,x1,x2 and A2: ( FT is filled & FT is symmetric ) and A3: x1 <> x2 ; ::_thesis: ( ( for i being Nat st 1 < i & i < len g holds (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) & (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) A4: dom g = Seg (len g) by FINSEQ_1:def_3; A5: g is continuous by A1, Def8; then A6: 1 <= len g by Def6; then A7: len g in dom g by A4; then A8: g . (len g) = g /. (len g) by PARTFUN1:def_6; A9: g is inv_continuous by A1, A2, Th56; then A10: 1 <= len g by Def9; thus for i being Nat st 1 < i & i < len g holds (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ::_thesis: ( (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} & (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ) proof let i be Nat; ::_thesis: ( 1 < i & i < len g implies (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ) assume that A11: 1 < i and A12: i < len g ; ::_thesis: (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} A13: i in Seg (len g) by A11, A12, FINSEQ_1:1; ( 1 < i + 1 & i + 1 <= len g ) by A11, A12, NAT_1:13; then A14: i + 1 in Seg (len g) ; i -' 1 <= i by NAT_D:35; then A15: i -' 1 < len g by A12, XXREAL_0:2; 1 + 1 <= i by A11, NAT_1:13; then A16: 1 <= i - 1 by XREAL_1:19; then 1 <= i -' 1 by A11, XREAL_1:233; then A17: i -' 1 in Seg (len g) by A15; A18: (i -' 1) + 1 = (i - 1) + 1 by A11, XREAL_1:233 .= i ; thus (rng g) /\ (U_FT (g /. i)) = {(g . (i -' 1)),(g . i),(g . (i + 1))} ::_thesis: verum proof thus (rng g) /\ (U_FT (g /. i)) c= {(g . (i -' 1)),(g . i),(g . (i + 1))} :: according to XBOOLE_0:def_10 ::_thesis: {(g . (i -' 1)),(g . i),(g . (i + 1))} c= (rng g) /\ (U_FT (g /. i)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng g) /\ (U_FT (g /. i)) or x in {(g . (i -' 1)),(g . i),(g . (i + 1))} ) assume A19: x in (rng g) /\ (U_FT (g /. i)) ; ::_thesis: x in {(g . (i -' 1)),(g . i),(g . (i + 1))} then A20: x in U_FT (g /. i) by XBOOLE_0:def_4; x in rng g by A19, XBOOLE_0:def_4; then consider nx being set such that A21: nx in dom g and A22: x = g . nx by FUNCT_1:def_3; reconsider j = nx as Element of NAT by A21; ( i = j + 1 implies i - 1 = j ) ; then A23: ( i = j + 1 implies i -' 1 = j ) by A11, XREAL_1:233; A24: g /. i = g . i by A4, A13, PARTFUN1:def_6; ( 1 <= j & j <= len g ) by A4, A21, FINSEQ_1:1; then ( j = i or i = j + 1 or j = i + 1 ) by A9, A11, A12, A20, A22, A24, Def9; hence x in {(g . (i -' 1)),(g . i),(g . (i + 1))} by A22, A23, ENUMSET1:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g . (i -' 1)),(g . i),(g . (i + 1))} or x in (rng g) /\ (U_FT (g /. i)) ) A25: g . i = g /. i by A4, A13, PARTFUN1:def_6; A26: g . (i -' 1) = g /. (i -' 1) by A4, A17, PARTFUN1:def_6; assume A27: x in {(g . (i -' 1)),(g . i),(g . (i + 1))} ; ::_thesis: x in (rng g) /\ (U_FT (g /. i)) percases ( x = g . (i -' 1) or x = g . i or x = g . (i + 1) ) by A27, ENUMSET1:def_1; supposeA28: x = g . (i -' 1) ; ::_thesis: x in (rng g) /\ (U_FT (g /. i)) g . i in U_FT (g /. (i -' 1)) by A5, A16, A15, A18, A26, Def6; then A29: x in U_FT (g /. i) by A2, A25, A26, A28, FIN_TOPO:def_13; x in rng g by A4, A17, A28, FUNCT_1:def_3; hence x in (rng g) /\ (U_FT (g /. i)) by A29, XBOOLE_0:def_4; ::_thesis: verum end; suppose x = g . i ; ::_thesis: x in (rng g) /\ (U_FT (g /. i)) then ( x in rng g & x in U_FT (g /. i) ) by A2, A4, A13, A25, FIN_TOPO:def_4, FUNCT_1:def_3; hence x in (rng g) /\ (U_FT (g /. i)) by XBOOLE_0:def_4; ::_thesis: verum end; suppose x = g . (i + 1) ; ::_thesis: x in (rng g) /\ (U_FT (g /. i)) then ( x in rng g & x in U_FT (g /. i) ) by A5, A4, A11, A12, A14, A25, Def6, FUNCT_1:def_3; hence x in (rng g) /\ (U_FT (g /. i)) by XBOOLE_0:def_4; ::_thesis: verum end; end; end; end; ( g . 1 = x1 & g . (len g) = x2 ) by A1, Def8; then A30: 1 < len g by A3, A6, XXREAL_0:1; then A31: 1 + 1 <= len g by NAT_1:13; then A32: (1 + 1) - 1 <= (len g) - 1 by XREAL_1:13; A33: 1 in dom g by A10, FINSEQ_3:25; then A34: g . 1 = g /. 1 by PARTFUN1:def_6; thus (rng g) /\ (U_FT (g /. 1)) = {(g . 1),(g . 2)} ::_thesis: (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} proof thus (rng g) /\ (U_FT (g /. 1)) c= {(g . 1),(g . 2)} :: according to XBOOLE_0:def_10 ::_thesis: {(g . 1),(g . 2)} c= (rng g) /\ (U_FT (g /. 1)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng g) /\ (U_FT (g /. 1)) or x in {(g . 1),(g . 2)} ) assume A35: x in (rng g) /\ (U_FT (g /. 1)) ; ::_thesis: x in {(g . 1),(g . 2)} then A36: x in U_FT (g /. 1) by XBOOLE_0:def_4; x in rng g by A35, XBOOLE_0:def_4; then consider y being set such that A37: y in dom g and A38: x = g . y by FUNCT_1:def_3; reconsider j = y as Element of NAT by A37; A39: 1 <= j by A4, A37, FINSEQ_1:1; j <= len g by A4, A37, FINSEQ_1:1; then ( 1 + 1 = j or 1 = j or j + 1 = 1 ) by A9, A10, A34, A36, A38, A39, Def9; then ( 1 + 1 = j or 1 = j ) by A39, XREAL_1:7; hence x in {(g . 1),(g . 2)} by A38, TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g . 1),(g . 2)} or x in (rng g) /\ (U_FT (g /. 1)) ) 2 in dom g by A31, A4; then A40: ( x = g . 2 implies x in rng g ) by FUNCT_1:def_3; assume A41: x in {(g . 1),(g . 2)} ; ::_thesis: x in (rng g) /\ (U_FT (g /. 1)) A42: now__::_thesis:_(_(_x_=_g_._1_&_x_in_U_FT_(g_/._1)_)_or_(_x_=_g_._2_&_x_in_U_FT_(g_/._1)_)_) percases ( x = g . 1 or x = g . 2 ) by A41, TARSKI:def_2; case x = g . 1 ; ::_thesis: x in U_FT (g /. 1) hence x in U_FT (g /. 1) by A2, A34, FIN_TOPO:def_4; ::_thesis: verum end; caseA43: x = g . 2 ; ::_thesis: x in U_FT (g /. 1) then reconsider xx = x as Element of FT by A40; xx = g . (1 + 1) by A43; hence x in U_FT (g /. 1) by A5, A30, A34, Def6; ::_thesis: verum end; end; end; ( x = g . 1 implies x in rng g ) by A33, FUNCT_1:def_3; hence x in (rng g) /\ (U_FT (g /. 1)) by A40, A42, XBOOLE_0:def_4; ::_thesis: verum end; len g < (len g) + 1 by NAT_1:13; then A44: (len g) - 1 < ((len g) + 1) - 1 by XREAL_1:14; then A45: (len g) -' 1 < len g by A10, XREAL_1:233; A46: (len g) -' 1 = (len g) - 1 by A10, XREAL_1:233; then A47: (len g) -' 1 in dom g by A32, A44, FINSEQ_3:25; then A48: g . ((len g) -' 1) = g /. ((len g) -' 1) by PARTFUN1:def_6; A49: 1 <= (len g) -' 1 by A10, A32, XREAL_1:233; thus (rng g) /\ (U_FT (g /. (len g))) = {(g . ((len g) -' 1)),(g . (len g))} ::_thesis: verum proof thus (rng g) /\ (U_FT (g /. (len g))) c= {(g . ((len g) -' 1)),(g . (len g))} :: according to XBOOLE_0:def_10 ::_thesis: {(g . ((len g) -' 1)),(g . (len g))} c= (rng g) /\ (U_FT (g /. (len g))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (rng g) /\ (U_FT (g /. (len g))) or x in {(g . ((len g) -' 1)),(g . (len g))} ) assume A50: x in (rng g) /\ (U_FT (g /. (len g))) ; ::_thesis: x in {(g . ((len g) -' 1)),(g . (len g))} then A51: x in U_FT (g /. (len g)) by XBOOLE_0:def_4; x in rng g by A50, XBOOLE_0:def_4; then consider y being set such that A52: y in dom g and A53: x = g . y by FUNCT_1:def_3; reconsider ny = y as Element of NAT by A52; A54: ny <= len g by A4, A52, FINSEQ_1:1; 1 <= ny by A4, A52, FINSEQ_1:1; then ( ny + 1 = len g or (len g) + 1 = ny or len g = ny ) by A9, A10, A8, A51, A53, A54, Def9; then ( ny = (len g) - 1 or len g = ny ) by A54, NAT_1:13; then ( x = g . ((len g) -' 1) or x = g . (len g) ) by A6, A53, XREAL_1:233; hence x in {(g . ((len g) -' 1)),(g . (len g))} by TARSKI:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(g . ((len g) -' 1)),(g . (len g))} or x in (rng g) /\ (U_FT (g /. (len g))) ) A55: g . (len g) in U_FT (g /. (len g)) by A2, A8, FIN_TOPO:def_4; g . (((len g) -' 1) + 1) in U_FT (g /. ((len g) -' 1)) by A5, A49, A45, A48, Def6; then A56: g . ((len g) -' 1) in U_FT (g /. (len g)) by A2, A8, A46, A48, FIN_TOPO:def_13; assume x in {(g . ((len g) -' 1)),(g . (len g))} ; ::_thesis: x in (rng g) /\ (U_FT (g /. (len g))) then A57: ( x = g . ((len g) -' 1) or x = g . (len g) ) by TARSKI:def_2; then x in rng g by A7, A47, FUNCT_1:def_3; hence x in (rng g) /\ (U_FT (g /. (len g))) by A57, A55, A56, XBOOLE_0:def_4; ::_thesis: verum end; end; theorem :: FINTOPO6:58 for FT being non empty RelStr for g being FinSequence of FT for A being non empty Subset of FT for x1, x2 being Element of FT for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds for i being Element of NAT st i < len g holds ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) proof let FT be non empty RelStr ; ::_thesis: for g being FinSequence of FT for A being non empty Subset of FT for x1, x2 being Element of FT for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds for i being Element of NAT st i < len g holds ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) let g be FinSequence of FT; ::_thesis: for A being non empty Subset of FT for x1, x2 being Element of FT for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds for i being Element of NAT st i < len g holds ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) let A be non empty Subset of FT; ::_thesis: for x1, x2 being Element of FT for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds for i being Element of NAT st i < len g holds ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) let x1, x2 be Element of FT; ::_thesis: for B0 being Subset of (FT | A) st g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} holds for i being Element of NAT st i < len g holds ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) let B0 be Subset of (FT | A); ::_thesis: ( g is_minimum_path_in A,x1,x2 & FT is filled & FT is symmetric & B0 = {x1} implies for i being Element of NAT st i < len g holds ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) ) assume that A1: g is_minimum_path_in A,x1,x2 and A2: ( FT is filled & FT is symmetric ) and A3: B0 = {x1} ; ::_thesis: for i being Element of NAT st i < len g holds ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) A4: rng g c= A by A1, Def8; defpred S1[ Nat] means ( $1 + 1 <= len g implies ( g . ($1 + 1) in Finf (B0,$1) & ( $1 >= 1 implies not g . ($1 + 1) in Finf (B0,($1 -' 1)) ) ) ); defpred S2[ Element of NAT ] means for y being Element of FT st y in Finf (B0,$1) holds ex h being FinSequence of FT st ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= $1 + 1 ); A5: [#] (FT | A) = A by Def3; A6: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A7: S2[k] ; ::_thesis: S2[k + 1] for y being Element of FT st y in Finf (B0,(k + 1)) holds ex h being FinSequence of FT st ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 ) proof let y be Element of FT; ::_thesis: ( y in Finf (B0,(k + 1)) implies ex h being FinSequence of FT st ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 ) ) A8: Finf (B0,(k + 1)) = (Finf (B0,k)) ^f by FINTOPO3:31; assume y in Finf (B0,(k + 1)) ; ::_thesis: ex h being FinSequence of FT st ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 ) then consider x being Element of (FT | A) such that A9: x = y and A10: ex y2 being Element of (FT | A) st ( y2 in Finf (B0,k) & x in U_FT y2 ) by A8; A11: [#] (FT | A) = A by Def3; then A12: {y} c= A by A9, ZFMISC_1:31; consider y2 being Element of (FT | A) such that A13: y2 in Finf (B0,k) and A14: x in U_FT y2 by A10; y2 in the carrier of (FT | A) ; then reconsider y3 = y2 as Element of FT by A11; consider h2 being FinSequence of FT such that A15: h2 is continuous and A16: rng h2 c= A and A17: h2 . 1 = x1 and A18: h2 . (len h2) = y3 and A19: len h2 <= k + 1 by A7, A13; U_FT y2 = (U_FT y3) /\ A by A11, Def2; then A20: y in U_FT y3 by A9, A14, XBOOLE_0:def_4; reconsider h3 = h2 ^ <*y*> as FinSequence of FT ; ( rng (h2 ^ <*y*>) = (rng h2) \/ (rng <*y*>) & rng <*y*> = {y} ) by FINSEQ_1:31, FINSEQ_1:39; then A21: rng h3 c= A by A16, A12, XBOOLE_1:8; 1 <= len h2 by A15, Def6; then 1 in dom h2 by FINSEQ_3:25; then A22: h3 . 1 = x1 by A17, FINSEQ_1:def_7; len <*y*> = 1 by FINSEQ_1:40; then A23: len h3 = (len h2) + 1 by FINSEQ_1:22; then A24: h3 . (len h3) = y by FINSEQ_1:42; len h3 <= (k + 1) + 1 by A19, A23, XREAL_1:6; hence ex h being FinSequence of FT st ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= (k + 1) + 1 ) by A15, A18, A20, A21, A22, A24, Th44; ::_thesis: verum end; hence S2[k + 1] ; ::_thesis: verum end; A25: g . 1 = x1 by A1, Def8; then A26: g . 1 in {x1} by TARSKI:def_1; A27: g . (len g) = x2 by A1, Def8; A28: g is continuous by A1, Def8; then 1 <= len g by Def6; then 1 in dom g by FINSEQ_3:25; then x1 in rng g by A25, FUNCT_1:def_3; then A29: {x1} c= A by A4, ZFMISC_1:31; for y being Element of FT st y in Finf (B0,0) holds ex h being FinSequence of FT st ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= 0 + 1 ) proof let y be Element of FT; ::_thesis: ( y in Finf (B0,0) implies ex h being FinSequence of FT st ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= 0 + 1 ) ) A30: len <*x1*> = 1 by FINSEQ_1:40; assume y in Finf (B0,0) ; ::_thesis: ex h being FinSequence of FT st ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= 0 + 1 ) then y in {x1} by A3, FINTOPO3:32; then A31: y = x1 by TARSKI:def_1; ( rng <*x1*> = {x1} & <*x1*> . 1 = x1 ) by FINSEQ_1:39, FINSEQ_1:40; hence ex h being FinSequence of FT st ( h is continuous & rng h c= A & h . 1 = x1 & h . (len h) = y & len h <= 0 + 1 ) by A29, A31, A30; ::_thesis: verum end; then A32: S2[ 0 ] ; A33: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A32, A6); A34: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A35: S1[k] ; ::_thesis: S1[k + 1] percases ( (k + 1) + 1 > len g or (k + 1) + 1 <= len g ) ; suppose (k + 1) + 1 > len g ; ::_thesis: S1[k + 1] hence S1[k + 1] ; ::_thesis: verum end; supposeA36: (k + 1) + 1 <= len g ; ::_thesis: S1[k + 1] A37: 1 <= k + 1 by NAT_1:12; then 1 < (k + 1) + 1 by NAT_1:13; then (k + 1) + 1 in dom g by A36, FINSEQ_3:25; then A38: g . ((k + 1) + 1) in rng g by FUNCT_1:def_3; reconsider y0 = g . (k + 1) as Element of (FT | A) by A35, A36, NAT_1:13; A39: k + 1 < len g by A36, NAT_1:13; then k + 1 in dom g by A37, FINSEQ_3:25; then A40: g . (k + 1) = g /. (k + 1) by PARTFUN1:def_6; 1 < (k + 1) + 1 by A37, NAT_1:13; then A41: (k + 1) + 1 in dom g by A36, FINSEQ_3:25; A42: now__::_thesis:_not_g_._((k_+_1)_+_1)_in_Finf_(B0,k) assume A43: g . ((k + 1) + 1) in Finf (B0,k) ; ::_thesis: contradiction now__::_thesis:_g_._((k_+_1)_+_1)_in_(Finf_(B0,(k_-'_1)))_^f percases ( k = 0 or k > 0 ) ; supposeA44: k = 0 ; ::_thesis: g . ((k + 1) + 1) in (Finf (B0,(k -' 1))) ^f then k - 1 < 0 ; then k -' 1 = 0 by XREAL_0:def_2; then Finf (B0,k) c= (Finf (B0,(k -' 1))) ^f by A2, A44, FINTOPO3:1; hence g . ((k + 1) + 1) in (Finf (B0,(k -' 1))) ^f by A43; ::_thesis: verum end; suppose k > 0 ; ::_thesis: g . ((k + 1) + 1) in (Finf (B0,(k -' 1))) ^f then k >= 0 + 1 by NAT_1:13; then k = (k -' 1) + 1 by XREAL_1:235; hence g . ((k + 1) + 1) in (Finf (B0,(k -' 1))) ^f by A43, FINTOPO3:31; ::_thesis: verum end; end; end; then consider x being Element of (FT | A) such that A45: g . ((k + 1) + 1) = x and ex y being Element of (FT | A) st ( y in Finf (B0,(k -' 1)) & x in U_FT y ) ; x in A by A5; then reconsider x3 = x as Element of FT ; consider h being FinSequence of FT such that A46: h is continuous and A47: rng h c= A and A48: h . 1 = x1 and A49: h . (len h) = x3 and A50: len h <= k + 1 by A33, A43, A45; reconsider s = h ^ (g /^ ((k + 1) + 1)) as FinSequence of FT ; A51: len s = (len h) + (len (g /^ ((k + 1) + 1))) by FINSEQ_1:22; g = (g | ((k + 1) + 1)) ^ (g /^ ((k + 1) + 1)) by RFINSEQ:8; then A52: len g = (len (g | ((k + 1) + 1))) + (len (g /^ ((k + 1) + 1))) by FINSEQ_1:22; A53: 1 <= len h by A46, Def6; then len h in dom h by FINSEQ_3:25; then A54: h . (len h) = h /. (len h) by PARTFUN1:def_6; len (g | ((k + 1) + 1)) = (k + 1) + 1 by A36, FINSEQ_1:59; then A55: len (g | ((k + 1) + 1)) > len h by A50, NAT_1:13; then A56: len s < len g by A51, A52, XREAL_1:8; percases ( (k + 1) + 1 < len g or (k + 1) + 1 >= len g ) ; supposeA57: (k + 1) + 1 < len g ; ::_thesis: contradiction then len g >= 1 + ((k + 1) + 1) by NAT_1:13; then 1 <= (len g) - ((k + 1) + 1) by XREAL_1:19; then 1 <= len (g /^ ((k + 1) + 1)) by A57, RFINSEQ:def_1; then A58: 1 in dom (g /^ ((k + 1) + 1)) by FINSEQ_3:25; A59: g . ((k + 1) + 1) = g /. ((k + 1) + 1) by A41, PARTFUN1:def_6; A60: g /^ ((k + 1) + 1) is continuous by A28, A57, Th48; then 1 <= len (g /^ ((k + 1) + 1)) by Def6; then len (g /^ ((k + 1) + 1)) in dom (g /^ ((k + 1) + 1)) by FINSEQ_3:25; then A61: s . (len s) = (g /^ ((k + 1) + 1)) . (len (g /^ ((k + 1) + 1))) by A51, FINSEQ_1:def_7 .= x2 by A27, A57, JORDAN4:6 ; 1 <= (k + 1) + 1 by NAT_1:12; then g . (((k + 1) + 1) + 1) in U_FT (g /. ((k + 1) + 1)) by A28, A57, A59, Def6; then (g /^ ((k + 1) + 1)) . 1 in U_FT (h /. (len h)) by A45, A49, A54, A57, A59, A58, RFINSEQ:def_1; then A62: s is continuous by A46, A60, Th45; 1 in dom h by A53, FINSEQ_3:25; then A63: s . 1 = x1 by A48, FINSEQ_1:def_7; rng (g /^ ((k + 1) + 1)) c= rng g by FINSEQ_5:33; then A64: rng (g /^ ((k + 1) + 1)) c= A by A4, XBOOLE_1:1; rng s = (rng h) \/ (rng (g /^ ((k + 1) + 1))) by FINSEQ_1:31; then rng s c= A by A47, A64, XBOOLE_1:8; hence contradiction by A1, A56, A62, A63, A61, Def8; ::_thesis: verum end; supposeA65: (k + 1) + 1 >= len g ; ::_thesis: contradiction then g /^ ((k + 1) + 1) = <*> the carrier of FT by FINSEQ_5:32; then A66: s = h by FINSEQ_1:34; (k + 1) + 1 = len g by A36, A65, XXREAL_0:1; hence contradiction by A1, A27, A45, A46, A47, A48, A49, A55, A51, A52, A66, Def8; ::_thesis: verum end; end; end; [#] (FT | A) = A by Def3; then A67: U_FT y0 = (U_FT (g /. (k + 1))) /\ A by A40, Def2; g . ((k + 1) + 1) in U_FT (g /. (k + 1)) by A28, A39, A37, A40, Def6; then g . ((k + 1) + 1) in U_FT y0 by A4, A67, A38, XBOOLE_0:def_4; then A68: g . ((k + 1) + 1) in (Finf (B0,k)) ^f by A35, A36, NAT_1:13; (k + 1) -' 1 = (k + 1) - 1 by NAT_D:37 .= k ; hence S1[k + 1] by A68, A42, FINTOPO3:31; ::_thesis: verum end; end; end; let i be Element of NAT ; ::_thesis: ( i < len g implies ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) ) assume i < len g ; ::_thesis: ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) then A69: i + 1 <= len g by NAT_1:13; Finf ({x1},0) = {x1} by FINTOPO3:32 .= Finf (B0,0) by A3, FINTOPO3:32 ; then A70: S1[ 0 ] by A26, FINTOPO3:32; for j being Element of NAT holds S1[j] from NAT_1:sch_1(A70, A34); hence ( g . (i + 1) in Finf (B0,i) & ( i >= 1 implies not g . (i + 1) in Finf (B0,(i -' 1)) ) ) by A69; ::_thesis: verum end;