let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds union (Cl (Int F)) c= Cl (Int (union F))
let F be Subset-Family of T; :: thesis: union (Cl (Int F)) c= Cl (Int (union F))
union (Int F) c= Int (union F) by Th28;
then ( union (Cl (Int F)) c= Cl (union (Int F)) & Cl (union (Int F)) c= Cl (Int (union F)) ) by Th15, PRE_TOPC:49;
hence union (Cl (Int F)) c= Cl (Int (union F)) by XBOOLE_1:1; :: thesis: verum