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:19, TOPS_1:16;
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 :: thesis: for A0 being set st A0 in F holds
A0 c= Cl (Int (union F))
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:19, ZFMISC_1:74;
then A5: Cl (Int A) c= Cl (Int (union F)) by PRE_TOPC:19;
A c= Cl (Int A) by A2, A4;
hence A0 c= Cl (Int (union F)) by A5; :: thesis: verum
end;
hence union F c= Cl (Int (union F)) by ZFMISC_1:76; :: thesis: Cl (union F) = Cl (Int (Cl (union F)))
Int (union F) c= Int (Cl (union F)) by PRE_TOPC:18, TOPS_1:19;
then A6: Cl (Int (union F)) c= Cl (Int (Cl (union F))) by PRE_TOPC:19;
union F c= Cl (Int (union F)) by A3, ZFMISC_1:76;
then Cl (union F) c= Cl (Cl (Int (union F))) by PRE_TOPC:19;
then Cl (union F) c= Cl (Int (Cl (union F))) by A6;
hence Cl (union F) = Cl (Int (Cl (union F))) by A1, XBOOLE_0:def 10; :: thesis: verum