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