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 } ) )
consider G0 being Element of I;
reconsider G0 = G0 as Subset-Family of T by XBOOLE_1:1;
assume A1: 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 } )
set Z = { (Cl (union G)) where G is Subset-Family of T : G in I } ;
A2: Cl (union G0) in { (Cl (union G)) where G is Subset-Family of T : G in I } ;
then reconsider Z' = { (Cl (union G)) where G is Subset-Family of T : G in I } as non empty set ;
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 set ; :: 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 A3: ( a in Cl (union F) & not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : G in I } ) ) ; :: thesis: contradiction
then reconsider a = a as Point of T ;
( not a in meet Z' & not a in union (clf F) ) by A3, XBOOLE_0:def 3;
then consider b being set such that
A4: ( b in { (Cl (union G)) where G is Subset-Family of T : G in I } & not a in b ) by SETFAM_1:def 1;
consider G being Subset-Family of T such that
A5: ( b = Cl (union G) & G in I ) by A4;
A6: not T is empty by A3;
F = G \/ (F \ G) by A5, XBOOLE_1:45;
then union F = (union G) \/ (union (F \ G)) by ZFMISC_1:96;
then ( Cl (union F) = (Cl (union G)) \/ (Cl (union (F \ G))) & F \ G c= F ) by PRE_TOPC:50, XBOOLE_1:36;
then ( a in Cl (union (F \ G)) & clf (F \ G) c= clf F & G c= F & F \ G is finite ) by A1, A3, A4, A5, A6, PCOMPS_1:17, XBOOLE_0:def 3;
then ( a in union (clf (F \ G)) & union (clf (F \ G)) c= union (clf F) ) by A6, PCOMPS_1:19, ZFMISC_1:95;
hence contradiction by A3, XBOOLE_0:def 3; :: thesis: verum

end;

let a be set ; :: 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 A7: 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 Z' ) by A7, XBOOLE_0:def 3;

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

then consider b being set such that
A8: ( a in b & b in clf F ) by TARSKI:def 4;
consider W being Subset of T such that
A9: ( b = Cl W & W in F ) by A8, PCOMPS_1:def 3;
b c= Cl (union F) by A9, PRE_TOPC:49, ZFMISC_1:92;
hence a in Cl (union F) by A8; :: thesis: verum

end;

suppose A10: a in meet Z' ; :: thesis: a in Cl (union F)

union G0 c= union F by ZFMISC_1:95;
then ( a in Cl (union G0) & Cl (union G0) c= Cl (union F) ) by A2, A10, PRE_TOPC:49, SETFAM_1:def 1;
hence a in Cl (union F) ; :: thesis: verum

end;

end;