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 \ 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 Z9 = { (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 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 c= F & F \ G is finite ) } ) )
assume that
A2: a in Cl (union F) and
A3: 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
reconsider a = a as Point of T by A2;
not a in meet Z9 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 c= F & F \ G is finite ) } and
A5: not a in b by SETFAM_1:def 1;
consider G being Subset-Family of T such that
A6: b = Cl (union G) and
A7: G c= F and
A8: F \ G is finite by A4;
A9: not T is empty by A2;
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 A7, 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 A2, A5, A6, XBOOLE_0:def 3;
then a in union (clf (F \ G)) by A8, A9, PCOMPS_1:16;
hence contradiction by A3, 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 c= F & F \ G is finite ) } ) 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 c= F & F \ G is finite ) } ) ; :: 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 a in meet Z9 ; :: thesis: a in Cl (union F)
hence a in Cl (union F) by A1, SETFAM_1:def 1; :: thesis: verum
end;
end;