let T be non empty TopSpace; :: thesis: for F being Subset-Family of T st ( for A being Subset of T st A in F holds
A c= Cl (Int A) ) holds
( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )
let F be Subset-Family of T; :: thesis: ( ( for A being Subset of T st A in F holds
A c= Cl (Int A) ) implies ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) ) )
A1: Cl (Int (Cl (union F))) c= Cl (Cl (union F)) by PRE_TOPC:49, TOPS_1:44;
assume A2: for A being Subset of T st A in F holds
A c= Cl (Int A) ; :: thesis: ( union F c= Cl (Int (union F)) & Cl (union F) = Cl (Int (Cl (union F))) )

A3: now

let A0 be set ; :: thesis: ( A0 in F implies A0 c= Cl (Int (union F)) )
assume A4: A0 in F ; :: thesis: A0 c= Cl (Int (union F))
then reconsider A = A0 as Subset of T ;
Int A c= Int (union F) by A4, TOPS_1:48, ZFMISC_1:92;
then A5: Cl (Int A) c= Cl (Int (union F)) by PRE_TOPC:49;
A c= Cl (Int A) by A2, A4;
hence A0 c= Cl (Int (union F)) by A5, XBOOLE_1:1; :: thesis: verum

end;

hence union F c= Cl (Int (union F)) by ZFMISC_1:94; :: thesis: Cl (union F) = Cl (Int (Cl (union F)))
Int (union F) c= Int (Cl (union F)) by PRE_TOPC:48, TOPS_1:48;
then A6: Cl (Int (union F)) c= Cl (Int (Cl (union F))) by PRE_TOPC:49;
union F c= Cl (Int (union F)) by A3, ZFMISC_1:94;
then Cl (union F) c= Cl (Cl (Int (union F))) by PRE_TOPC:49;
then Cl (union F) c= Cl (Int (Cl (union F))) by A6, XBOOLE_1:1;
hence Cl (union F) = Cl (Int (Cl (union F))) by A1, XBOOLE_0:def 10; :: thesis: verum