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)
A1: Int (union (Int F)) c= Int (union F) by Th26, TOPS_1:48;
union (Int F) is open by Th18, TOPS_2:26;
hence union (Int F) c= Int (union F) by A1, TOPS_1:55; :: thesis: verum