let T be TopSpace; :: thesis: for F being Subset-Family of T holds union (Int F) c= Int (union F)
let F be Subset-Family of T; :: thesis: union (Int F) c= Int (union F)
Int F is open by Th18;
then ( union (Int F) is open & union (Int F) c= union F ) by Th26, TOPS_2:26;
then ( Int (union (Int F)) = union (Int F) & Int (union (Int F)) c= Int (union F) ) by TOPS_1:48, TOPS_1:55;
hence union (Int F) c= Int (union F) ; :: thesis: verum