let T be TopSpace; :: thesis: for F being Subset-Family of T
for I being non empty Subset-Family of F st ( for G being set st G in I holds
F \ G is finite ) holds
Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )
let F be Subset-Family of T; :: thesis: for I being non empty Subset-Family of F st ( for G being set st G in I holds
F \ G is finite ) holds
Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )
let I be non empty Subset-Family of F; :: thesis: ( ( for G being set st G in I holds
F \ G is finite ) implies Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) )
set G0 = the Element of I;
reconsider G0 = the Element of I as Subset-Family of T by XBOOLE_1:1;
set Z = { (Cl (union G)) where G is Subset-Family of T : G in I } ;
A1: Cl (union G0) in { (Cl (union G)) where G is Subset-Family of T : G in I } ;
then reconsider Z9 = { (Cl (union G)) where G is Subset-Family of T : G in I } as non empty set ;
assume A2: for G being set st G in I holds
F \ G is finite ; :: thesis: Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } )
thus Cl (union F) c= (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) :: according to XBOOLE_0:def 10 :: thesis: (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) c= Cl (union F)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Cl (union F) or a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) )
assume that
A3: a in Cl (union F) and
A4: not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) ; :: thesis: contradiction
reconsider a = a as Point of T by A3;
not a in meet Z9 by A4, XBOOLE_0:def 3;
then consider b being set such that
A5: b in { (Cl (union G)) where G is Subset-Family of T : G in I } and
A6: not a in b by SETFAM_1:def 1;
consider G being Subset-Family of T such that
A7: b = Cl (union G) and
A8: G in I by A5;
A9: not T is empty by A3;
then clf (F \ G) c= clf F by PCOMPS_1:14, XBOOLE_1:36;
then A10: union (clf (F \ G)) c= union (clf F) by ZFMISC_1:77;
F = G \/ (F \ G) by A8, XBOOLE_1:45;
then union F = (union G) \/ (union (F \ G)) by ZFMISC_1:78;
then Cl (union F) = (Cl (union G)) \/ (Cl (union (F \ G))) by PRE_TOPC:20;
then a in Cl (union (F \ G)) by A3, A6, A7, XBOOLE_0:def 3;
then a in union (clf (F \ G)) by A2, A8, A9, PCOMPS_1:16;
hence contradiction by A4, A10, XBOOLE_0:def 3; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) or a in Cl (union F) )
assume A11: a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) ; :: thesis: a in Cl (union F)

per cases ( a in union (clf F) or a in meet Z9 ) by A11, XBOOLE_0:def 3;

suppose a in union (clf F) ; :: thesis: a in Cl (union F)

then consider b being set such that
A12: a in b and
A13: b in clf F by TARSKI:def 4;
ex W being Subset of T st
( b = Cl W & W in F ) by A13, PCOMPS_1:def 2;
then b c= Cl (union F) by PRE_TOPC:19, ZFMISC_1:74;
hence a in Cl (union F) by A12; :: thesis: verum

end;

suppose A14: a in meet Z9 ; :: thesis: a in Cl (union F)

union G0 c= union F by ZFMISC_1:77;
then A15: Cl (union G0) c= Cl (union F) by PRE_TOPC:19;
a in Cl (union G0) by A1, A14, SETFAM_1:def 1;
hence a in Cl (union F) by A15; :: thesis: verum

end;

end;