let T be TopSpace; :: thesis: for F being Subset-Family of T holds Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } )
let F be Subset-Family of T; :: thesis: Cl (union F) = (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } )
set Z = { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ;
( F c= F & F \ F = {} ) by XBOOLE_1:37;
then A1: Cl (union F) in { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ;
then reconsider Z' = { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } as non empty set ;
thus Cl (union F) c= (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) :: according to XBOOLE_0:def 10 :: thesis: (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) 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 c= F & F \ G is finite ) } ) )
assume A2: ( a in Cl (union F) & not a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) ) ; :: thesis: contradiction
then reconsider a = a as Point of T ;
( not a in meet Z' & not a in union (clf F) ) by A2, XBOOLE_0:def 3;
then consider b being set such that
A3: ( b in { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } & not a in b ) by SETFAM_1:def 1;
consider G being Subset-Family of T such that
A4: ( b = Cl (union G) & G c= F & F \ G is finite ) by A3;
A5: not T is empty by A2;
F = G \/ (F \ G) by A4, 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 ) by A2, A3, A4, A5, PCOMPS_1:17, XBOOLE_0:def 3;
then ( a in union (clf (F \ G)) & union (clf (F \ G)) c= union (clf F) ) by A4, A5, PCOMPS_1:19, ZFMISC_1:95;
hence contradiction by A2, 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 c= F & F \ G is finite ) } ) or a in Cl (union F) )
assume A6: a in (union (clf F)) \/ (meet { (Cl (union G)) where G is Subset-Family of T : ( G c= F & F \ G is finite ) } ) ; :: thesis: a in Cl (union F)

per cases ( a in union (clf F) or a in meet Z' ) by A6, XBOOLE_0:def 3;

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

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

end;

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

hence a in Cl (union F) by A1, SETFAM_1:def 1; :: thesis: verum

end;

end;