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