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