:: FINTOPO3 semantic presentation begin definition let T be non empty RelStr ; let A be Subset of T; funcA ^d -> Subset of T equals :: FINTOPO3:def 1 { x where x is Element of T : for y being Element of T st y in A ` holds not x in U_FT y } ; coherence { x where x is Element of T : for y being Element of T st y in A ` holds not x in U_FT y } is Subset of T proof defpred S1[ Element of T] means for y being Element of T st y in A ` holds not \$1 in U_FT y; { x where x is Element of T : S1[x] } is Subset of T from DOMAIN_1:sch_7(); hence { x where x is Element of T : for y being Element of T st y in A ` holds not x in U_FT y } is Subset of T ; ::_thesis: verum end; end; :: deftheorem defines ^d FINTOPO3:def_1_:_ for T being non empty RelStr for A being Subset of T holds A ^d = { x where x is Element of T : for y being Element of T st y in A ` holds not x in U_FT y } ; theorem Th1: :: FINTOPO3:1 for T being non empty RelStr for A being Subset of T st T is filled holds A c= A ^f proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds A c= A ^f let A be Subset of T; ::_thesis: ( T is filled implies A c= A ^f ) assume A1: T is filled ; ::_thesis: A c= A ^f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A ^f ) assume A2: x in A ; ::_thesis: x in A ^f then reconsider y = x as Element of T ; y in U_FT y by A1, FIN_TOPO:def_4; hence x in A ^f by A2, FIN_TOPO:11; ::_thesis: verum end; theorem Th2: :: FINTOPO3:2 for T being non empty RelStr for A being Subset of T for x being Element of T holds ( x in A ^d iff for y being Element of T st y in A ` holds not x in U_FT y ) proof let T be non empty RelStr ; ::_thesis: for A being Subset of T for x being Element of T holds ( x in A ^d iff for y being Element of T st y in A ` holds not x in U_FT y ) let A be Subset of T; ::_thesis: for x being Element of T holds ( x in A ^d iff for y being Element of T st y in A ` holds not x in U_FT y ) let x be Element of T; ::_thesis: ( x in A ^d iff for y being Element of T st y in A ` holds not x in U_FT y ) thus ( x in A ^d implies for y being Element of T st y in A ` holds not x in U_FT y ) ::_thesis: ( ( for y being Element of T st y in A ` holds not x in U_FT y ) implies x in A ^d ) proof assume x in A ^d ; ::_thesis: for y being Element of T st y in A ` holds not x in U_FT y then ex y being Element of T st ( y = x & ( for z being Element of T st z in A ` holds not y in U_FT z ) ) ; hence for y being Element of T st y in A ` holds not x in U_FT y ; ::_thesis: verum end; assume for z being Element of T st z in A ` holds not x in U_FT z ; ::_thesis: x in A ^d hence x in A ^d ; ::_thesis: verum end; theorem Th3: :: FINTOPO3:3 for T being non empty RelStr for A being Subset of T st T is filled holds A ^d c= A proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds A ^d c= A let A be Subset of T; ::_thesis: ( T is filled implies A ^d c= A ) assume A1: T is filled ; ::_thesis: A ^d c= A thus A ^d c= A ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^d or x in A ) assume A2: x in A ^d ; ::_thesis: x in A then reconsider z = x as Element of T ; now__::_thesis:_x_in_A assume not x in A ; ::_thesis: contradiction then A3: x in A ` by A2, SUBSET_1:29; x in U_FT z by A1, FIN_TOPO:def_4; hence contradiction by A2, A3, Th2; ::_thesis: verum end; hence x in A ; ::_thesis: verum end; end; theorem Th4: :: FINTOPO3:4 for T being non empty RelStr for A being Subset of T holds A ^d = ((A `) ^f) ` proof let T be non empty RelStr ; ::_thesis: for A being Subset of T holds A ^d = ((A `) ^f) ` let A be Subset of T; ::_thesis: A ^d = ((A `) ^f) ` for x being set holds ( x in A ^d iff x in ((A `) ^f) ` ) proof let x be set ; ::_thesis: ( x in A ^d iff x in ((A `) ^f) ` ) A1: (A `) ^f = { x2 where x2 is Element of T : ex y being Element of T st ( y in A ` & x2 in U_FT y ) } by FIN_TOPO:def_12; thus ( x in A ^d implies x in ((A `) ^f) ` ) ::_thesis: ( x in ((A `) ^f) ` implies x in A ^d ) proof A2: (A `) ^f = { x2 where x2 is Element of T : ex y being Element of T st ( y in A ` & x2 in U_FT y ) } by FIN_TOPO:def_12; assume A3: x in A ^d ; ::_thesis: x in ((A `) ^f) ` then for x2 being Element of T holds ( not x2 = x or for y being Element of T holds ( not y in A ` or not x2 in U_FT y ) ) by Th2; then not x in (A `) ^f by A2; hence x in ((A `) ^f) ` by A3, SUBSET_1:29; ::_thesis: verum end; assume A4: x in ((A `) ^f) ` ; ::_thesis: x in A ^d then not x in (A `) ^f by XBOOLE_0:def_5; then for y being Element of T st y in A ` holds not x in U_FT y by A1; hence x in A ^d by A4; ::_thesis: verum end; hence A ^d = ((A `) ^f) ` by TARSKI:1; ::_thesis: verum end; theorem Th5: :: FINTOPO3:5 for T being non empty RelStr for A, B being Subset of T st A c= B holds A ^f c= B ^f proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T st A c= B holds A ^f c= B ^f let A, B be Subset of T; ::_thesis: ( A c= B implies A ^f c= B ^f ) assume A1: A c= B ; ::_thesis: A ^f c= B ^f let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A ^f or z in B ^f ) assume z in A ^f ; ::_thesis: z in B ^f then ex y being Element of T st ( y in A & z in U_FT y ) by FIN_TOPO:11; hence z in B ^f by A1, FIN_TOPO:11; ::_thesis: verum end; theorem Th6: :: FINTOPO3:6 for T being non empty RelStr for A, B being Subset of T st A c= B holds A ^d c= B ^d proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T st A c= B holds A ^d c= B ^d let A, B be Subset of T; ::_thesis: ( A c= B implies A ^d c= B ^d ) assume A c= B ; ::_thesis: A ^d c= B ^d then A1: B ` c= A ` by SUBSET_1:12; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A ^d or z in B ^d ) assume A2: z in A ^d ; ::_thesis: z in B ^d then for y being Element of T st y in B ` holds not z in U_FT y by A1, Th2; hence z in B ^d by A2; ::_thesis: verum end; theorem :: FINTOPO3:7 for T being non empty RelStr for A, B being Subset of T holds (A /\ B) ^b c= (A ^b) /\ (B ^b) proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A /\ B) ^b c= (A ^b) /\ (B ^b) let A, B be Subset of T; ::_thesis: (A /\ B) ^b c= (A ^b) /\ (B ^b) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) ^b or x in (A ^b) /\ (B ^b) ) assume A1: x in (A /\ B) ^b ; ::_thesis: x in (A ^b) /\ (B ^b) then reconsider px = x as Point of T ; A2: U_FT px meets A /\ B by A1, FIN_TOPO:8; then U_FT px meets B by XBOOLE_1:74; then A3: x in B ^b by FIN_TOPO:8; U_FT px meets A by A2, XBOOLE_1:74; then x in A ^b by FIN_TOPO:8; hence x in (A ^b) /\ (B ^b) by A3, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th8: :: FINTOPO3:8 for T being non empty RelStr for A, B being Subset of T holds (A \/ B) ^b = (A ^b) \/ (B ^b) proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A \/ B) ^b = (A ^b) \/ (B ^b) let A, B be Subset of T; ::_thesis: (A \/ B) ^b = (A ^b) \/ (B ^b) thus (A \/ B) ^b c= (A ^b) \/ (B ^b) :: according to XBOOLE_0:def_10 ::_thesis: (A ^b) \/ (B ^b) c= (A \/ 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 A1: x in (A \/ B) ^b ; ::_thesis: x in (A ^b) \/ (B ^b) then reconsider px = x as Point of T ; U_FT px meets A \/ B by A1, FIN_TOPO:8; then ( U_FT px meets A or U_FT px meets B ) by XBOOLE_1:70; then ( x in A ^b or x in B ^b ) by FIN_TOPO:8; hence x in (A ^b) \/ (B ^b) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^b) \/ (B ^b) or x in (A \/ B) ^b ) assume A2: x in (A ^b) \/ (B ^b) ; ::_thesis: x in (A \/ B) ^b then reconsider px = x as Point of T ; ( x in A ^b or x in B ^b ) by A2, XBOOLE_0:def_3; then ( U_FT px meets A or U_FT px meets B ) by FIN_TOPO:8; then U_FT px meets A \/ B by XBOOLE_1:70; hence x in (A \/ B) ^b by FIN_TOPO:8; ::_thesis: verum end; theorem :: FINTOPO3:9 for T being non empty RelStr for A, B being Subset of T holds (A ^i) \/ (B ^i) c= (A \/ B) ^i proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A ^i) \/ (B ^i) c= (A \/ B) ^i let A, B be Subset of T; ::_thesis: (A ^i) \/ (B ^i) c= (A \/ B) ^i let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^i) \/ (B ^i) or x in (A \/ B) ^i ) assume A1: x in (A ^i) \/ (B ^i) ; ::_thesis: x in (A \/ B) ^i then reconsider px = x as Point of T ; ( x in A ^i or x in B ^i ) by A1, XBOOLE_0:def_3; then A2: ( U_FT px c= A or U_FT px c= B ) by FIN_TOPO:7; ( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7; then U_FT px c= A \/ B by A2, XBOOLE_1:1; hence x in (A \/ B) ^i by FIN_TOPO:7; ::_thesis: verum end; theorem Th10: :: FINTOPO3:10 for T being non empty RelStr for A, B being Subset of T holds (A ^i) /\ (B ^i) = (A /\ B) ^i proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A ^i) /\ (B ^i) = (A /\ B) ^i let A, B be Subset of T; ::_thesis: (A ^i) /\ (B ^i) = (A /\ B) ^i thus (A ^i) /\ (B ^i) c= (A /\ B) ^i :: according to XBOOLE_0:def_10 ::_thesis: (A /\ B) ^i c= (A ^i) /\ (B ^i) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^i) /\ (B ^i) or x in (A /\ B) ^i ) assume A1: x in (A ^i) /\ (B ^i) ; ::_thesis: x in (A /\ B) ^i then reconsider px = x as Point of T ; x in B ^i by A1, XBOOLE_0:def_4; then A2: U_FT px c= B by FIN_TOPO:7; x in A ^i by A1, XBOOLE_0:def_4; then U_FT px c= A by FIN_TOPO:7; then U_FT px c= A /\ B by A2, XBOOLE_1:19; hence x in (A /\ B) ^i by FIN_TOPO:7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) ^i or x in (A ^i) /\ (B ^i) ) assume A3: x in (A /\ B) ^i ; ::_thesis: x in (A ^i) /\ (B ^i) then reconsider px = x as Point of T ; A4: U_FT px c= A /\ B by A3, FIN_TOPO:7; then U_FT px c= B by XBOOLE_1:18; then A5: x in B ^i by FIN_TOPO:7; U_FT px c= A by A4, XBOOLE_1:18; then x in A ^i by FIN_TOPO:7; hence x in (A ^i) /\ (B ^i) by A5, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th11: :: FINTOPO3:11 for T being non empty RelStr for A, B being Subset of T holds (A ^f) \/ (B ^f) = (A \/ B) ^f proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A ^f) \/ (B ^f) = (A \/ B) ^f let A, B be Subset of T; ::_thesis: (A ^f) \/ (B ^f) = (A \/ B) ^f ( A ^f c= (A \/ B) ^f & B ^f c= (A \/ B) ^f ) by Th5, XBOOLE_1:7; hence (A ^f) \/ (B ^f) c= (A \/ B) ^f by XBOOLE_1:8; :: according to XBOOLE_0:def_10 ::_thesis: (A \/ B) ^f c= (A ^f) \/ (B ^f) let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (A \/ B) ^f or z in (A ^f) \/ (B ^f) ) assume z in (A \/ B) ^f ; ::_thesis: z in (A ^f) \/ (B ^f) then consider y being Element of T such that A1: y in A \/ B and A2: z in U_FT y by FIN_TOPO:11; percases ( y in A or y in B ) by A1, XBOOLE_0:def_3; suppose y in A ; ::_thesis: z in (A ^f) \/ (B ^f) then z in A ^f by A2, FIN_TOPO:11; hence z in (A ^f) \/ (B ^f) by XBOOLE_0:def_3; ::_thesis: verum end; suppose y in B ; ::_thesis: z in (A ^f) \/ (B ^f) then z in B ^f by A2, FIN_TOPO:11; hence z in (A ^f) \/ (B ^f) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; theorem Th12: :: FINTOPO3:12 for T being non empty RelStr for A, B being Subset of T holds (A ^d) /\ (B ^d) = (A /\ B) ^d proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A ^d) /\ (B ^d) = (A /\ B) ^d let A, B be Subset of T; ::_thesis: (A ^d) /\ (B ^d) = (A /\ B) ^d A1: B ^d = ((B `) ^f) ` by Th4; thus (A ^d) /\ (B ^d) = (((A `) ^f) `) /\ (B ^d) by Th4 .= (((A `) ^f) \/ ((B `) ^f)) ` by A1, XBOOLE_1:53 .= (((A `) \/ (B `)) ^f) ` by Th11 .= (((A /\ B) `) ^f) ` by XBOOLE_1:54 .= (A /\ B) ^d by Th4 ; ::_thesis: verum end; definition let T be non empty RelStr ; let A be Subset of T; func Fcl A -> Function of NAT,(bool the carrier of T) means :Def2: :: FINTOPO3:def 2 ( ( for n being Element of NAT for B being Subset of T st B = it . n holds it . (n + 1) = B ^b ) & it . 0 = A ); existence ex b1 being Function of NAT,(bool the carrier of T) st ( ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^b ) & b1 . 0 = A ) proof defpred S1[ set , set , set ] means for B being Subset of T st B = \$2 holds \$3 = B ^b ; A1: for n being Element of NAT for x being Subset of T ex y being Subset of T st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Subset of T ex y being Subset of T st S1[n,x,y] let x be Subset of T; ::_thesis: ex y being Subset of T st S1[n,x,y] reconsider C = x as Subset of T ; S1[n,x,C ^b ] ; hence ex y being Subset of T st S1[n,x,y] ; ::_thesis: verum end; ex f being Function of NAT,(bool the carrier of T) st ( f . 0 = A & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A1); hence ex b1 being Function of NAT,(bool the carrier of T) st ( ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^b ) & b1 . 0 = A ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^b ) & b1 . 0 = A & ( for n being Element of NAT for B being Subset of T st B = b2 . n holds b2 . (n + 1) = B ^b ) & b2 . 0 = A holds b1 = b2 proof let f1, f2 be Function of NAT,(bool the carrier of T); ::_thesis: ( ( for n being Element of NAT for B being Subset of T st B = f1 . n holds f1 . (n + 1) = B ^b ) & f1 . 0 = A & ( for n being Element of NAT for B being Subset of T st B = f2 . n holds f2 . (n + 1) = B ^b ) & f2 . 0 = A implies f1 = f2 ) assume that A2: for n being Element of NAT for B being Subset of T st B = f1 . n holds f1 . (n + 1) = B ^b and A3: f1 . 0 = A and A4: for n being Element of NAT for B being Subset of T st B = f2 . n holds f2 . (n + 1) = B ^b and A5: f2 . 0 = A ; ::_thesis: f1 = f2 defpred S1[ Element of NAT ] means f1 . \$1 = f2 . \$1; A6: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A7: S1[n] ; ::_thesis: S1[n + 1] reconsider B1 = f1 . n as Subset of T ; B1 ^b = f1 . (n + 1) by A2; hence S1[n + 1] by A4, A7; ::_thesis: verum end; A8: dom f1 = NAT by FUNCT_2:def_1; then A9: dom f1 = dom f2 by FUNCT_2:def_1; A10: S1[ 0 ] by A3, A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A10, A6); then for x being set st x in dom f1 holds f1 . x = f2 . x by A8; hence f1 = f2 by A9, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines Fcl FINTOPO3:def_2_:_ for T being non empty RelStr for A being Subset of T for b3 being Function of NAT,(bool the carrier of T) holds ( b3 = Fcl A iff ( ( for n being Element of NAT for B being Subset of T st B = b3 . n holds b3 . (n + 1) = B ^b ) & b3 . 0 = A ) ); definition let T be non empty RelStr ; let A be Subset of T; let n be Nat; func Fcl (A,n) -> Subset of T equals :: FINTOPO3:def 3 (Fcl A) . n; coherence (Fcl A) . n is Subset of T proof reconsider n9 = n as Element of NAT by ORDINAL1:def_12; (Fcl A) . n9 c= the carrier of T ; hence (Fcl A) . n is Subset of T ; ::_thesis: verum end; end; :: deftheorem defines Fcl FINTOPO3:def_3_:_ for T being non empty RelStr for A being Subset of T for n being Nat holds Fcl (A,n) = (Fcl A) . n; definition let T be non empty RelStr ; let A be Subset of T; func Fint A -> Function of NAT,(bool the carrier of T) means :Def4: :: FINTOPO3:def 4 ( ( for n being Element of NAT for B being Subset of T st B = it . n holds it . (n + 1) = B ^i ) & it . 0 = A ); existence ex b1 being Function of NAT,(bool the carrier of T) st ( ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^i ) & b1 . 0 = A ) proof defpred S1[ set , set , set ] means for B being Subset of T st B = \$2 holds \$3 = B ^i ; A1: for n being Element of NAT for x being Subset of T ex y being Subset of T st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Subset of T ex y being Subset of T st S1[n,x,y] let x be Subset of T; ::_thesis: ex y being Subset of T st S1[n,x,y] reconsider C = x as Subset of T ; for B being Subset of T st B = x holds C ^i = B ^i ; hence ex y being Subset of T st S1[n,x,y] ; ::_thesis: verum end; ex f being Function of NAT,(bool the carrier of T) st ( f . 0 = A & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A1); hence ex b1 being Function of NAT,(bool the carrier of T) st ( ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^i ) & b1 . 0 = A ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^i ) & b1 . 0 = A & ( for n being Element of NAT for B being Subset of T st B = b2 . n holds b2 . (n + 1) = B ^i ) & b2 . 0 = A holds b1 = b2 proof let f1, f2 be Function of NAT,(bool the carrier of T); ::_thesis: ( ( for n being Element of NAT for B being Subset of T st B = f1 . n holds f1 . (n + 1) = B ^i ) & f1 . 0 = A & ( for n being Element of NAT for B being Subset of T st B = f2 . n holds f2 . (n + 1) = B ^i ) & f2 . 0 = A implies f1 = f2 ) assume that A2: for n being Element of NAT for B being Subset of T st B = f1 . n holds f1 . (n + 1) = B ^i and A3: f1 . 0 = A and A4: for n being Element of NAT for B being Subset of T st B = f2 . n holds f2 . (n + 1) = B ^i and A5: f2 . 0 = A ; ::_thesis: f1 = f2 defpred S1[ Element of NAT ] means f1 . \$1 = f2 . \$1; A6: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A7: S1[n] ; ::_thesis: S1[n + 1] reconsider B1 = f1 . n as Subset of T ; B1 ^i = f1 . (n + 1) by A2; hence S1[n + 1] by A4, A7; ::_thesis: verum end; A8: dom f1 = NAT by FUNCT_2:def_1; then A9: dom f1 = dom f2 by FUNCT_2:def_1; A10: S1[ 0 ] by A3, A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A10, A6); then for x being set st x in dom f1 holds f1 . x = f2 . x by A8; hence f1 = f2 by A9, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines Fint FINTOPO3:def_4_:_ for T being non empty RelStr for A being Subset of T for b3 being Function of NAT,(bool the carrier of T) holds ( b3 = Fint A iff ( ( for n being Element of NAT for B being Subset of T st B = b3 . n holds b3 . (n + 1) = B ^i ) & b3 . 0 = A ) ); definition let T be non empty RelStr ; let A be Subset of T; let n be Nat; func Fint (A,n) -> Subset of T equals :: FINTOPO3:def 5 (Fint A) . n; coherence (Fint A) . n is Subset of T proof reconsider n9 = n as Element of NAT by ORDINAL1:def_12; (Fint A) . n9 c= the carrier of T ; hence (Fint A) . n is Subset of T ; ::_thesis: verum end; end; :: deftheorem defines Fint FINTOPO3:def_5_:_ for T being non empty RelStr for A being Subset of T for n being Nat holds Fint (A,n) = (Fint A) . n; theorem :: FINTOPO3:13 for T being non empty RelStr for A being Subset of T for n being Element of NAT holds Fcl (A,(n + 1)) = (Fcl (A,n)) ^b by Def2; theorem :: FINTOPO3:14 for T being non empty RelStr for A being Subset of T holds Fcl (A,0) = A by Def2; theorem Th15: :: FINTOPO3:15 for T being non empty RelStr for A being Subset of T holds Fcl (A,1) = A ^b proof let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fcl (A,1) = A ^b let A be Subset of T; ::_thesis: Fcl (A,1) = A ^b (Fcl A) . 0 = A by Def2; then (Fcl A) . (0 + 1) = A ^b by Def2; hence Fcl (A,1) = A ^b ; ::_thesis: verum end; theorem :: FINTOPO3:16 for T being non empty RelStr for A being Subset of T holds Fcl (A,2) = (A ^b) ^b proof let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fcl (A,2) = (A ^b) ^b let A be Subset of T; ::_thesis: Fcl (A,2) = (A ^b) ^b for B being Subset of T st B = (Fcl A) . 1 holds (Fcl A) . (1 + 1) = B ^b by Def2; then Fcl (A,2) = (Fcl (A,1)) ^b .= (A ^b) ^b by Th15 ; hence Fcl (A,2) = (A ^b) ^b ; ::_thesis: verum end; theorem Th17: :: FINTOPO3:17 for T being non empty RelStr for A, B being Subset of T for n being Element of NAT holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n)) proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T for n being Element of NAT holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n)) let A, B be Subset of T; ::_thesis: for n being Element of NAT holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n)) let n be Element of NAT ; ::_thesis: Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n)) for n being Element of NAT holds (Fcl (A \/ B)) . n = ((Fcl A) . n) \/ ((Fcl B) . n) proof defpred S1[ Element of NAT ] means (Fcl (A \/ B)) . \$1 = ((Fcl A) . \$1) \/ ((Fcl B) . \$1); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] (Fcl (A \/ B)) . (k + 1) = (Fcl ((A \/ B),k)) ^b by Def2 .= ((Fcl (A,k)) ^b) \/ ((Fcl (B,k)) ^b) by A2, Th8 .= (Fcl (A,(k + 1))) \/ ((Fcl (B,k)) ^b) by Def2 .= ((Fcl A) . (k + 1)) \/ ((Fcl B) . (k + 1)) by Def2 ; hence S1[k + 1] ; ::_thesis: verum end; (Fcl (A \/ B)) . 0 = A \/ B by Def2 .= ((Fcl A) . 0) \/ B by Def2 .= ((Fcl A) . 0) \/ ((Fcl B) . 0) by Def2 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence for n being Element of NAT holds (Fcl (A \/ B)) . n = ((Fcl A) . n) \/ ((Fcl B) . n) ; ::_thesis: verum end; hence Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n)) ; ::_thesis: verum end; theorem :: FINTOPO3:18 for T being non empty RelStr for A being Subset of T for n being Element of NAT holds Fint (A,(n + 1)) = (Fint (A,n)) ^i by Def4; theorem :: FINTOPO3:19 for T being non empty RelStr for A being Subset of T holds Fint (A,0) = A by Def4; theorem Th20: :: FINTOPO3:20 for T being non empty RelStr for A being Subset of T holds Fint (A,1) = A ^i proof let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fint (A,1) = A ^i let A be Subset of T; ::_thesis: Fint (A,1) = A ^i ( (Fint A) . 0 = A & ( for B being Subset of T st B = (Fint A) . 0 holds (Fint A) . (0 + 1) = B ^i ) ) by Def4; hence Fint (A,1) = A ^i ; ::_thesis: verum end; theorem :: FINTOPO3:21 for T being non empty RelStr for A being Subset of T holds Fint (A,2) = (A ^i) ^i proof let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fint (A,2) = (A ^i) ^i let A be Subset of T; ::_thesis: Fint (A,2) = (A ^i) ^i thus Fint (A,2) = Fint (A,(1 + 1)) .= (Fint (A,1)) ^i by Def4 .= (A ^i) ^i by Th20 ; ::_thesis: verum end; theorem Th22: :: FINTOPO3:22 for T being non empty RelStr for A, B being Subset of T for n being Element of NAT holds Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n)) proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T for n being Element of NAT holds Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n)) let A, B be Subset of T; ::_thesis: for n being Element of NAT holds Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n)) defpred S1[ Element of NAT ] means (Fint (A /\ B)) . \$1 = ((Fint A) . \$1) /\ ((Fint B) . \$1); let n be Element of NAT ; ::_thesis: Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n)) A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] (Fint (A /\ B)) . (k + 1) = (Fint ((A /\ B),k)) ^i by Def4 .= ((Fint (A,k)) ^i) /\ ((Fint (B,k)) ^i) by A2, Th10 .= (Fint (A,(k + 1))) /\ ((Fint (B,k)) ^i) by Def4 .= ((Fint A) . (k + 1)) /\ ((Fint B) . (k + 1)) by Def4 ; hence S1[k + 1] ; ::_thesis: verum end; (Fint (A /\ B)) . 0 = A /\ B by Def4 .= ((Fint A) . 0) /\ B by Def4 .= ((Fint A) . 0) /\ ((Fint B) . 0) by Def4 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n)) ; ::_thesis: verum end; theorem :: FINTOPO3:23 for T being non empty RelStr for A being Subset of T st T is filled holds for n being Element of NAT holds A c= Fcl (A,n) proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds for n being Element of NAT holds A c= Fcl (A,n) let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds A c= Fcl (A,n) ) defpred S1[ Element of NAT ] means A c= (Fcl A) . \$1; assume A1: T is filled ; ::_thesis: for n being Element of NAT holds A c= Fcl (A,n) A2: 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 S1[k] ; ::_thesis: S1[k + 1] then A ^b c= (Fcl (A,k)) ^b by FIN_TOPO:14; then A3: A ^b c= Fcl (A,(k + 1)) by Def2; A c= A ^b by A1, FIN_TOPO:13; hence S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: A c= Fcl (A,n) A4: S1[ 0 ] by Def2; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence A c= Fcl (A,n) ; ::_thesis: verum end; theorem :: FINTOPO3:24 for T being non empty RelStr for A being Subset of T st T is filled holds for n being Element of NAT holds Fint (A,n) c= A proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds for n being Element of NAT holds Fint (A,n) c= A let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fint (A,n) c= A ) defpred S1[ Element of NAT ] means (Fint A) . \$1 c= A; assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fint (A,n) c= A A2: 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 S1[k] ; ::_thesis: S1[k + 1] then (Fint (A,k)) ^i c= A ^i by FINTOPO2:1; then A3: Fint (A,(k + 1)) c= A ^i by Def4; A ^i c= A by A1, FIN_TOPO:22; hence S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: Fint (A,n) c= A A4: S1[ 0 ] by Def4; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence Fint (A,n) c= A ; ::_thesis: verum end; theorem :: FINTOPO3:25 for T being non empty RelStr for A being Subset of T st T is filled holds for n being Element of NAT holds Fcl (A,n) c= Fcl (A,(n + 1)) proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds for n being Element of NAT holds Fcl (A,n) c= Fcl (A,(n + 1)) let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fcl (A,n) c= Fcl (A,(n + 1)) ) assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fcl (A,n) c= Fcl (A,(n + 1)) let n be Element of NAT ; ::_thesis: Fcl (A,n) c= Fcl (A,(n + 1)) ((Fcl A) . n) ^b = Fcl (A,(n + 1)) by Def2; hence Fcl (A,n) c= Fcl (A,(n + 1)) by A1, FIN_TOPO:13; ::_thesis: verum end; theorem :: FINTOPO3:26 for T being non empty RelStr for A being Subset of T st T is filled holds for n being Element of NAT holds Fint (A,(n + 1)) c= Fint (A,n) proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds for n being Element of NAT holds Fint (A,(n + 1)) c= Fint (A,n) let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fint (A,(n + 1)) c= Fint (A,n) ) assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fint (A,(n + 1)) c= Fint (A,n) let n be Element of NAT ; ::_thesis: Fint (A,(n + 1)) c= Fint (A,n) ((Fint A) . n) ^i = Fint (A,(n + 1)) by Def4; hence Fint (A,(n + 1)) c= Fint (A,n) by A1, FIN_TOPO:22; ::_thesis: verum end; theorem Th27: :: FINTOPO3:27 for T being non empty RelStr for A being Subset of T for n being Element of NAT holds (Fint ((A `),n)) ` = Fcl (A,n) proof let T be non empty RelStr ; ::_thesis: for A being Subset of T for n being Element of NAT holds (Fint ((A `),n)) ` = Fcl (A,n) let A be Subset of T; ::_thesis: for n being Element of NAT holds (Fint ((A `),n)) ` = Fcl (A,n) defpred S1[ Element of NAT ] means (Fint ((A `),\$1)) ` = Fcl (A,\$1); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] Fcl (A,(k + 1)) = (Fcl (A,k)) ^b by Def2 .= ((((Fint ((A `),k)) `) `) ^i) ` by A2, FIN_TOPO:16 .= (Fint ((A `),(k + 1))) ` by Def4 ; hence S1[k + 1] ; ::_thesis: verum end; (Fint ((A `),0)) ` = (A `) ` by Def4 .= Fcl (A,0) by Def2 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence for n being Element of NAT holds (Fint ((A `),n)) ` = Fcl (A,n) ; ::_thesis: verum end; theorem Th28: :: FINTOPO3:28 for T being non empty RelStr for A being Subset of T for n being Element of NAT holds (Fcl ((A `),n)) ` = Fint (A,n) proof let T be non empty RelStr ; ::_thesis: for A being Subset of T for n being Element of NAT holds (Fcl ((A `),n)) ` = Fint (A,n) let A be Subset of T; ::_thesis: for n being Element of NAT holds (Fcl ((A `),n)) ` = Fint (A,n) let n be Element of NAT ; ::_thesis: (Fcl ((A `),n)) ` = Fint (A,n) Fint (A,n) = ((Fint (((A `) `),n)) `) ` .= (Fcl ((A `),n)) ` by Th27 ; hence (Fcl ((A `),n)) ` = Fint (A,n) ; ::_thesis: verum end; theorem :: FINTOPO3:29 for T being non empty RelStr for A, B being Subset of T for n being Element of NAT holds (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) ` proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T for n being Element of NAT holds (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) ` let A, B be Subset of T; ::_thesis: for n being Element of NAT holds (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) ` let n be Element of NAT ; ::_thesis: (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) ` (Fcl (A,n)) \/ (Fcl (B,n)) = Fcl ((A \/ B),n) by Th17 .= (Fint (((A \/ B) `),n)) ` by Th27 ; hence (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) ` ; ::_thesis: verum end; theorem :: FINTOPO3:30 for T being non empty RelStr for A, B being Subset of T for n being Element of NAT holds (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) ` proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T for n being Element of NAT holds (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) ` let A, B be Subset of T; ::_thesis: for n being Element of NAT holds (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) ` let n be Element of NAT ; ::_thesis: (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) ` (Fint (A,n)) /\ (Fint (B,n)) = Fint ((A /\ B),n) by Th22 .= (Fcl (((A /\ B) `),n)) ` by Th28 ; hence (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) ` ; ::_thesis: verum end; definition let T be non empty RelStr ; let A be Subset of T; func Finf A -> Function of NAT,(bool the carrier of T) means :Def6: :: FINTOPO3:def 6 ( ( for n being Element of NAT for B being Subset of T st B = it . n holds it . (n + 1) = B ^f ) & it . 0 = A ); existence ex b1 being Function of NAT,(bool the carrier of T) st ( ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^f ) & b1 . 0 = A ) proof defpred S1[ set , set , set ] means for B being Subset of T st B = \$2 holds \$3 = B ^f ; A1: for n being Element of NAT for x being Subset of T ex y being Subset of T st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Subset of T ex y being Subset of T st S1[n,x,y] let x be Subset of T; ::_thesis: ex y being Subset of T st S1[n,x,y] reconsider C = x as Subset of T ; for B being Subset of T st B = x holds C ^f = B ^f ; hence ex y being Subset of T st S1[n,x,y] ; ::_thesis: verum end; ex f being Function of NAT,(bool the carrier of T) st ( f . 0 = A & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A1); hence ex b1 being Function of NAT,(bool the carrier of T) st ( ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^f ) & b1 . 0 = A ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^f ) & b1 . 0 = A & ( for n being Element of NAT for B being Subset of T st B = b2 . n holds b2 . (n + 1) = B ^f ) & b2 . 0 = A holds b1 = b2 proof let f1, f2 be Function of NAT,(bool the carrier of T); ::_thesis: ( ( for n being Element of NAT for B being Subset of T st B = f1 . n holds f1 . (n + 1) = B ^f ) & f1 . 0 = A & ( for n being Element of NAT for B being Subset of T st B = f2 . n holds f2 . (n + 1) = B ^f ) & f2 . 0 = A implies f1 = f2 ) assume that A2: for n being Element of NAT for B being Subset of T st B = f1 . n holds f1 . (n + 1) = B ^f and A3: f1 . 0 = A and A4: for n being Element of NAT for B being Subset of T st B = f2 . n holds f2 . (n + 1) = B ^f and A5: f2 . 0 = A ; ::_thesis: f1 = f2 defpred S1[ Element of NAT ] means f1 . \$1 = f2 . \$1; A6: dom f1 = NAT by FUNCT_2:def_1; then A7: dom f1 = dom f2 by FUNCT_2:def_1; for n being Element of NAT holds S1[n] proof let n be Element of NAT ; ::_thesis: S1[n] A8: 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 A9: S1[k] ; ::_thesis: S1[k + 1] reconsider B1 = f1 . k as Subset of T ; B1 ^f = f1 . (k + 1) by A2; hence S1[k + 1] by A4, A9; ::_thesis: verum end; A10: S1[ 0 ] by A3, A5; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A10, A8); hence S1[n] ; ::_thesis: verum end; then for x being set st x in dom f1 holds f1 . x = f2 . x by A6; hence f1 = f2 by A7, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def6 defines Finf FINTOPO3:def_6_:_ for T being non empty RelStr for A being Subset of T for b3 being Function of NAT,(bool the carrier of T) holds ( b3 = Finf A iff ( ( for n being Element of NAT for B being Subset of T st B = b3 . n holds b3 . (n + 1) = B ^f ) & b3 . 0 = A ) ); definition let T be non empty RelStr ; let A be Subset of T; let n be Nat; func Finf (A,n) -> Subset of T equals :: FINTOPO3:def 7 (Finf A) . n; coherence (Finf A) . n is Subset of T proof reconsider n9 = n as Element of NAT by ORDINAL1:def_12; (Finf A) . n9 c= the carrier of T ; hence (Finf A) . n is Subset of T ; ::_thesis: verum end; end; :: deftheorem defines Finf FINTOPO3:def_7_:_ for T being non empty RelStr for A being Subset of T for n being Nat holds Finf (A,n) = (Finf A) . n; definition let T be non empty RelStr ; let A be Subset of T; func Fdfl A -> Function of NAT,(bool the carrier of T) means :Def8: :: FINTOPO3:def 8 ( ( for n being Element of NAT for B being Subset of T st B = it . n holds it . (n + 1) = B ^d ) & it . 0 = A ); existence ex b1 being Function of NAT,(bool the carrier of T) st ( ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^d ) & b1 . 0 = A ) proof defpred S1[ set , set , set ] means for B being Subset of T st B = \$2 holds \$3 = B ^d ; A1: for n being Element of NAT for x being Subset of T ex y being Subset of T st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Subset of T ex y being Subset of T st S1[n,x,y] let x be Subset of T; ::_thesis: ex y being Subset of T st S1[n,x,y] for B being Subset of T st B = x holds x ^d = B ^d ; hence ex y being Subset of T st S1[n,x,y] ; ::_thesis: verum end; ex f being Function of NAT,(bool the carrier of T) st ( f . 0 = A & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A1); hence ex b1 being Function of NAT,(bool the carrier of T) st ( ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^d ) & b1 . 0 = A ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT for B being Subset of T st B = b1 . n holds b1 . (n + 1) = B ^d ) & b1 . 0 = A & ( for n being Element of NAT for B being Subset of T st B = b2 . n holds b2 . (n + 1) = B ^d ) & b2 . 0 = A holds b1 = b2 proof let f1, f2 be Function of NAT,(bool the carrier of T); ::_thesis: ( ( for n being Element of NAT for B being Subset of T st B = f1 . n holds f1 . (n + 1) = B ^d ) & f1 . 0 = A & ( for n being Element of NAT for B being Subset of T st B = f2 . n holds f2 . (n + 1) = B ^d ) & f2 . 0 = A implies f1 = f2 ) assume that A2: for n being Element of NAT for B being Subset of T st B = f1 . n holds f1 . (n + 1) = B ^d and A3: f1 . 0 = A and A4: for n being Element of NAT for B being Subset of T st B = f2 . n holds f2 . (n + 1) = B ^d and A5: f2 . 0 = A ; ::_thesis: f1 = f2 defpred S1[ Element of NAT ] means f1 . \$1 = f2 . \$1; A6: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A7: S1[n] ; ::_thesis: S1[n + 1] reconsider B1 = f1 . n as Subset of T ; B1 ^d = f1 . (n + 1) by A2; hence S1[n + 1] by A4, A7; ::_thesis: verum end; A8: dom f1 = NAT by FUNCT_2:def_1; then A9: dom f1 = dom f2 by FUNCT_2:def_1; A10: S1[ 0 ] by A3, A5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A10, A6); then for x being set st x in dom f1 holds f1 . x = f2 . x by A8; hence f1 = f2 by A9, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def8 defines Fdfl FINTOPO3:def_8_:_ for T being non empty RelStr for A being Subset of T for b3 being Function of NAT,(bool the carrier of T) holds ( b3 = Fdfl A iff ( ( for n being Element of NAT for B being Subset of T st B = b3 . n holds b3 . (n + 1) = B ^d ) & b3 . 0 = A ) ); definition let T be non empty RelStr ; let A be Subset of T; let n be Nat; func Fdfl (A,n) -> Subset of T equals :: FINTOPO3:def 9 (Fdfl A) . n; coherence (Fdfl A) . n is Subset of T proof reconsider n9 = n as Element of NAT by ORDINAL1:def_12; (Fdfl A) . n9 c= the carrier of T ; hence (Fdfl A) . n is Subset of T ; ::_thesis: verum end; end; :: deftheorem defines Fdfl FINTOPO3:def_9_:_ for T being non empty RelStr for A being Subset of T for n being Nat holds Fdfl (A,n) = (Fdfl A) . n; theorem :: FINTOPO3:31 for T being non empty RelStr for A being Subset of T for n being Element of NAT holds Finf (A,(n + 1)) = (Finf (A,n)) ^f by Def6; theorem :: FINTOPO3:32 for T being non empty RelStr for A being Subset of T holds Finf (A,0) = A by Def6; theorem Th33: :: FINTOPO3:33 for T being non empty RelStr for A being Subset of T holds Finf (A,1) = A ^f proof let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Finf (A,1) = A ^f let A be Subset of T; ::_thesis: Finf (A,1) = A ^f ( (Finf A) . 0 = A & ( for B being Subset of T st B = (Finf A) . 0 holds (Finf A) . (0 + 1) = B ^f ) ) by Def6; hence Finf (A,1) = A ^f ; ::_thesis: verum end; theorem :: FINTOPO3:34 for T being non empty RelStr for A being Subset of T holds Finf (A,2) = (A ^f) ^f proof let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Finf (A,2) = (A ^f) ^f let A be Subset of T; ::_thesis: Finf (A,2) = (A ^f) ^f Finf (A,2) = Finf (A,(1 + 1)) .= (Finf (A,1)) ^f by Def6 .= (A ^f) ^f by Th33 ; hence Finf (A,2) = (A ^f) ^f ; ::_thesis: verum end; theorem :: FINTOPO3:35 for T being non empty RelStr for A, B being Subset of T for n being Element of NAT holds Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n)) proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T for n being Element of NAT holds Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n)) let A, B be Subset of T; ::_thesis: for n being Element of NAT holds Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n)) defpred S1[ Element of NAT ] means (Finf (A \/ B)) . \$1 = ((Finf A) . \$1) \/ ((Finf B) . \$1); let n be Element of NAT ; ::_thesis: Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n)) A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] (Finf (A \/ B)) . (k + 1) = (Finf ((A \/ B),k)) ^f by Def6 .= ((Finf (A,k)) ^f) \/ ((Finf (B,k)) ^f) by A2, Th11 .= (Finf (A,(k + 1))) \/ ((Finf (B,k)) ^f) by Def6 .= ((Finf A) . (k + 1)) \/ ((Finf B) . (k + 1)) by Def6 ; hence S1[k + 1] ; ::_thesis: verum end; (Finf (A \/ B)) . 0 = A \/ B by Def6 .= ((Finf A) . 0) \/ B by Def6 .= ((Finf A) . 0) \/ ((Finf B) . 0) by Def6 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n)) ; ::_thesis: verum end; theorem :: FINTOPO3:36 for T being non empty RelStr for A being Subset of T st T is filled holds for n being Element of NAT holds A c= Finf (A,n) proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds for n being Element of NAT holds A c= Finf (A,n) let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds A c= Finf (A,n) ) defpred S1[ Element of NAT ] means A c= (Finf A) . \$1; assume A1: T is filled ; ::_thesis: for n being Element of NAT holds A c= Finf (A,n) A2: 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 S1[k] ; ::_thesis: S1[k + 1] then A ^f c= (Finf (A,k)) ^f by Th5; then A3: A ^f c= Finf (A,(k + 1)) by Def6; A c= A ^f by A1, Th1; hence S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: A c= Finf (A,n) A4: S1[ 0 ] by Def6; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence A c= Finf (A,n) ; ::_thesis: verum end; theorem :: FINTOPO3:37 for T being non empty RelStr for A being Subset of T st T is filled holds for n being Element of NAT holds Finf (A,n) c= Finf (A,(n + 1)) proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds for n being Element of NAT holds Finf (A,n) c= Finf (A,(n + 1)) let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Finf (A,n) c= Finf (A,(n + 1)) ) assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Finf (A,n) c= Finf (A,(n + 1)) let n be Element of NAT ; ::_thesis: Finf (A,n) c= Finf (A,(n + 1)) ((Finf A) . n) ^f = Finf (A,(n + 1)) by Def6; hence Finf (A,n) c= Finf (A,(n + 1)) by A1, Th1; ::_thesis: verum end; theorem :: FINTOPO3:38 for T being non empty RelStr for A being Subset of T for n being Element of NAT holds Fdfl (A,(n + 1)) = (Fdfl (A,n)) ^d by Def8; theorem :: FINTOPO3:39 for T being non empty RelStr for A being Subset of T holds Fdfl (A,0) = A by Def8; theorem Th40: :: FINTOPO3:40 for T being non empty RelStr for A being Subset of T holds Fdfl (A,1) = A ^d proof let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fdfl (A,1) = A ^d let A be Subset of T; ::_thesis: Fdfl (A,1) = A ^d ( (Fdfl A) . 0 = A & ( for B being Subset of T st B = (Fdfl A) . 0 holds (Fdfl A) . (0 + 1) = B ^d ) ) by Def8; hence Fdfl (A,1) = A ^d ; ::_thesis: verum end; theorem :: FINTOPO3:41 for T being non empty RelStr for A being Subset of T holds Fdfl (A,2) = (A ^d) ^d proof let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fdfl (A,2) = (A ^d) ^d let A be Subset of T; ::_thesis: Fdfl (A,2) = (A ^d) ^d Fdfl (A,2) = Fdfl (A,(1 + 1)) .= (Fdfl (A,1)) ^d by Def8 ; hence Fdfl (A,2) = (A ^d) ^d by Th40; ::_thesis: verum end; theorem Th42: :: FINTOPO3:42 for T being non empty RelStr for A, B being Subset of T for n being Element of NAT holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n)) proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T for n being Element of NAT holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n)) let A, B be Subset of T; ::_thesis: for n being Element of NAT holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n)) defpred S1[ Element of NAT ] means (Fdfl (A /\ B)) . \$1 = ((Fdfl A) . \$1) /\ ((Fdfl B) . \$1); let n be Element of NAT ; ::_thesis: Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n)) A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] (Fdfl (A /\ B)) . (k + 1) = (Fdfl ((A /\ B),k)) ^d by Def8 .= ((Fdfl (A,k)) ^d) /\ ((Fdfl (B,k)) ^d) by A2, Th12 .= (Fdfl (A,(k + 1))) /\ ((Fdfl (B,k)) ^d) by Def8 .= ((Fdfl A) . (k + 1)) /\ ((Fdfl B) . (k + 1)) by Def8 ; hence S1[k + 1] ; ::_thesis: verum end; (Fdfl (A /\ B)) . 0 = A /\ B by Def8 .= ((Fdfl A) . 0) /\ B by Def8 .= ((Fdfl A) . 0) /\ ((Fdfl B) . 0) by Def8 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n)) ; ::_thesis: verum end; theorem :: FINTOPO3:43 for T being non empty RelStr for A being Subset of T st T is filled holds for n being Element of NAT holds Fdfl (A,n) c= A proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds for n being Element of NAT holds Fdfl (A,n) c= A let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fdfl (A,n) c= A ) defpred S1[ Element of NAT ] means (Fdfl A) . \$1 c= A; assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fdfl (A,n) c= A A2: 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 S1[k] ; ::_thesis: S1[k + 1] then (Fdfl (A,k)) ^d c= A ^d by Th6; then A3: Fdfl (A,(k + 1)) c= A ^d by Def8; A ^d c= A by A1, Th3; hence S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: Fdfl (A,n) c= A A4: S1[ 0 ] by Def8; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence Fdfl (A,n) c= A ; ::_thesis: verum end; theorem :: FINTOPO3:44 for T being non empty RelStr for A being Subset of T st T is filled holds for n being Element of NAT holds Fdfl (A,(n + 1)) c= Fdfl (A,n) proof let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds for n being Element of NAT holds Fdfl (A,(n + 1)) c= Fdfl (A,n) let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fdfl (A,(n + 1)) c= Fdfl (A,n) ) assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fdfl (A,(n + 1)) c= Fdfl (A,n) let n be Element of NAT ; ::_thesis: Fdfl (A,(n + 1)) c= Fdfl (A,n) ((Fdfl A) . n) ^d = Fdfl (A,(n + 1)) by Def8; hence Fdfl (A,(n + 1)) c= Fdfl (A,n) by A1, Th3; ::_thesis: verum end; theorem Th45: :: FINTOPO3:45 for T being non empty RelStr for A being Subset of T for n being Element of NAT holds Fdfl (A,n) = (Finf ((A `),n)) ` proof let T be non empty RelStr ; ::_thesis: for A being Subset of T for n being Element of NAT holds Fdfl (A,n) = (Finf ((A `),n)) ` let A be Subset of T; ::_thesis: for n being Element of NAT holds Fdfl (A,n) = (Finf ((A `),n)) ` defpred S1[ Element of NAT ] means (Fdfl A) . \$1 = ((Finf (A `)) . \$1) ` ; let n be Element of NAT ; ::_thesis: Fdfl (A,n) = (Finf ((A `),n)) ` A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] (Fdfl A) . (k + 1) = (Fdfl (A,k)) ^d by Def8; then (Fdfl A) . (k + 1) = ((((Fdfl A) . k) `) ^f) ` by Th4 .= ((Finf (A `)) . (k + 1)) ` by A2, Def6 ; hence S1[k + 1] ; ::_thesis: verum end; ((Finf (A `)) . 0) ` = (A `) ` by Def6 .= A ; then A3: S1[ 0 ] by Def8; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence Fdfl (A,n) = (Finf ((A `),n)) ` ; ::_thesis: verum end; theorem :: FINTOPO3:46 for T being non empty RelStr for A, B being Subset of T for n being Element of NAT holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) ` proof let T be non empty RelStr ; ::_thesis: for A, B being Subset of T for n being Element of NAT holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) ` let A, B be Subset of T; ::_thesis: for n being Element of NAT holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) ` let n be Element of NAT ; ::_thesis: (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) ` (Fdfl (A,n)) /\ (Fdfl (B,n)) = Fdfl ((A /\ B),n) by Th42 .= (Finf (((A /\ B) `),n)) ` by Th45 ; hence (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) ` ; ::_thesis: verum end; definition let T be non empty RelStr ; let n be Nat; let x be Element of T; func U_FT (x,n) -> Subset of T equals :: FINTOPO3:def 10 Finf ((U_FT x),n); coherence Finf ((U_FT x),n) is Subset of T ; end; :: deftheorem defines U_FT FINTOPO3:def_10_:_ for T being non empty RelStr for n being Nat for x being Element of T holds U_FT (x,n) = Finf ((U_FT x),n); theorem :: FINTOPO3:47 for T being non empty RelStr for x being Element of T holds U_FT (x,0) = U_FT x by Def6; theorem :: FINTOPO3:48 for T being non empty RelStr for x being Element of T for n being Element of NAT holds U_FT (x,(n + 1)) = (U_FT (x,n)) ^f by Def6; definition let S, T be non empty RelStr ; predS,T are_mutually_symmetric means :: FINTOPO3:def 11 ( the carrier of S = the carrier of T & ( for x being Element of S for y being Element of T holds ( y in U_FT x iff x in U_FT y ) ) ); symmetry for S, T being non empty RelStr st the carrier of S = the carrier of T & ( for x being Element of S for y being Element of T holds ( y in U_FT x iff x in U_FT y ) ) holds ( the carrier of T = the carrier of S & ( for x being Element of T for y being Element of S holds ( y in U_FT x iff x in U_FT y ) ) ) ; end; :: deftheorem defines are_mutually_symmetric FINTOPO3:def_11_:_ for S, T being non empty RelStr holds ( S,T are_mutually_symmetric iff ( the carrier of S = the carrier of T & ( for x being Element of S for y being Element of T holds ( y in U_FT x iff x in U_FT y ) ) ) );