let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds
( ( F is open implies for B being Subset of T st B in F holds
B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A ) )
let F be Subset-Family of T; :: thesis: ( ( F is open implies for B being Subset of T st B in F holds
B c= Int (Cl (union F)) ) & ( for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A ) )
thus ( F is open implies for B being Subset of T st B in F holds
B c= Int (Cl (union F)) ) :: thesis: for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A

proof

assume A1: F is open ; :: thesis: for B being Subset of T st B in F holds
B c= Int (Cl (union F))
let B be Subset of T; :: thesis: ( B in F implies B c= Int (Cl (union F)) )
assume B in F ; :: thesis: B c= Int (Cl (union F))
then A2: B c= union F by ZFMISC_1:92;
( union F c= Cl (union F) & union F is open ) by A1, PRE_TOPC:48, TOPS_2:26;
then ( Int (union F) c= Int (Cl (union F)) & Int (union F) = union F ) by TOPS_1:48, TOPS_1:55;
hence B c= Int (Cl (union F)) by A2, XBOOLE_1:1; :: thesis: verum

end;

thus for A being Subset of T st A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) holds
Int (Cl (union F)) c= A :: thesis: verum

proof

let A be Subset of T; :: thesis: ( A is open_condensed & ( for B being Subset of T st B in F holds
B c= A ) implies Int (Cl (union F)) c= A )
assume A3: A is open_condensed ; :: thesis: ( ex B being Subset of T st
( B in F & not B c= A ) or Int (Cl (union F)) c= A )
assume for B being Subset of T st B in F holds
B c= A ; :: thesis: Int (Cl (union F)) c= A
then for P being set st P in F holds
P c= A ;
then union F c= A by ZFMISC_1:94;
then Cl (union F) c= Cl A by PRE_TOPC:49;
then ( A = Int (Cl A) & Int (Cl (union F)) c= Int (Cl A) ) by A3, TOPS_1:48, TOPS_1:def 8;
hence Int (Cl (union F)) c= A ; :: thesis: verum

end;