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

proof

let B be Subset of T; :: thesis: ( B in F implies B c= (union F) \/ (Int (Cl (union F))) )
assume B in F ; :: thesis: B c= (union F) \/ (Int (Cl (union F)))
then A1: B c= union F by ZFMISC_1:74;
union F c= (union F) \/ (Int (Cl (union F))) by XBOOLE_1:7;
hence B c= (union F) \/ (Int (Cl (union F))) by A1; :: thesis: verum

end;

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

proof

let A be Subset of T; :: thesis: ( A is condensed & ( for B being Subset of T st B in F holds
B c= A ) implies (union F) \/ (Int (Cl (union F))) c= A )
assume A is condensed ; :: thesis: ( ex B being Subset of T st
( B in F & not B c= A ) or (union F) \/ (Int (Cl (union F))) c= A )
then A2: Int (Cl A) c= A by TOPS_1:def 6;
assume for B being Subset of T st B in F holds
B c= A ; :: thesis: (union F) \/ (Int (Cl (union F))) c= A
then for P being set st P in F holds
P c= A ;
then A3: union F c= A by ZFMISC_1:76;
then Cl (union F) c= Cl A by PRE_TOPC:19;
then Int (Cl (union F)) c= Int (Cl A) by TOPS_1:19;
then Int (Cl (union F)) c= A by A2;
hence (union F) \/ (Int (Cl (union F))) c= A by A3, XBOOLE_1:8; :: thesis: verum

end;