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))) ) )
assume A1: 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))) )
thus A2: union F c= Cl (Int (union F)) :: thesis: Cl (union F) = Cl (Int (Cl (union F)))

proof

now

let A0 be set ; :: thesis: ( A0 in F implies A0 c= Cl (Int (union F)) )
assume A3: 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 A3, TOPS_1:48, ZFMISC_1:92;
then ( Cl (Int A) c= Cl (Int (union F)) & A c= Cl (Int A) ) by A1, A3, PRE_TOPC:49;
hence A0 c= Cl (Int (union F)) by XBOOLE_1:1; :: thesis: verum

end;

hence union F c= Cl (Int (union F)) by ZFMISC_1:94; :: thesis: verum

end;

thus Cl (union F) = Cl (Int (Cl (union F))) :: thesis: verum

proof

( union F c= Cl (Int (union F)) & union F c= Cl (union F) ) by A2, PRE_TOPC:48;
then ( Cl (union F) c= Cl (Cl (Int (union F))) & Int (union F) c= Int (Cl (union F)) ) by PRE_TOPC:49, TOPS_1:48;
then ( Cl (union F) c= Cl (Int (union F)) & Cl (Int (union F)) c= Cl (Int (Cl (union F))) ) by PRE_TOPC:49;
then A4: Cl (union F) c= Cl (Int (Cl (union F))) by XBOOLE_1:1;
Cl (Int (Cl (union F))) c= Cl (Cl (union F)) by PRE_TOPC:49, TOPS_1:44;
hence Cl (union F) = Cl (Int (Cl (union F))) by A4, XBOOLE_0:def 10; :: thesis: verum

end;