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 F is open ; :: thesis: for B being Subset of T st B in F holds
B c= Int (Cl (union F))
then union F is open by TOPS_2:19;
then A1: Int (union F) = union F by TOPS_1:23;
let B be Subset of T; :: thesis: ( B in F implies B c= Int (Cl (union F)) )
A2: Int (union F) c= Int (Cl (union F)) by PRE_TOPC:18, TOPS_1:19;
assume B in F ; :: thesis: B c= Int (Cl (union F))
then B c= union F by ZFMISC_1:74;
hence B c= Int (Cl (union F)) by A2, A1; :: 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 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 )
then A3: A = Int (Cl A) by TOPS_1:def 8;
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:76;
then Cl (union F) c= Cl A by PRE_TOPC:19;
hence Int (Cl (union F)) c= A by A3, TOPS_1:19; :: thesis: verum

end;