:: FINTOPO2 semantic presentation begin theorem :: FINTOPO2:1 for FT being non empty RelStr for A, B being Subset of FT st A c= B holds A ^i c= B ^i proof let FT be non empty RelStr ; ::_thesis: for A, B being Subset of FT st A c= B holds A ^i c= B ^i let A, B be Subset of FT; ::_thesis: ( A c= B implies A ^i c= B ^i ) assume A1: A c= B ; ::_thesis: A ^i c= B ^i let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^i or x in B ^i ) assume A2: x in A ^i ; ::_thesis: x in B ^i then reconsider y = x as Element of FT ; A3: U_FT y c= A by A2, FIN_TOPO:7; for t being Element of FT st t in U_FT y holds t in B proof let t be Element of FT; ::_thesis: ( t in U_FT y implies t in B ) assume t in U_FT y ; ::_thesis: t in B then t in A by A3; hence t in B by A1; ::_thesis: verum end; then U_FT y c= B by SUBSET_1:2; hence x in B ^i ; ::_thesis: verum end; theorem Th2: :: FINTOPO2:2 for FT being non empty RelStr for A being Subset of FT holds A ^delta = (A ^b) /\ ((A ^i) `) proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^delta = (A ^b) /\ ((A ^i) `) let A be Subset of FT; ::_thesis: A ^delta = (A ^b) /\ ((A ^i) `) for x being set holds ( x in A ^delta iff x in (A ^b) /\ ((A ^i) `) ) proof let x be set ; ::_thesis: ( x in A ^delta iff x in (A ^b) /\ ((A ^i) `) ) thus ( x in A ^delta implies x in (A ^b) /\ ((A ^i) `) ) ::_thesis: ( x in (A ^b) /\ ((A ^i) `) implies x in A ^delta ) proof assume A1: x in A ^delta ; ::_thesis: x in (A ^b) /\ ((A ^i) `) then reconsider y = x as Element of FT ; U_FT y meets A ` by A1, FIN_TOPO:5; then y in (((A `) ^b) `) ` ; then A2: y in (A ^i) ` by FIN_TOPO:17; U_FT y meets A by A1, FIN_TOPO:5; then y in A ^b ; hence x in (A ^b) /\ ((A ^i) `) by A2, XBOOLE_0:def_4; ::_thesis: verum end; assume A3: x in (A ^b) /\ ((A ^i) `) ; ::_thesis: x in A ^delta then reconsider y = x as Element of FT ; x in (A ^i) ` by A3, XBOOLE_0:def_4; then x in (((A `) ^b) `) ` by FIN_TOPO:17; then A4: U_FT y meets A ` by FIN_TOPO:8; x in A ^b by A3, XBOOLE_0:def_4; then U_FT y meets A by FIN_TOPO:8; hence x in A ^delta by A4; ::_thesis: verum end; hence A ^delta = (A ^b) /\ ((A ^i) `) by TARSKI:1; ::_thesis: verum end; theorem :: FINTOPO2:3 for FT being non empty RelStr for A being Subset of FT holds A ^delta = (A ^b) \ (A ^i) proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT holds A ^delta = (A ^b) \ (A ^i) let A be Subset of FT; ::_thesis: A ^delta = (A ^b) \ (A ^i) for x being set holds ( x in A ^delta iff x in (A ^b) \ (A ^i) ) proof let x be set ; ::_thesis: ( x in A ^delta iff x in (A ^b) \ (A ^i) ) thus ( x in A ^delta implies x in (A ^b) \ (A ^i) ) ::_thesis: ( x in (A ^b) \ (A ^i) implies x in A ^delta ) proof assume x in A ^delta ; ::_thesis: x in (A ^b) \ (A ^i) then x in (A ^b) /\ ((A ^i) `) by Th2; hence x in (A ^b) \ (A ^i) by SUBSET_1:13; ::_thesis: verum end; assume x in (A ^b) \ (A ^i) ; ::_thesis: x in A ^delta then x in (A ^b) /\ ((A ^i) `) by SUBSET_1:13; hence x in A ^delta by Th2; ::_thesis: verum end; hence A ^delta = (A ^b) \ (A ^i) by TARSKI:1; ::_thesis: verum end; theorem :: FINTOPO2:4 for FT being non empty RelStr for A being Subset of FT st A ` is open holds A is closed proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A ` is open holds A is closed let A be Subset of FT; ::_thesis: ( A ` is open implies A is closed ) assume A ` is open ; ::_thesis: A is closed then A1: A ` = (A `) ^i by FIN_TOPO:def_14; (A `) ^i = (((A `) `) ^b) ` by FIN_TOPO:17 .= (A ^b) ` ; then A = ((A ^b) `) ` by A1 .= A ^b ; hence A is closed by FIN_TOPO:def_15; ::_thesis: verum end; theorem :: FINTOPO2:5 for FT being non empty RelStr for A being Subset of FT st A ` is closed holds A is open proof let FT be non empty RelStr ; ::_thesis: for A being Subset of FT st A ` is closed holds A is open let A be Subset of FT; ::_thesis: ( A ` is closed implies A is open ) assume A ` is closed ; ::_thesis: A is open then A1: A ` = (A `) ^b by FIN_TOPO:def_15; (A `) ^b = (((A `) `) ^i) ` by FIN_TOPO:16 .= (A ^i) ` ; then A = ((A ^i) `) ` by A1 .= A ^i ; hence A is open by FIN_TOPO:def_14; ::_thesis: verum end; definition let FT be non empty RelStr ; let x, y be Element of FT; let A be Subset of FT; func P_1 (x,y,A) -> Element of BOOLEAN equals :Def1: :: FINTOPO2:def 1 TRUE if ( y in U_FT x & y in A ) otherwise FALSE ; correctness coherence ( ( y in U_FT x & y in A implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ) implies FALSE is Element of BOOLEAN ) ); consistency for b1 being Element of BOOLEAN holds verum; ; end; :: deftheorem Def1 defines P_1 FINTOPO2:def_1_:_ for FT being non empty RelStr for x, y being Element of FT for A being Subset of FT holds ( ( y in U_FT x & y in A implies P_1 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ) implies P_1 (x,y,A) = FALSE ) ); definition let FT be non empty RelStr ; let x, y be Element of FT; let A be Subset of FT; func P_2 (x,y,A) -> Element of BOOLEAN equals :Def2: :: FINTOPO2:def 2 TRUE if ( y in U_FT x & y in A ` ) otherwise FALSE ; correctness coherence ( ( y in U_FT x & y in A ` implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ` ) implies FALSE is Element of BOOLEAN ) ); consistency for b1 being Element of BOOLEAN holds verum; ; end; :: deftheorem Def2 defines P_2 FINTOPO2:def_2_:_ for FT being non empty RelStr for x, y being Element of FT for A being Subset of FT holds ( ( y in U_FT x & y in A ` implies P_2 (x,y,A) = TRUE ) & ( ( not y in U_FT x or not y in A ` ) implies P_2 (x,y,A) = FALSE ) ); theorem :: FINTOPO2:6 for FT being non empty RelStr for x, y being Element of FT for A being Subset of FT holds ( P_1 (x,y,A) = TRUE iff ( y in U_FT x & y in A ) ) by Def1; theorem :: FINTOPO2:7 for FT being non empty RelStr for x, y being Element of FT for A being Subset of FT holds ( P_2 (x,y,A) = TRUE iff ( y in U_FT x & y in A ` ) ) by Def2; theorem Th8: :: FINTOPO2:8 for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( x in A ^delta iff ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) ) proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT for A being Subset of FT holds ( x in A ^delta iff ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) ) let x be Element of FT; ::_thesis: for A being Subset of FT holds ( x in A ^delta iff ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) ) let A be Subset of FT; ::_thesis: ( x in A ^delta iff ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) ) A1: ( x in A ^delta implies ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) ) proof reconsider z = x as Element of FT ; assume A2: x in A ^delta ; ::_thesis: ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) then U_FT z meets A by FIN_TOPO:5; then consider w1 being set such that A3: w1 in U_FT z and A4: w1 in A by XBOOLE_0:3; reconsider w1 = w1 as Element of FT by A3; take w1 ; ::_thesis: ex y2 being Element of FT st ( P_1 (x,w1,A) = TRUE & P_2 (x,y2,A) = TRUE ) U_FT z meets A ` by A2, FIN_TOPO:5; then consider w2 being set such that A5: ( w2 in U_FT z & w2 in A ` ) by XBOOLE_0:3; take w2 ; ::_thesis: ( w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE ) thus ( w2 is Element of FT & P_1 (x,w1,A) = TRUE & P_2 (x,w2,A) = TRUE ) by A3, A4, A5, Def1, Def2; ::_thesis: verum end; ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) implies x in A ^delta ) proof given y1, y2 being Element of FT such that A6: P_1 (x,y1,A) = TRUE and A7: P_2 (x,y2,A) = TRUE ; ::_thesis: x in A ^delta ( y1 in U_FT x & y1 in A ) by A6, Def1; then (U_FT x) /\ A <> {} by XBOOLE_0:def_4; then A8: U_FT x meets A by XBOOLE_0:def_7; ( y2 in U_FT x & y2 in A ` ) by A7, Def2; then U_FT x meets A ` by XBOOLE_0:3; hence x in A ^delta by A8; ::_thesis: verum end; hence ( x in A ^delta iff ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) ) by A1; ::_thesis: verum end; definition let FT be non empty RelStr ; let x, y be Element of FT; func P_0 (x,y) -> Element of BOOLEAN equals :Def3: :: FINTOPO2:def 3 TRUE if y in U_FT x otherwise FALSE ; correctness coherence ( ( y in U_FT x implies TRUE is Element of BOOLEAN ) & ( not y in U_FT x implies FALSE is Element of BOOLEAN ) ); consistency for b1 being Element of BOOLEAN holds verum; ; end; :: deftheorem Def3 defines P_0 FINTOPO2:def_3_:_ for FT being non empty RelStr for x, y being Element of FT holds ( ( y in U_FT x implies P_0 (x,y) = TRUE ) & ( not y in U_FT x implies P_0 (x,y) = FALSE ) ); theorem :: FINTOPO2:9 for FT being non empty RelStr for x, y being Element of FT holds ( P_0 (x,y) = TRUE iff y in U_FT x ) by Def3; theorem :: FINTOPO2:10 for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds P_1 (x,y,A) = TRUE ) proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT for A being Subset of FT holds ( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds P_1 (x,y,A) = TRUE ) let x be Element of FT; ::_thesis: for A being Subset of FT holds ( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds P_1 (x,y,A) = TRUE ) let A be Subset of FT; ::_thesis: ( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds P_1 (x,y,A) = TRUE ) A1: ( ( for y being Element of FT st P_0 (x,y) = TRUE holds P_1 (x,y,A) = TRUE ) implies x in A ^i ) proof assume A2: for y being Element of FT st P_0 (x,y) = TRUE holds P_1 (x,y,A) = TRUE ; ::_thesis: x in A ^i for y being Element of FT st y in U_FT x holds ( y in U_FT x & y in A ) proof let y be Element of FT; ::_thesis: ( y in U_FT x implies ( y in U_FT x & y in A ) ) assume y in U_FT x ; ::_thesis: ( y in U_FT x & y in A ) then P_0 (x,y) = TRUE by Def3; then P_1 (x,y,A) = TRUE by A2; hence ( y in U_FT x & y in A ) by Def1; ::_thesis: verum end; then for y being Element of FT st y in U_FT x holds y in A ; then U_FT x c= A by SUBSET_1:2; hence x in A ^i ; ::_thesis: verum end; ( x in A ^i implies for y being Element of FT st P_0 (x,y) = TRUE holds P_1 (x,y,A) = TRUE ) proof assume x in A ^i ; ::_thesis: for y being Element of FT st P_0 (x,y) = TRUE holds P_1 (x,y,A) = TRUE then A3: U_FT x c= A by FIN_TOPO:7; let y be Element of FT; ::_thesis: ( P_0 (x,y) = TRUE implies P_1 (x,y,A) = TRUE ) assume P_0 (x,y) = TRUE ; ::_thesis: P_1 (x,y,A) = TRUE then y in U_FT x by Def3; hence P_1 (x,y,A) = TRUE by A3, Def1; ::_thesis: verum end; hence ( x in A ^i iff for y being Element of FT st P_0 (x,y) = TRUE holds P_1 (x,y,A) = TRUE ) by A1; ::_thesis: verum end; theorem :: FINTOPO2:11 for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE ) proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT for A being Subset of FT holds ( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE ) let x be Element of FT; ::_thesis: for A being Subset of FT holds ( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE ) let A be Subset of FT; ::_thesis: ( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE ) A1: ( x in A ^b implies ex y1 being Element of FT st P_1 (x,y1,A) = TRUE ) proof reconsider z = x as Element of FT ; assume x in A ^b ; ::_thesis: ex y1 being Element of FT st P_1 (x,y1,A) = TRUE then U_FT z meets A by FIN_TOPO:8; then consider w being set such that A2: w in U_FT z and A3: w in A by XBOOLE_0:3; reconsider w = w as Element of FT by A2; take w ; ::_thesis: P_1 (x,w,A) = TRUE thus P_1 (x,w,A) = TRUE by A2, A3, Def1; ::_thesis: verum end; ( ex y1 being Element of FT st P_1 (x,y1,A) = TRUE implies x in A ^b ) proof given y being Element of FT such that A4: P_1 (x,y,A) = TRUE ; ::_thesis: x in A ^b ( y in U_FT x & y in A ) by A4, Def1; then y in (U_FT x) /\ A by XBOOLE_0:def_4; then U_FT x meets A by XBOOLE_0:def_7; hence x in A ^b ; ::_thesis: verum end; hence ( x in A ^b iff ex y1 being Element of FT st P_1 (x,y1,A) = TRUE ) by A1; ::_thesis: verum end; definition let FT be non empty RelStr ; let x be Element of FT; let A be Subset of FT; func P_A (x,A) -> Element of BOOLEAN equals :Def4: :: FINTOPO2:def 4 TRUE if x in A otherwise FALSE ; correctness coherence ( ( x in A implies TRUE is Element of BOOLEAN ) & ( not x in A implies FALSE is Element of BOOLEAN ) ); consistency for b1 being Element of BOOLEAN holds verum; ; end; :: deftheorem Def4 defines P_A FINTOPO2:def_4_:_ for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( ( x in A implies P_A (x,A) = TRUE ) & ( not x in A implies P_A (x,A) = FALSE ) ); theorem :: FINTOPO2:12 for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( P_A (x,A) = TRUE iff x in A ) by Def4; theorem :: FINTOPO2:13 for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( x in A ^deltai iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) ) proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT for A being Subset of FT holds ( x in A ^deltai iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) ) let x be Element of FT; ::_thesis: for A being Subset of FT holds ( x in A ^deltai iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) ) let A be Subset of FT; ::_thesis: ( x in A ^deltai iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) ) A1: ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE implies x in A ^deltai ) proof assume ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) ; ::_thesis: x in A ^deltai then ( x in A ^delta & x in A ) by Def4, Th8; hence x in A ^deltai by XBOOLE_0:def_4; ::_thesis: verum end; ( x in A ^deltai implies ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) ) proof assume x in A ^deltai ; ::_thesis: ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) then ( x in A & x in A ^delta ) by XBOOLE_0:def_4; hence ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) by Def4, Th8; ::_thesis: verum end; hence ( x in A ^deltai iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = TRUE ) ) by A1; ::_thesis: verum end; theorem :: FINTOPO2:14 for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( x in A ^deltao iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) ) proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT for A being Subset of FT holds ( x in A ^deltao iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) ) let x be Element of FT; ::_thesis: for A being Subset of FT holds ( x in A ^deltao iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) ) let A be Subset of FT; ::_thesis: ( x in A ^deltao iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) ) A1: ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE implies x in A ^deltao ) proof assume that A2: ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) and A3: P_A (x,A) = FALSE ; ::_thesis: x in A ^deltao not x in A by A3, Def4; then A4: x in A ` by XBOOLE_0:def_5; x in A ^delta by A2, Th8; hence x in A ^deltao by A4, XBOOLE_0:def_4; ::_thesis: verum end; ( x in A ^deltao implies ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) ) proof assume A5: x in A ^deltao ; ::_thesis: ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) then x in A ` by XBOOLE_0:def_4; then A6: not x in A by XBOOLE_0:def_5; x in A ^delta by A5, XBOOLE_0:def_4; hence ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) by A6, Def4, Th8; ::_thesis: verum end; hence ( x in A ^deltao iff ( ex y1, y2 being Element of FT st ( P_1 (x,y1,A) = TRUE & P_2 (x,y2,A) = TRUE ) & P_A (x,A) = FALSE ) ) by A1; ::_thesis: verum end; definition let FT be non empty RelStr ; let x, y be Element of FT; func P_e (x,y) -> Element of BOOLEAN equals :Def5: :: FINTOPO2:def 5 TRUE if x = y otherwise FALSE ; correctness coherence ( ( x = y implies TRUE is Element of BOOLEAN ) & ( not x = y implies FALSE is Element of BOOLEAN ) ); consistency for b1 being Element of BOOLEAN holds verum; ; end; :: deftheorem Def5 defines P_e FINTOPO2:def_5_:_ for FT being non empty RelStr for x, y being Element of FT holds ( ( x = y implies P_e (x,y) = TRUE ) & ( not x = y implies P_e (x,y) = FALSE ) ); theorem :: FINTOPO2:15 for FT being non empty RelStr for x, y being Element of FT holds ( P_e (x,y) = TRUE iff x = y ) by Def5; theorem :: FINTOPO2:16 for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) ) proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT for A being Subset of FT holds ( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) ) let x be Element of FT; ::_thesis: for A being Subset of FT holds ( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) ) let A be Subset of FT; ::_thesis: ( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) ) A1: ( x in A ^s implies ( P_A (x,A) = TRUE & ( for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) ) proof assume A2: x in A ^s ; ::_thesis: ( P_A (x,A) = TRUE & ( for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) then (U_FT x) \ {x} misses A by FIN_TOPO:9; then A3: ((U_FT x) \ {x}) /\ A = {} by XBOOLE_0:def_7; A4: for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) proof given y being Element of FT such that A5: P_1 (x,y,A) = TRUE and A6: P_e (x,y) = FALSE ; ::_thesis: contradiction not x = y by A6, Def5; then A7: not y in {x} by TARSKI:def_1; y in U_FT x by A5, Def1; then A8: y in (U_FT x) \ {x} by A7, XBOOLE_0:def_5; y in A by A5, Def1; hence contradiction by A3, A8, XBOOLE_0:def_4; ::_thesis: verum end; x in A by A2, FIN_TOPO:9; hence ( P_A (x,A) = TRUE & ( for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) by A4, Def4; ::_thesis: verum end; ( P_A (x,A) = TRUE & ( for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) implies x in A ^s ) proof assume that A9: P_A (x,A) = TRUE and A10: for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ; ::_thesis: x in A ^s for y being Element of FT holds not y in ((U_FT x) \ {x}) /\ A proof let y be Element of FT; ::_thesis: not y in ((U_FT x) \ {x}) /\ A ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) by A10; then ( not y in U_FT x or x = y or not y in A ) by Def1, Def5; then ( not y in U_FT x or y in {x} or not y in A ) by TARSKI:def_1; then ( not y in (U_FT x) \ {x} or not y in A ) by XBOOLE_0:def_5; hence not y in ((U_FT x) \ {x}) /\ A by XBOOLE_0:def_4; ::_thesis: verum end; then ((U_FT x) \ {x}) /\ A = {} by SUBSET_1:4; then A11: (U_FT x) \ {x} misses A by XBOOLE_0:def_7; x in A by A9, Def4; hence x in A ^s by A11; ::_thesis: verum end; hence ( x in A ^s iff ( P_A (x,A) = TRUE & ( for y being Element of FT holds ( not P_1 (x,y,A) = TRUE or not P_e (x,y) = FALSE ) ) ) ) by A1; ::_thesis: verum end; theorem :: FINTOPO2:17 for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) ) proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT for A being Subset of FT holds ( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) ) let x be Element of FT; ::_thesis: for A being Subset of FT holds ( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) ) let A be Subset of FT; ::_thesis: ( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) ) A1: ( x in A ^n implies ( P_A (x,A) = TRUE & ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) ) proof assume A2: x in A ^n ; ::_thesis: ( P_A (x,A) = TRUE & ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) then (U_FT x) \ {x} meets A by FIN_TOPO:10; then ((U_FT x) \ {x}) /\ A <> {} by XBOOLE_0:def_7; then consider y being Element of FT such that A3: y in ((U_FT x) \ {x}) /\ A by SUBSET_1:4; A4: y in (U_FT x) \ {x} by A3, XBOOLE_0:def_4; then A5: y in U_FT x by XBOOLE_0:def_5; not y in {x} by A4, XBOOLE_0:def_5; then not x = y by TARSKI:def_1; then A6: P_e (x,y) = FALSE by Def5; y in A by A3, XBOOLE_0:def_4; then A7: P_1 (x,y,A) = TRUE by A5, Def1; x in A by A2, FIN_TOPO:10; hence ( P_A (x,A) = TRUE & ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) by A6, A7, Def4; ::_thesis: verum end; ( P_A (x,A) = TRUE & ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) implies x in A ^n ) proof assume that A8: P_A (x,A) = TRUE and A9: ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ; ::_thesis: x in A ^n consider y being Element of FT such that A10: P_1 (x,y,A) = TRUE and A11: P_e (x,y) = FALSE by A9; x <> y by A11, Def5; then A12: not y in {x} by TARSKI:def_1; y in U_FT x by A10, Def1; then A13: y in (U_FT x) \ {x} by A12, XBOOLE_0:def_5; y in A by A10, Def1; then A14: (U_FT x) \ {x} meets A by A13, XBOOLE_0:3; x in A by A8, Def4; hence x in A ^n by A14, FIN_TOPO:10; ::_thesis: verum end; hence ( x in A ^n iff ( P_A (x,A) = TRUE & ex y being Element of FT st ( P_1 (x,y,A) = TRUE & P_e (x,y) = FALSE ) ) ) by A1; ::_thesis: verum end; theorem :: FINTOPO2:18 for FT being non empty RelStr for x being Element of FT for A being Subset of FT holds ( x in A ^f iff ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ) proof let FT be non empty RelStr ; ::_thesis: for x being Element of FT for A being Subset of FT holds ( x in A ^f iff ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ) let x be Element of FT; ::_thesis: for A being Subset of FT holds ( x in A ^f iff ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ) let A be Subset of FT; ::_thesis: ( x in A ^f iff ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ) A1: ( ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) implies x in A ^f ) proof assume ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ; ::_thesis: x in A ^f then consider y being Element of FT such that A2: ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ; ( y in A & x in U_FT y ) by A2, Def3, Def4; hence x in A ^f ; ::_thesis: verum end; ( x in A ^f implies ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ) proof assume x in A ^f ; ::_thesis: ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) then consider y being Element of FT such that A3: ( y in A & x in U_FT y ) by FIN_TOPO:11; ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) by A3, Def3, Def4; hence ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ; ::_thesis: verum end; hence ( x in A ^f iff ex y being Element of FT st ( P_A (y,A) = TRUE & P_0 (y,x) = TRUE ) ) by A1; ::_thesis: verum end; begin definition attrc1 is strict ; struct FMT_Space_Str -> 1-sorted ; aggrFMT_Space_Str(# carrier, BNbd #) -> FMT_Space_Str ; sel BNbd c1 -> Function of the carrier of c1,(bool (bool the carrier of c1)); end; registration cluster non empty strict for FMT_Space_Str ; existence ex b1 being FMT_Space_Str st ( not b1 is empty & b1 is strict ) proof set D = the non empty set ; set f = the Function of the non empty set ,(bool (bool the non empty set )); take FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) ; ::_thesis: ( not FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is empty & FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is strict ) thus not the carrier of FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is strict thus FMT_Space_Str(# the non empty set , the Function of the non empty set ,(bool (bool the non empty set )) #) is strict ; ::_thesis: verum end; end; definition let FMT be non empty FMT_Space_Str ; let x be Element of FMT; func U_FMT x -> Subset-Family of FMT equals :: FINTOPO2:def 6 the BNbd of FMT . x; correctness coherence the BNbd of FMT . x is Subset-Family of FMT; ; end; :: deftheorem defines U_FMT FINTOPO2:def_6_:_ for FMT being non empty FMT_Space_Str for x being Element of FMT holds U_FMT x = the BNbd of FMT . x; definition let T be non empty TopStruct ; func NeighSp T -> non empty strict FMT_Space_Str means :: FINTOPO2:def 7 ( the carrier of it = the carrier of T & ( for x being Point of it holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ); existence ex b1 being non empty strict FMT_Space_Str st ( the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) proof ex IT being non empty strict FMT_Space_Str st ( the carrier of IT = the carrier of T & ( for x being Point of IT holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) proof deffunc H1( set ) -> set = { V where V is Subset of T : ( V in the topology of T & $1 in V ) } ; A1: for x being Element of T holds H1(x) in bool (bool the carrier of T) proof let x be Element of T; ::_thesis: H1(x) in bool (bool the carrier of T) now__::_thesis:_for_Y_being_set_st_Y_in__{__V_where_V_is_Subset_of_T_:_(_V_in_the_topology_of_T_&_x_in_V_)__}__holds_ Y_in_bool_the_carrier_of_T let Y be set ; ::_thesis: ( Y in { V where V is Subset of T : ( V in the topology of T & x in V ) } implies Y in bool the carrier of T ) assume Y in { V where V is Subset of T : ( V in the topology of T & x in V ) } ; ::_thesis: Y in bool the carrier of T then ex V being Subset of T st ( V = Y & V in the topology of T & x in V ) ; hence Y in bool the carrier of T ; ::_thesis: verum end; then { V where V is Subset of T : ( V in the topology of T & x in V ) } c= bool the carrier of T by TARSKI:def_3; hence H1(x) in bool (bool the carrier of T) ; ::_thesis: verum end; consider f being Function of the carrier of T,(bool (bool the carrier of T)) such that A2: for x being Element of T holds f . x = H1(x) from FUNCT_2:sch_8(A1); reconsider IT = FMT_Space_Str(# the carrier of T,f #) as non empty strict FMT_Space_Str ; take IT ; ::_thesis: ( the carrier of IT = the carrier of T & ( for x being Point of IT holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) thus ( the carrier of IT = the carrier of T & ( for x being Point of IT holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) by A2; ::_thesis: verum end; hence ex b1 being non empty strict FMT_Space_Str st ( the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict FMT_Space_Str st the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) & the carrier of b2 = the carrier of T & ( for x being Point of b2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) holds b1 = b2 proof let it1, it2 be non empty strict FMT_Space_Str ; ::_thesis: ( the carrier of it1 = the carrier of T & ( for x being Point of it1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) & the carrier of it2 = the carrier of T & ( for x being Point of it2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) implies it1 = it2 ) assume that A3: the carrier of it1 = the carrier of T and A4: for x being Point of it1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } and A5: the carrier of it2 = the carrier of T and A6: for x being Point of it2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ; ::_thesis: it1 = it2 A7: for x being Element of it2 holds the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } proof let x be Element of it2; ::_thesis: the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } the BNbd of it2 . x = U_FMT x ; hence the BNbd of it2 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A6; ::_thesis: verum end; A8: for x being Element of it1 holds the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } proof let x be Element of it1; ::_thesis: the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } the BNbd of it1 . x = U_FMT x ; hence the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A4; ::_thesis: verum end; now__::_thesis:_for_x_being_Point_of_it1_holds_the_BNbd_of_it1_._x_=_the_BNbd_of_it2_._x let x be Point of it1; ::_thesis: the BNbd of it1 . x = the BNbd of it2 . x thus the BNbd of it1 . x = { V where V is Subset of T : ( V in the topology of T & x in V ) } by A8 .= the BNbd of it2 . x by A3, A5, A7 ; ::_thesis: verum end; hence it1 = it2 by A3, A5, FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem defines NeighSp FINTOPO2:def_7_:_ for T being non empty TopStruct for b2 being non empty strict FMT_Space_Str holds ( b2 = NeighSp T iff ( the carrier of b2 = the carrier of T & ( for x being Point of b2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) ); definition let IT be non empty FMT_Space_Str ; attrIT is Fo_filled means :Def8: :: FINTOPO2:def 8 for x being Element of IT for D being Subset of IT st D in U_FMT x holds x in D; end; :: deftheorem Def8 defines Fo_filled FINTOPO2:def_8_:_ for IT being non empty FMT_Space_Str holds ( IT is Fo_filled iff for x being Element of IT for D being Subset of IT st D in U_FMT x holds x in D ); definition let FMT be non empty FMT_Space_Str ; let A be Subset of FMT; funcA ^Fodelta -> Subset of FMT equals :: FINTOPO2:def 9 { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) } ; coherence { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) } is Subset of FMT proof defpred S1[ Element of FMT] means for W being Subset of FMT st W in U_FMT $1 holds ( W meets A & W meets A ` ); { x where x is Element of FMT : S1[x] } is Subset of FMT from DOMAIN_1:sch_7(); hence { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) } is Subset of FMT ; ::_thesis: verum end; end; :: deftheorem defines ^Fodelta FINTOPO2:def_9_:_ for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fodelta = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) } ; theorem Th19: :: FINTOPO2:19 for FMT being non empty FMT_Space_Str for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) ) let x be Element of FMT; ::_thesis: for A being Subset of FMT holds ( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) ) let A be Subset of FMT; ::_thesis: ( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) ) thus ( x in A ^Fodelta implies for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) ) ::_thesis: ( ( for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) ) implies x in A ^Fodelta ) proof assume x in A ^Fodelta ; ::_thesis: for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) then ex y being Element of FMT st ( y = x & ( for W being Subset of FMT st W in U_FMT y holds ( W meets A & W meets A ` ) ) ) ; hence for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) ; ::_thesis: verum end; assume for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) ; ::_thesis: x in A ^Fodelta hence x in A ^Fodelta ; ::_thesis: verum end; definition let FMT be non empty FMT_Space_Str ; let A be Subset of FMT; funcA ^Fob -> Subset of FMT equals :: FINTOPO2:def 10 { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds W meets A } ; coherence { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds W meets A } is Subset of FMT proof defpred S1[ Element of FMT] means for W being Subset of FMT st W in U_FMT $1 holds W meets A; { x where x is Element of FMT : S1[x] } is Subset of FMT from DOMAIN_1:sch_7(); hence { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds W meets A } is Subset of FMT ; ::_thesis: verum end; end; :: deftheorem defines ^Fob FINTOPO2:def_10_:_ for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fob = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds W meets A } ; theorem Th20: :: FINTOPO2:20 for FMT being non empty FMT_Space_Str for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds W meets A ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds W meets A ) let x be Element of FMT; ::_thesis: for A being Subset of FMT holds ( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds W meets A ) let A be Subset of FMT; ::_thesis: ( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds W meets A ) thus ( x in A ^Fob implies for W being Subset of FMT st W in U_FMT x holds W meets A ) ::_thesis: ( ( for W being Subset of FMT st W in U_FMT x holds W meets A ) implies x in A ^Fob ) proof assume x in A ^Fob ; ::_thesis: for W being Subset of FMT st W in U_FMT x holds W meets A then ex y being Element of FMT st ( y = x & ( for W being Subset of FMT st W in U_FMT y holds W meets A ) ) ; hence for W being Subset of FMT st W in U_FMT x holds W meets A ; ::_thesis: verum end; assume for W being Subset of FMT st W in U_FMT x holds W meets A ; ::_thesis: x in A ^Fob hence x in A ^Fob ; ::_thesis: verum end; definition let FMT be non empty FMT_Space_Str ; let A be Subset of FMT; funcA ^Foi -> Subset of FMT equals :: FINTOPO2:def 11 { x where x is Element of FMT : ex V being Subset of FMT st ( V in U_FMT x & V c= A ) } ; coherence { x where x is Element of FMT : ex V being Subset of FMT st ( V in U_FMT x & V c= A ) } is Subset of FMT proof defpred S1[ Element of FMT] means ex V being Subset of FMT st ( V in U_FMT $1 & V c= A ); { x where x is Element of FMT : S1[x] } is Subset of FMT from DOMAIN_1:sch_7(); hence { x where x is Element of FMT : ex V being Subset of FMT st ( V in U_FMT x & V c= A ) } is Subset of FMT ; ::_thesis: verum end; end; :: deftheorem defines ^Foi FINTOPO2:def_11_:_ for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Foi = { x where x is Element of FMT : ex V being Subset of FMT st ( V in U_FMT x & V c= A ) } ; theorem Th21: :: FINTOPO2:21 for FMT being non empty FMT_Space_Str for x being Element of FMT for A being Subset of FMT holds ( x in A ^Foi iff ex V being Subset of FMT st ( V in U_FMT x & V c= A ) ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT for A being Subset of FMT holds ( x in A ^Foi iff ex V being Subset of FMT st ( V in U_FMT x & V c= A ) ) let x be Element of FMT; ::_thesis: for A being Subset of FMT holds ( x in A ^Foi iff ex V being Subset of FMT st ( V in U_FMT x & V c= A ) ) let A be Subset of FMT; ::_thesis: ( x in A ^Foi iff ex V being Subset of FMT st ( V in U_FMT x & V c= A ) ) thus ( x in A ^Foi implies ex V being Subset of FMT st ( V in U_FMT x & V c= A ) ) ::_thesis: ( ex V being Subset of FMT st ( V in U_FMT x & V c= A ) implies x in A ^Foi ) proof assume x in A ^Foi ; ::_thesis: ex V being Subset of FMT st ( V in U_FMT x & V c= A ) then ex y being Element of FMT st ( y = x & ex V being Subset of FMT st ( V in U_FMT y & V c= A ) ) ; hence ex V being Subset of FMT st ( V in U_FMT x & V c= A ) ; ::_thesis: verum end; assume ex V being Subset of FMT st ( V in U_FMT x & V c= A ) ; ::_thesis: x in A ^Foi hence x in A ^Foi ; ::_thesis: verum end; definition let FMT be non empty FMT_Space_Str ; let A be Subset of FMT; funcA ^Fos -> Subset of FMT equals :: FINTOPO2:def 12 { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) } ; coherence { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) } is Subset of FMT proof defpred S1[ Element of FMT] means ( $1 in A & ex V being Subset of FMT st ( V in U_FMT $1 & V \ {$1} misses A ) ); { x where x is Element of FMT : S1[x] } is Subset of FMT from DOMAIN_1:sch_7(); hence { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) } is Subset of FMT ; ::_thesis: verum end; end; :: deftheorem defines ^Fos FINTOPO2:def_12_:_ for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fos = { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) } ; theorem Th22: :: FINTOPO2:22 for FMT being non empty FMT_Space_Str for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fos iff ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fos iff ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) ) let x be Element of FMT; ::_thesis: for A being Subset of FMT holds ( x in A ^Fos iff ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) ) let A be Subset of FMT; ::_thesis: ( x in A ^Fos iff ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) ) thus ( x in A ^Fos implies ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) ) ::_thesis: ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) implies x in A ^Fos ) proof assume x in A ^Fos ; ::_thesis: ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) then ex y being Element of FMT st ( y = x & y in A & ex V being Subset of FMT st ( V in U_FMT y & V \ {y} misses A ) ) ; hence ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) ; ::_thesis: verum end; assume ( x in A & ex V being Subset of FMT st ( V in U_FMT x & V \ {x} misses A ) ) ; ::_thesis: x in A ^Fos hence x in A ^Fos ; ::_thesis: verum end; definition let FMT be non empty FMT_Space_Str ; let A be Subset of FMT; funcA ^Fon -> Subset of FMT equals :: FINTOPO2:def 13 A \ (A ^Fos); coherence A \ (A ^Fos) is Subset of FMT ; end; :: deftheorem defines ^Fon FINTOPO2:def_13_:_ for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fon = A \ (A ^Fos); theorem :: FINTOPO2:23 for FMT being non empty FMT_Space_Str for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds V \ {x} meets A ) ) ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds V \ {x} meets A ) ) ) let x be Element of FMT; ::_thesis: for A being Subset of FMT holds ( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds V \ {x} meets A ) ) ) let A be Subset of FMT; ::_thesis: ( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds V \ {x} meets A ) ) ) thus ( x in A ^Fon implies ( x in A & ( for V being Subset of FMT st V in U_FMT x holds V \ {x} meets A ) ) ) ::_thesis: ( x in A & ( for V being Subset of FMT st V in U_FMT x holds V \ {x} meets A ) implies x in A ^Fon ) proof assume x in A ^Fon ; ::_thesis: ( x in A & ( for V being Subset of FMT st V in U_FMT x holds V \ {x} meets A ) ) then ( x in A & not x in A ^Fos ) by XBOOLE_0:def_5; hence ( x in A & ( for V being Subset of FMT st V in U_FMT x holds V \ {x} meets A ) ) ; ::_thesis: verum end; assume that A1: x in A and A2: for V being Subset of FMT st V in U_FMT x holds V \ {x} meets A ; ::_thesis: x in A ^Fon not x in A ^Fos by A2, Th22; hence x in A ^Fon by A1, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th24: :: FINTOPO2:24 for FMT being non empty FMT_Space_Str for A, B being Subset of FMT st A c= B holds A ^Fob c= B ^Fob proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st A c= B holds A ^Fob c= B ^Fob let A, B be Subset of FMT; ::_thesis: ( A c= B implies A ^Fob c= B ^Fob ) assume A1: A c= B ; ::_thesis: A ^Fob c= B ^Fob let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^Fob or x in B ^Fob ) assume A2: x in A ^Fob ; ::_thesis: x in B ^Fob then reconsider y = x as Element of FMT ; for W being Subset of FMT st W in U_FMT y holds W meets B proof let W be Subset of FMT; ::_thesis: ( W in U_FMT y implies W meets B ) assume W in U_FMT y ; ::_thesis: W meets B then W meets A by A2, Th20; then ex z being set st ( z in W & z in A ) by XBOOLE_0:3; hence W /\ B <> {} by A1, XBOOLE_0:def_4; :: according to XBOOLE_0:def_7 ::_thesis: verum end; hence x in B ^Fob ; ::_thesis: verum end; theorem Th25: :: FINTOPO2:25 for FMT being non empty FMT_Space_Str for A, B being Subset of FMT st A c= B holds A ^Foi c= B ^Foi proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st A c= B holds A ^Foi c= B ^Foi let A, B be Subset of FMT; ::_thesis: ( A c= B implies A ^Foi c= B ^Foi ) assume A1: A c= B ; ::_thesis: A ^Foi c= B ^Foi let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^Foi or x in B ^Foi ) assume A2: x in A ^Foi ; ::_thesis: x in B ^Foi then reconsider y = x as Element of FMT ; consider V9 being Subset of FMT such that A3: V9 in U_FMT y and A4: V9 c= A by A2, Th21; V9 c= B by A1, A4, XBOOLE_1:1; hence x in B ^Foi by A3; ::_thesis: verum end; theorem Th26: :: FINTOPO2:26 for FMT being non empty FMT_Space_Str for A, B being Subset of FMT holds (A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT holds (A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob let A, B be Subset of FMT; ::_thesis: (A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^Fob) \/ (B ^Fob) or x in (A \/ B) ^Fob ) assume x in (A ^Fob) \/ (B ^Fob) ; ::_thesis: x in (A \/ B) ^Fob then A1: ( x in A ^Fob or x in B ^Fob ) by XBOOLE_0:def_3; ( A ^Fob c= (A \/ B) ^Fob & B ^Fob c= (B \/ A) ^Fob ) by Th24, XBOOLE_1:7; hence x in (A \/ B) ^Fob by A1; ::_thesis: verum end; theorem :: FINTOPO2:27 for FMT being non empty FMT_Space_Str for A, B being Subset of FMT holds (A /\ B) ^Fob c= (A ^Fob) /\ (B ^Fob) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT holds (A /\ B) ^Fob c= (A ^Fob) /\ (B ^Fob) let A, B be Subset of FMT; ::_thesis: (A /\ B) ^Fob c= (A ^Fob) /\ (B ^Fob) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) ^Fob or x in (A ^Fob) /\ (B ^Fob) ) assume A1: x in (A /\ B) ^Fob ; ::_thesis: x in (A ^Fob) /\ (B ^Fob) ( (A /\ B) ^Fob c= A ^Fob & (B /\ A) ^Fob c= B ^Fob ) by Th24, XBOOLE_1:17; hence x in (A ^Fob) /\ (B ^Fob) by A1, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: FINTOPO2:28 for FMT being non empty FMT_Space_Str for A, B being Subset of FMT holds (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT holds (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi let A, B be Subset of FMT; ::_thesis: (A ^Foi) \/ (B ^Foi) c= (A \/ B) ^Foi let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^Foi) \/ (B ^Foi) or x in (A \/ B) ^Foi ) assume x in (A ^Foi) \/ (B ^Foi) ; ::_thesis: x in (A \/ B) ^Foi then A1: ( x in A ^Foi or x in B ^Foi ) by XBOOLE_0:def_3; ( A ^Foi c= (A \/ B) ^Foi & B ^Foi c= (B \/ A) ^Foi ) by Th25, XBOOLE_1:7; hence x in (A \/ B) ^Foi by A1; ::_thesis: verum end; theorem Th29: :: FINTOPO2:29 for FMT being non empty FMT_Space_Str for A, B being Subset of FMT holds (A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT holds (A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi) let A, B be Subset of FMT; ::_thesis: (A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) ^Foi or x in (A ^Foi) /\ (B ^Foi) ) assume A1: x in (A /\ B) ^Foi ; ::_thesis: x in (A ^Foi) /\ (B ^Foi) ( (A /\ B) ^Foi c= A ^Foi & (B /\ A) ^Foi c= B ^Foi ) by Th25, XBOOLE_1:17; hence x in (A ^Foi) /\ (B ^Foi) by A1, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: FINTOPO2:30 for FMT being non empty FMT_Space_Str holds ( ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: ( ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) ) A1: ( ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) implies for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) ) proof assume A2: for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ; ::_thesis: for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) let A, B be Subset of FMT; ::_thesis: (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) for x being Element of FMT holds ( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) ) proof let x be Element of FMT; ::_thesis: ( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) ) A3: ( x in (A \/ B) ^Fob implies x in (A ^Fob) \/ (B ^Fob) ) proof assume A4: x in (A \/ B) ^Fob ; ::_thesis: x in (A ^Fob) \/ (B ^Fob) A5: for W1 being Subset of FMT holds ( not W1 in U_FMT x or W1 meets A or W1 meets B ) proof let W1 be Subset of FMT; ::_thesis: ( not W1 in U_FMT x or W1 meets A or W1 meets B ) assume W1 in U_FMT x ; ::_thesis: ( W1 meets A or W1 meets B ) then W1 meets A \/ B by A4, Th20; then W1 /\ (A \/ B) <> {} by XBOOLE_0:def_7; then (W1 /\ A) \/ (W1 /\ B) <> {} by XBOOLE_1:23; then ( W1 /\ A <> {} or W1 /\ B <> {} ) ; hence ( W1 meets A or W1 meets B ) by XBOOLE_0:def_7; ::_thesis: verum end; for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x & not V1 meets A holds V2 meets B proof let V1, V2 be Subset of FMT; ::_thesis: ( V1 in U_FMT x & V2 in U_FMT x & not V1 meets A implies V2 meets B ) assume ( V1 in U_FMT x & V2 in U_FMT x ) ; ::_thesis: ( V1 meets A or V2 meets B ) then consider W being Subset of FMT such that A6: W in U_FMT x and A7: W c= V1 /\ V2 by A2; V1 /\ V2 c= V1 by XBOOLE_1:17; then W c= V1 by A7, XBOOLE_1:1; then A8: W /\ A c= V1 /\ A by XBOOLE_1:26; V1 /\ V2 c= V2 by XBOOLE_1:17; then W c= V2 by A7, XBOOLE_1:1; then A9: W /\ B c= V2 /\ B by XBOOLE_1:26; ( W meets A or W meets B ) by A5, A6; then ( W /\ A <> {} or W /\ B <> {} ) by XBOOLE_0:def_7; then ex z1, z2 being Element of FMT st ( z1 in W /\ A or z2 in W /\ B ) by SUBSET_1:4; hence ( V1 meets A or V2 meets B ) by A8, A9, XBOOLE_0:def_7; ::_thesis: verum end; then ( for V1 being Subset of FMT st V1 in U_FMT x holds V1 meets A or for V2 being Subset of FMT st V2 in U_FMT x holds V2 meets B ) ; then ( x in A ^Fob or x in B ^Fob ) ; hence x in (A ^Fob) \/ (B ^Fob) by XBOOLE_0:def_3; ::_thesis: verum end; ( x in (A ^Fob) \/ (B ^Fob) implies x in (A \/ B) ^Fob ) proof assume A10: x in (A ^Fob) \/ (B ^Fob) ; ::_thesis: x in (A \/ B) ^Fob (A ^Fob) \/ (B ^Fob) c= (A \/ B) ^Fob by Th26; hence x in (A \/ B) ^Fob by A10; ::_thesis: verum end; hence ( x in (A \/ B) ^Fob iff x in (A ^Fob) \/ (B ^Fob) ) by A3; ::_thesis: verum end; hence (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) by SUBSET_1:3; ::_thesis: verum end; ( ex x being Element of FMT ex V1, V2 being Subset of FMT st ( V1 in U_FMT x & V2 in U_FMT x & ( for W being Subset of FMT st W in U_FMT x holds not W c= V1 /\ V2 ) ) implies ex A, B being Subset of FMT st (A \/ B) ^Fob <> (A ^Fob) \/ (B ^Fob) ) proof given x0 being Element of FMT, V1, V2 being Subset of FMT such that A11: V1 in U_FMT x0 and A12: V2 in U_FMT x0 and A13: for W being Subset of FMT st W in U_FMT x0 holds not W c= V1 /\ V2 ; ::_thesis: ex A, B being Subset of FMT st (A \/ B) ^Fob <> (A ^Fob) \/ (B ^Fob) A14: not x0 in (V2 `) ^Fob proof A15: V2 misses V2 ` by XBOOLE_1:79; assume x0 in (V2 `) ^Fob ; ::_thesis: contradiction hence contradiction by A12, A15, Th20; ::_thesis: verum end; take V1 ` ; ::_thesis: ex B being Subset of FMT st ((V1 `) \/ B) ^Fob <> ((V1 `) ^Fob) \/ (B ^Fob) take V2 ` ; ::_thesis: ((V1 `) \/ (V2 `)) ^Fob <> ((V1 `) ^Fob) \/ ((V2 `) ^Fob) for W being Subset of FMT st W in U_FMT x0 holds W meets (V1 `) \/ (V2 `) proof let W be Subset of FMT; ::_thesis: ( W in U_FMT x0 implies W meets (V1 `) \/ (V2 `) ) assume W in U_FMT x0 ; ::_thesis: W meets (V1 `) \/ (V2 `) then A16: not W c= V1 /\ V2 by A13; W /\ ((V1 /\ V2) `) <> {} proof assume W /\ ((V1 /\ V2) `) = {} ; ::_thesis: contradiction then W \ (V1 /\ V2) = {} by SUBSET_1:13; hence contradiction by A16, XBOOLE_1:37; ::_thesis: verum end; hence W /\ ((V1 `) \/ (V2 `)) <> {} by XBOOLE_1:54; :: according to XBOOLE_0:def_7 ::_thesis: verum end; then A17: x0 in ((V1 `) \/ (V2 `)) ^Fob ; not x0 in (V1 `) ^Fob proof A18: V1 misses V1 ` by XBOOLE_1:79; assume x0 in (V1 `) ^Fob ; ::_thesis: contradiction hence contradiction by A11, A18, Th20; ::_thesis: verum end; hence ((V1 `) \/ (V2 `)) ^Fob <> ((V1 `) ^Fob) \/ ((V2 `) ^Fob) by A17, A14, XBOOLE_0:def_3; ::_thesis: verum end; hence ( ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob) \/ (B ^Fob) ) by A1; ::_thesis: verum end; theorem :: FINTOPO2:31 for FMT being non empty FMT_Space_Str holds ( ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: ( ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi ) thus ( ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) implies for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi ) ::_thesis: ( ( for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi ) implies for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) proof assume A1: for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ; ::_thesis: for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi let A, B be Subset of FMT; ::_thesis: (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi for x being Element of FMT holds ( x in (A ^Foi) /\ (B ^Foi) iff x in (A /\ B) ^Foi ) proof let x be Element of FMT; ::_thesis: ( x in (A ^Foi) /\ (B ^Foi) iff x in (A /\ B) ^Foi ) A2: ( x in (A ^Foi) /\ (B ^Foi) implies x in (A /\ B) ^Foi ) proof assume A3: x in (A ^Foi) /\ (B ^Foi) ; ::_thesis: x in (A /\ B) ^Foi then x in B ^Foi by XBOOLE_0:def_4; then A4: ex W2 being Subset of FMT st ( W2 in U_FMT x & W2 c= B ) by Th21; x in A ^Foi by A3, XBOOLE_0:def_4; then ex W1 being Subset of FMT st ( W1 in U_FMT x & W1 c= A ) by Th21; then consider W1, W2 being Subset of FMT such that A5: ( W1 in U_FMT x & W2 in U_FMT x ) and A6: W1 c= A and A7: W2 c= B by A4; consider W being Subset of FMT such that A8: W in U_FMT x and A9: W c= W1 /\ W2 by A1, A5; W1 /\ W2 c= W2 by XBOOLE_1:17; then W c= W2 by A9, XBOOLE_1:1; then A10: W c= B by A7, XBOOLE_1:1; W1 /\ W2 c= W1 by XBOOLE_1:17; then W c= W1 by A9, XBOOLE_1:1; then W c= A by A6, XBOOLE_1:1; then W c= A /\ B by A10, XBOOLE_1:19; hence x in (A /\ B) ^Foi by A8; ::_thesis: verum end; ( x in (A /\ B) ^Foi implies x in (A ^Foi) /\ (B ^Foi) ) proof assume A11: x in (A /\ B) ^Foi ; ::_thesis: x in (A ^Foi) /\ (B ^Foi) (A /\ B) ^Foi c= (A ^Foi) /\ (B ^Foi) by Th29; hence x in (A ^Foi) /\ (B ^Foi) by A11; ::_thesis: verum end; hence ( x in (A ^Foi) /\ (B ^Foi) iff x in (A /\ B) ^Foi ) by A2; ::_thesis: verum end; hence (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi by SUBSET_1:3; ::_thesis: verum end; ( ex x being Element of FMT ex V1, V2 being Subset of FMT st ( V1 in U_FMT x & V2 in U_FMT x & ( for W being Subset of FMT st W in U_FMT x holds not W c= V1 /\ V2 ) ) implies ex A, B being Subset of FMT st (A ^Foi) /\ (B ^Foi) <> (A /\ B) ^Foi ) proof given x0 being Element of FMT, V1, V2 being Subset of FMT such that A12: ( V1 in U_FMT x0 & V2 in U_FMT x0 ) and A13: for W being Subset of FMT st W in U_FMT x0 holds not W c= V1 /\ V2 ; ::_thesis: ex A, B being Subset of FMT st (A ^Foi) /\ (B ^Foi) <> (A /\ B) ^Foi take V1 ; ::_thesis: ex B being Subset of FMT st (V1 ^Foi) /\ (B ^Foi) <> (V1 /\ B) ^Foi take V2 ; ::_thesis: (V1 ^Foi) /\ (V2 ^Foi) <> (V1 /\ V2) ^Foi ( x0 in V1 ^Foi & x0 in V2 ^Foi ) by A12; then x0 in (V1 ^Foi) /\ (V2 ^Foi) by XBOOLE_0:def_4; hence (V1 ^Foi) /\ (V2 ^Foi) <> (V1 /\ V2) ^Foi by A13, Th21; ::_thesis: verum end; hence ( ( for A, B being Subset of FMT holds (A ^Foi) /\ (B ^Foi) = (A /\ B) ^Foi ) implies for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) ; ::_thesis: verum end; theorem :: FINTOPO2:32 for FMT being non empty FMT_Space_Str for A, B being Subset of FMT st ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) holds (A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) holds (A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta) let A, B be Subset of FMT; ::_thesis: ( ( for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) implies (A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta) ) assume A1: for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ; ::_thesis: (A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta) for x being Element of FMT st x in (A \/ B) ^Fodelta holds x in (A ^Fodelta) \/ (B ^Fodelta) proof let x be Element of FMT; ::_thesis: ( x in (A \/ B) ^Fodelta implies x in (A ^Fodelta) \/ (B ^Fodelta) ) assume A2: x in (A \/ B) ^Fodelta ; ::_thesis: x in (A ^Fodelta) \/ (B ^Fodelta) A3: for W1 being Subset of FMT holds ( not W1 in U_FMT x or ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) ) proof let W1 be Subset of FMT; ::_thesis: ( not W1 in U_FMT x or ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) ) assume A4: W1 in U_FMT x ; ::_thesis: ( ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) ) then W1 meets (A \/ B) ` by A2, Th19; then W1 /\ ((A \/ B) `) <> {} by XBOOLE_0:def_7; then A5: W1 /\ ((A `) /\ (B `)) <> {} by XBOOLE_1:53; then (W1 /\ (A `)) /\ (B `) <> {} by XBOOLE_1:16; then W1 /\ (A `) meets B ` by XBOOLE_0:def_7; then A6: ex z1 being set st z1 in (W1 /\ (A `)) /\ (B `) by XBOOLE_0:4; (W1 /\ (B `)) /\ (A `) <> {} by A5, XBOOLE_1:16; then W1 /\ (B `) meets A ` by XBOOLE_0:def_7; then A7: ex z2 being set st z2 in (W1 /\ (B `)) /\ (A `) by XBOOLE_0:4; W1 meets A \/ B by A2, A4, Th19; then W1 /\ (A \/ B) <> {} by XBOOLE_0:def_7; then (W1 /\ A) \/ (W1 /\ B) <> {} by XBOOLE_1:23; then ( ( W1 /\ A <> {} & W1 /\ (A `) <> {} ) or ( W1 /\ B <> {} & W1 /\ (B `) <> {} ) ) by A6, A7; hence ( ( W1 meets A & W1 meets A ` ) or ( W1 meets B & W1 meets B ` ) ) by XBOOLE_0:def_7; ::_thesis: verum end; for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x & not ( V1 meets A & V1 meets A ` ) holds ( V2 meets B & V2 meets B ` ) proof let V1, V2 be Subset of FMT; ::_thesis: ( V1 in U_FMT x & V2 in U_FMT x & not ( V1 meets A & V1 meets A ` ) implies ( V2 meets B & V2 meets B ` ) ) assume ( V1 in U_FMT x & V2 in U_FMT x ) ; ::_thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) then consider W being Subset of FMT such that A8: W in U_FMT x and A9: W c= V1 /\ V2 by A1; V1 /\ V2 c= V2 by XBOOLE_1:17; then W c= V2 by A9, XBOOLE_1:1; then A10: ( W /\ B c= V2 /\ B & W /\ (B `) c= V2 /\ (B `) ) by XBOOLE_1:26; V1 /\ V2 c= V1 by XBOOLE_1:17; then W c= V1 by A9, XBOOLE_1:1; then A11: ( W /\ A c= V1 /\ A & W /\ (A `) c= V1 /\ (A `) ) by XBOOLE_1:26; ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) proof now__::_thesis:_(_(_W_meets_A_&_W_meets_A_`_&_(_(_V1_meets_A_&_V1_meets_A_`_)_or_(_V2_meets_B_&_V2_meets_B_`_)_)_)_or_(_W_meets_B_&_W_meets_B_`_&_(_(_V1_meets_A_&_V1_meets_A_`_)_or_(_V2_meets_B_&_V2_meets_B_`_)_)_)_) percases ( ( W meets A & W meets A ` ) or ( W meets B & W meets B ` ) ) by A3, A8; case ( W meets A & W meets A ` ) ; ::_thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) then ( ex z1 being set st z1 in W /\ A & ex z2 being set st z2 in W /\ (A `) ) by XBOOLE_0:4; hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A11, XBOOLE_0:4; ::_thesis: verum end; case ( W meets B & W meets B ` ) ; ::_thesis: ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) then ( ex z3 being set st z3 in W /\ B & ex z4 being set st z4 in W /\ (B `) ) by XBOOLE_0:4; hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) by A10, XBOOLE_0:4; ::_thesis: verum end; end; end; hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) ; ::_thesis: verum end; hence ( ( V1 meets A & V1 meets A ` ) or ( V2 meets B & V2 meets B ` ) ) ; ::_thesis: verum end; then ( for V1 being Subset of FMT st V1 in U_FMT x holds ( V1 meets A & V1 meets A ` ) or for V2 being Subset of FMT st V2 in U_FMT x holds ( V2 meets B & V2 meets B ` ) ) ; then ( x in A ^Fodelta or x in B ^Fodelta ) ; hence x in (A ^Fodelta) \/ (B ^Fodelta) by XBOOLE_0:def_3; ::_thesis: verum end; hence (A \/ B) ^Fodelta c= (A ^Fodelta) \/ (B ^Fodelta) by SUBSET_1:2; ::_thesis: verum end; theorem :: FINTOPO2:33 for FMT being non empty FMT_Space_Str st FMT is Fo_filled & ( for A, B being Subset of FMT holds (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) ) holds for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: ( FMT is Fo_filled & ( for A, B being Subset of FMT holds (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) ) implies for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) assume A1: FMT is Fo_filled ; ::_thesis: ( ex A, B being Subset of FMT st not (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) or for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) ( ex x being Element of FMT ex V1, V2 being Subset of FMT st ( V1 in U_FMT x & V2 in U_FMT x & ( for W being Subset of FMT st W in U_FMT x holds not W c= V1 /\ V2 ) ) implies ex A, B being Subset of FMT st (A \/ B) ^Fodelta <> (A ^Fodelta) \/ (B ^Fodelta) ) proof given x0 being Element of FMT, V1, V2 being Subset of FMT such that A2: V1 in U_FMT x0 and A3: V2 in U_FMT x0 and A4: for W being Subset of FMT st W in U_FMT x0 holds not W c= V1 /\ V2 ; ::_thesis: ex A, B being Subset of FMT st (A \/ B) ^Fodelta <> (A ^Fodelta) \/ (B ^Fodelta) take V1 ` ; ::_thesis: ex B being Subset of FMT st ((V1 `) \/ B) ^Fodelta <> ((V1 `) ^Fodelta) \/ (B ^Fodelta) take V2 ` ; ::_thesis: ((V1 `) \/ (V2 `)) ^Fodelta <> ((V1 `) ^Fodelta) \/ ((V2 `) ^Fodelta) A5: not x0 in (V2 `) ^Fodelta proof assume x0 in (V2 `) ^Fodelta ; ::_thesis: contradiction then V2 meets V2 ` by A3, Th19; hence contradiction by XBOOLE_1:79; ::_thesis: verum end; for W being Subset of FMT st W in U_FMT x0 holds ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` ) proof let W be Subset of FMT; ::_thesis: ( W in U_FMT x0 implies ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` ) ) assume A6: W in U_FMT x0 ; ::_thesis: ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` ) then A7: not W c= V1 /\ V2 by A4; A8: W meets (V1 /\ V2) ` proof assume W /\ ((V1 /\ V2) `) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then W \ (V1 /\ V2) = {} by SUBSET_1:13; hence contradiction by A7, XBOOLE_1:37; ::_thesis: verum end; ( x0 in V1 & x0 in V2 ) by A1, A2, A3, Def8; then A9: x0 in V1 /\ V2 by XBOOLE_0:def_4; x0 in W by A1, A6, Def8; then W /\ (((V1 /\ V2) `) `) <> {} by A9, XBOOLE_0:def_4; then W meets ((V1 /\ V2) `) ` by XBOOLE_0:def_7; hence ( W meets (V1 `) \/ (V2 `) & W meets ((V1 `) \/ (V2 `)) ` ) by A8, XBOOLE_1:54; ::_thesis: verum end; then A10: x0 in ((V1 `) \/ (V2 `)) ^Fodelta ; not x0 in (V1 `) ^Fodelta proof assume x0 in (V1 `) ^Fodelta ; ::_thesis: contradiction then V1 meets V1 ` by A2, Th19; hence contradiction by XBOOLE_1:79; ::_thesis: verum end; hence ((V1 `) \/ (V2 `)) ^Fodelta <> ((V1 `) ^Fodelta) \/ ((V2 `) ^Fodelta) by A10, A5, XBOOLE_0:def_3; ::_thesis: verum end; hence ( ex A, B being Subset of FMT st not (A \/ B) ^Fodelta = (A ^Fodelta) \/ (B ^Fodelta) or for x being Element of FMT for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds ex W being Subset of FMT st ( W in U_FMT x & W c= V1 /\ V2 ) ) ; ::_thesis: verum end; theorem :: FINTOPO2:34 for FMT being non empty FMT_Space_Str for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for x being Element of FMT for A being Subset of FMT holds ( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) ) let x be Element of FMT; ::_thesis: for A being Subset of FMT holds ( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) ) let A be Subset of FMT; ::_thesis: ( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) ) A1: ( x in A & not x in (A \ {x}) ^Fob implies x in A ^Fos ) proof assume that A2: x in A and A3: not x in (A \ {x}) ^Fob ; ::_thesis: x in A ^Fos consider V9 being Subset of FMT such that A4: V9 in U_FMT x and A5: V9 misses A \ {x} by A3; V9 misses A /\ ({x} `) by A5, SUBSET_1:13; then V9 /\ (A /\ ({x} `)) = {} by XBOOLE_0:def_7; then (V9 /\ ({x} `)) /\ A = {} by XBOOLE_1:16; then (V9 \ {x}) /\ A = {} by SUBSET_1:13; then V9 \ {x} misses A by XBOOLE_0:def_7; hence x in A ^Fos by A2, A4; ::_thesis: verum end; ( x in A ^Fos implies ( x in A & not x in (A \ {x}) ^Fob ) ) proof assume A6: x in A ^Fos ; ::_thesis: ( x in A & not x in (A \ {x}) ^Fob ) then consider V9 being Subset of FMT such that A7: V9 in U_FMT x and A8: V9 \ {x} misses A by Th22; V9 /\ ({x} `) misses A by A8, SUBSET_1:13; then (V9 /\ ({x} `)) /\ A = {} by XBOOLE_0:def_7; then V9 /\ (({x} `) /\ A) = {} by XBOOLE_1:16; then V9 misses ({x} `) /\ A by XBOOLE_0:def_7; then V9 misses A \ {x} by SUBSET_1:13; hence ( x in A & not x in (A \ {x}) ^Fob ) by A6, A7, Th20, Th22; ::_thesis: verum end; hence ( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) ) by A1; ::_thesis: verum end; theorem Th35: :: FINTOPO2:35 for FMT being non empty FMT_Space_Str holds ( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: ( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob ) A1: ( ( for A being Subset of FMT holds A c= A ^Fob ) implies FMT is Fo_filled ) proof assume A2: for A being Subset of FMT holds A c= A ^Fob ; ::_thesis: FMT is Fo_filled assume not FMT is Fo_filled ; ::_thesis: contradiction then consider y being Element of FMT, V being Subset of FMT such that A3: V in U_FMT y and A4: not y in V by Def8; A5: V misses {y} proof assume V meets {y} ; ::_thesis: contradiction then ex z being set st ( z in V & z in {y} ) by XBOOLE_0:3; hence contradiction by A4, TARSKI:def_1; ::_thesis: verum end; not {y} c= {y} ^Fob proof A6: y in {y} by TARSKI:def_1; assume {y} c= {y} ^Fob ; ::_thesis: contradiction hence contradiction by A3, A5, A6, Th20; ::_thesis: verum end; hence contradiction by A2; ::_thesis: verum end; ( FMT is Fo_filled implies for A being Subset of FMT holds A c= A ^Fob ) proof assume A7: FMT is Fo_filled ; ::_thesis: for A being Subset of FMT holds A c= A ^Fob let A be Subset of FMT; ::_thesis: A c= A ^Fob let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A ^Fob ) assume A8: x in A ; ::_thesis: x in A ^Fob then reconsider y = x as Element of FMT ; for W being Subset of FMT st W in U_FMT y holds W meets A proof let W be Subset of FMT; ::_thesis: ( W in U_FMT y implies W meets A ) assume W in U_FMT y ; ::_thesis: W meets A then y in W by A7, Def8; hence W meets A by A8, XBOOLE_0:3; ::_thesis: verum end; hence x in A ^Fob ; ::_thesis: verum end; hence ( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob ) by A1; ::_thesis: verum end; theorem Th36: :: FINTOPO2:36 for FMT being non empty FMT_Space_Str holds ( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A ) proof let FMT be non empty FMT_Space_Str ; ::_thesis: ( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A ) A1: ( FMT is Fo_filled implies for A being Subset of FMT holds A ^Foi c= A ) proof assume A2: FMT is Fo_filled ; ::_thesis: for A being Subset of FMT holds A ^Foi c= A let A be Subset of FMT; ::_thesis: A ^Foi c= A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^Foi or x in A ) assume A3: x in A ^Foi ; ::_thesis: x in A then reconsider y = x as Element of FMT ; consider V being Subset of FMT such that A4: V in U_FMT y and A5: V c= A by A3, Th21; y in V by A2, A4, Def8; hence x in A by A5; ::_thesis: verum end; ( ( for A being Subset of FMT holds A ^Foi c= A ) implies FMT is Fo_filled ) proof assume A6: for A being Subset of FMT holds A ^Foi c= A ; ::_thesis: FMT is Fo_filled assume not FMT is Fo_filled ; ::_thesis: contradiction then consider y being Element of FMT, V being Subset of FMT such that A7: V in U_FMT y and A8: not y in V by Def8; y in V ^Foi by A7; then not V ^Foi c= V by A8; hence contradiction by A6; ::_thesis: verum end; hence ( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A ) by A1; ::_thesis: verum end; theorem Th37: :: FINTOPO2:37 for FMT being non empty FMT_Space_Str for A being Subset of FMT holds ((A `) ^Fob) ` = A ^Foi proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds ((A `) ^Fob) ` = A ^Foi let A be Subset of FMT; ::_thesis: ((A `) ^Fob) ` = A ^Foi for x being set holds ( x in ((A `) ^Fob) ` iff x in A ^Foi ) proof let x be set ; ::_thesis: ( x in ((A `) ^Fob) ` iff x in A ^Foi ) thus ( x in ((A `) ^Fob) ` implies x in A ^Foi ) ::_thesis: ( x in A ^Foi implies x in ((A `) ^Fob) ` ) proof assume A1: x in ((A `) ^Fob) ` ; ::_thesis: x in A ^Foi then reconsider y = x as Element of FMT ; not y in (A `) ^Fob by A1, XBOOLE_0:def_5; then consider V being Subset of FMT such that A2: V in U_FMT y and A3: V misses A ` ; V /\ (A `) = {} by A3, XBOOLE_0:def_7; then V \ A = {} by SUBSET_1:13; then V c= A by XBOOLE_1:37; hence x in A ^Foi by A2; ::_thesis: verum end; assume A4: x in A ^Foi ; ::_thesis: x in ((A `) ^Fob) ` then reconsider y = x as Element of FMT ; consider V being Subset of FMT such that A5: V in U_FMT y and A6: V c= A by A4, Th21; V \ A = {} by A6, XBOOLE_1:37; then V /\ (A `) = {} by SUBSET_1:13; then V misses A ` by XBOOLE_0:def_7; then not y in (A `) ^Fob by A5, Th20; hence x in ((A `) ^Fob) ` by XBOOLE_0:def_5; ::_thesis: verum end; hence ((A `) ^Fob) ` = A ^Foi by TARSKI:1; ::_thesis: verum end; theorem Th38: :: FINTOPO2:38 for FMT being non empty FMT_Space_Str for A being Subset of FMT holds ((A `) ^Foi) ` = A ^Fob proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds ((A `) ^Foi) ` = A ^Fob let A be Subset of FMT; ::_thesis: ((A `) ^Foi) ` = A ^Fob for x being set holds ( x in ((A `) ^Foi) ` iff x in A ^Fob ) proof let x be set ; ::_thesis: ( x in ((A `) ^Foi) ` iff x in A ^Fob ) thus ( x in ((A `) ^Foi) ` implies x in A ^Fob ) ::_thesis: ( x in A ^Fob implies x in ((A `) ^Foi) ` ) proof assume A1: x in ((A `) ^Foi) ` ; ::_thesis: x in A ^Fob then reconsider y = x as Element of FMT ; A2: not y in (A `) ^Foi by A1, XBOOLE_0:def_5; for W being Subset of FMT st W in U_FMT y holds W meets A proof let W be Subset of FMT; ::_thesis: ( W in U_FMT y implies W meets A ) assume W in U_FMT y ; ::_thesis: W meets A then not W c= A ` by A2; then consider z being set such that A3: z in W and A4: not z in A ` by TARSKI:def_3; z in A by A3, A4, XBOOLE_0:def_5; hence W meets A by A3, XBOOLE_0:3; ::_thesis: verum end; hence x in A ^Fob ; ::_thesis: verum end; assume A5: x in A ^Fob ; ::_thesis: x in ((A `) ^Foi) ` then reconsider y = x as Element of FMT ; for W being Subset of FMT st W in U_FMT y holds not W c= A ` proof let W be Subset of FMT; ::_thesis: ( W in U_FMT y implies not W c= A ` ) assume W in U_FMT y ; ::_thesis: not W c= A ` then W meets A by A5, Th20; then ex z being set st ( z in W & z in A ) by XBOOLE_0:3; hence not W c= A ` by XBOOLE_0:def_5; ::_thesis: verum end; then not y in (A `) ^Foi by Th21; hence x in ((A `) ^Foi) ` by XBOOLE_0:def_5; ::_thesis: verum end; hence ((A `) ^Foi) ` = A ^Fob by TARSKI:1; ::_thesis: verum end; theorem Th39: :: FINTOPO2:39 for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob) let A be Subset of FMT; ::_thesis: A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob) for x being Element of FMT holds ( x in A ^Fodelta iff x in (A ^Fob) /\ ((A `) ^Fob) ) proof let x be Element of FMT; ::_thesis: ( x in A ^Fodelta iff x in (A ^Fob) /\ ((A `) ^Fob) ) thus ( x in A ^Fodelta implies x in (A ^Fob) /\ ((A `) ^Fob) ) ::_thesis: ( x in (A ^Fob) /\ ((A `) ^Fob) implies x in A ^Fodelta ) proof assume A1: x in A ^Fodelta ; ::_thesis: x in (A ^Fob) /\ ((A `) ^Fob) then for W being Subset of FMT st W in U_FMT x holds W meets A ` by Th19; then A2: x in (A `) ^Fob ; for W being Subset of FMT st W in U_FMT x holds W meets A by A1, Th19; then x in A ^Fob ; hence x in (A ^Fob) /\ ((A `) ^Fob) by A2, XBOOLE_0:def_4; ::_thesis: verum end; assume x in (A ^Fob) /\ ((A `) ^Fob) ; ::_thesis: x in A ^Fodelta then ( x in A ^Fob & x in (A `) ^Fob ) by XBOOLE_0:def_4; then for W being Subset of FMT st W in U_FMT x holds ( W meets A & W meets A ` ) by Th20; hence x in A ^Fodelta ; ::_thesis: verum end; hence A ^Fodelta = (A ^Fob) /\ ((A `) ^Fob) by SUBSET_1:3; ::_thesis: verum end; theorem :: FINTOPO2:40 for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `) let A be Subset of FMT; ::_thesis: A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `) ((A `) ^Fob) ` = A ^Foi by Th37; hence A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `) by Th39; ::_thesis: verum end; theorem :: FINTOPO2:41 for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fodelta = (A `) ^Fodelta proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A `) ^Fodelta let A be Subset of FMT; ::_thesis: A ^Fodelta = (A `) ^Fodelta A ^Fodelta = (((A `) `) ^Fob) /\ ((A `) ^Fob) by Th39; hence A ^Fodelta = (A `) ^Fodelta by Th39; ::_thesis: verum end; theorem :: FINTOPO2:42 for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fodelta = (A ^Fob) \ (A ^Foi) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob) \ (A ^Foi) let A be Subset of FMT; ::_thesis: A ^Fodelta = (A ^Fob) \ (A ^Foi) for x being set holds ( x in A ^Fodelta iff x in (A ^Fob) \ (A ^Foi) ) proof let x be set ; ::_thesis: ( x in A ^Fodelta iff x in (A ^Fob) \ (A ^Foi) ) thus ( x in A ^Fodelta implies x in (A ^Fob) \ (A ^Foi) ) ::_thesis: ( x in (A ^Fob) \ (A ^Foi) implies x in A ^Fodelta ) proof assume x in A ^Fodelta ; ::_thesis: x in (A ^Fob) \ (A ^Foi) then x in (A ^Fob) /\ ((((A `) ^Fob) `) `) by Th39; then x in (A ^Fob) /\ ((A ^Foi) `) by Th37; hence x in (A ^Fob) \ (A ^Foi) by SUBSET_1:13; ::_thesis: verum end; assume x in (A ^Fob) \ (A ^Foi) ; ::_thesis: x in A ^Fodelta then x in (A ^Fob) /\ ((A ^Foi) `) by SUBSET_1:13; then x in (A ^Fob) /\ ((((A `) ^Fob) `) `) by Th37; hence x in A ^Fodelta by Th39; ::_thesis: verum end; hence A ^Fodelta = (A ^Fob) \ (A ^Foi) by TARSKI:1; ::_thesis: verum end; definition let FMT be non empty FMT_Space_Str ; let A be Subset of FMT; funcA ^Fodel_i -> Subset of FMT equals :: FINTOPO2:def 14 A /\ (A ^Fodelta); coherence A /\ (A ^Fodelta) is Subset of FMT ; funcA ^Fodel_o -> Subset of FMT equals :: FINTOPO2:def 15 (A `) /\ (A ^Fodelta); coherence (A `) /\ (A ^Fodelta) is Subset of FMT ; end; :: deftheorem defines ^Fodel_i FINTOPO2:def_14_:_ for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fodel_i = A /\ (A ^Fodelta); :: deftheorem defines ^Fodel_o FINTOPO2:def_15_:_ for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fodel_o = (A `) /\ (A ^Fodelta); theorem :: FINTOPO2:43 for FMT being non empty FMT_Space_Str for A being Subset of FMT holds A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o) let A be Subset of FMT; ::_thesis: A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o) for x being set holds ( x in A ^Fodelta iff x in (A ^Fodel_i) \/ (A ^Fodel_o) ) proof let x be set ; ::_thesis: ( x in A ^Fodelta iff x in (A ^Fodel_i) \/ (A ^Fodel_o) ) thus ( x in A ^Fodelta implies x in (A ^Fodel_i) \/ (A ^Fodel_o) ) ::_thesis: ( x in (A ^Fodel_i) \/ (A ^Fodel_o) implies x in A ^Fodelta ) proof assume x in A ^Fodelta ; ::_thesis: x in (A ^Fodel_i) \/ (A ^Fodel_o) then x in ([#] the carrier of FMT) /\ (A ^Fodelta) by XBOOLE_1:28; then x in (A \/ (A `)) /\ (A ^Fodelta) by SUBSET_1:10; hence x in (A ^Fodel_i) \/ (A ^Fodel_o) by XBOOLE_1:23; ::_thesis: verum end; assume x in (A ^Fodel_i) \/ (A ^Fodel_o) ; ::_thesis: x in A ^Fodelta then x in (A \/ (A `)) /\ (A ^Fodelta) by XBOOLE_1:23; then x in ([#] the carrier of FMT) /\ (A ^Fodelta) by SUBSET_1:10; hence x in A ^Fodelta by XBOOLE_1:28; ::_thesis: verum end; hence A ^Fodelta = (A ^Fodel_i) \/ (A ^Fodel_o) by TARSKI:1; ::_thesis: verum end; definition let FMT be non empty FMT_Space_Str ; let G be Subset of FMT; attrG is Fo_open means :Def16: :: FINTOPO2:def 16 G = G ^Foi ; attrG is Fo_closed means :Def17: :: FINTOPO2:def 17 G = G ^Fob ; end; :: deftheorem Def16 defines Fo_open FINTOPO2:def_16_:_ for FMT being non empty FMT_Space_Str for G being Subset of FMT holds ( G is Fo_open iff G = G ^Foi ); :: deftheorem Def17 defines Fo_closed FINTOPO2:def_17_:_ for FMT being non empty FMT_Space_Str for G being Subset of FMT holds ( G is Fo_closed iff G = G ^Fob ); theorem :: FINTOPO2:44 for FMT being non empty FMT_Space_Str for A being Subset of FMT st A ` is Fo_open holds A is Fo_closed proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT st A ` is Fo_open holds A is Fo_closed let A be Subset of FMT; ::_thesis: ( A ` is Fo_open implies A is Fo_closed ) assume A ` is Fo_open ; ::_thesis: A is Fo_closed then A1: A ` = (A `) ^Foi by Def16; (((A `) ^Foi) `) ` = (A ^Fob) ` by Th38; hence A is Fo_closed by A1, Def17; ::_thesis: verum end; theorem :: FINTOPO2:45 for FMT being non empty FMT_Space_Str for A being Subset of FMT st A ` is Fo_closed holds A is Fo_open proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A being Subset of FMT st A ` is Fo_closed holds A is Fo_open let A be Subset of FMT; ::_thesis: ( A ` is Fo_closed implies A is Fo_open ) assume A ` is Fo_closed ; ::_thesis: A is Fo_open then A1: A ` = (A `) ^Fob by Def17; (A `) ^Fob = (((A `) `) ^Foi) ` by Th38 .= (A ^Foi) ` ; then A = ((A ^Foi) `) ` by A1 .= A ^Foi ; hence A is Fo_open by Def16; ::_thesis: verum end; theorem :: FINTOPO2:46 for FMT being non empty FMT_Space_Str for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) let A, B be Subset of FMT; ::_thesis: ( FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) implies (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) ) assume A1: FMT is Fo_filled ; ::_thesis: ( ex x being Element of FMT st not {x} in U_FMT x or (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) ) assume A2: for x being Element of FMT holds {x} in U_FMT x ; ::_thesis: (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) A3: for C being Subset of FMT holds C ^Fob c= C proof let C be Subset of FMT; ::_thesis: C ^Fob c= C for y being Element of FMT st y in C ^Fob holds y in C proof let y be Element of FMT; ::_thesis: ( y in C ^Fob implies y in C ) assume A4: y in C ^Fob ; ::_thesis: y in C {y} in U_FMT y by A2; then {y} meets C by A4, Th20; then ex z being set st ( z in {y} & z in C ) by XBOOLE_0:3; hence y in C by TARSKI:def_1; ::_thesis: verum end; hence C ^Fob c= C by SUBSET_1:2; ::_thesis: verum end; A5: for C being Subset of FMT holds C ^Fob = C proof let C be Subset of FMT; ::_thesis: C ^Fob = C ( C c= C ^Fob & C ^Fob c= C ) by A1, A3, Th35; hence C ^Fob = C by XBOOLE_0:def_10; ::_thesis: verum end; then ( (A /\ B) ^Fob = A /\ B & A ^Fob = A ) ; hence (A /\ B) ^Fob = (A ^Fob) /\ (B ^Fob) by A5; ::_thesis: verum end; theorem :: FINTOPO2:47 for FMT being non empty FMT_Space_Str for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi proof let FMT be non empty FMT_Space_Str ; ::_thesis: for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi let A, B be Subset of FMT; ::_thesis: ( FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) implies (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi ) assume A1: FMT is Fo_filled ; ::_thesis: ( ex x being Element of FMT st not {x} in U_FMT x or (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi ) assume A2: for x being Element of FMT holds {x} in U_FMT x ; ::_thesis: (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi A3: for C being Subset of FMT holds C c= C ^Foi proof let C be Subset of FMT; ::_thesis: C c= C ^Foi for y being Element of FMT st y in C holds y in C ^Foi proof let y be Element of FMT; ::_thesis: ( y in C implies y in C ^Foi ) assume y in C ; ::_thesis: y in C ^Foi then A4: {y} is Subset of C by SUBSET_1:41; {y} in U_FMT y by A2; hence y in C ^Foi by A4; ::_thesis: verum end; hence C c= C ^Foi by SUBSET_1:2; ::_thesis: verum end; A5: for C being Subset of FMT holds C = C ^Foi proof let C be Subset of FMT; ::_thesis: C = C ^Foi ( C c= C ^Foi & C ^Foi c= C ) by A1, A3, Th36; hence C = C ^Foi by XBOOLE_0:def_10; ::_thesis: verum end; then ( (A \/ B) ^Foi = A \/ B & A ^Foi = A ) ; hence (A ^Foi) \/ (B ^Foi) = (A \/ B) ^Foi by A5; ::_thesis: verum end;