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))
A1: Cl (union (Int F)) c= Cl (Int (union F)) by Th27, PRE_TOPC:19;
union (Cl (Int F)) c= Cl (union (Int F)) by Th15;
hence union (Cl (Int F)) c= Cl (Int (union F)) by A1; :: thesis: verum