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 Th25, TOPS_1:19;
union (Int F) is open by Th17, TOPS_2:19;
hence union (Int F) c= Int (union F) by A1, TOPS_1:23; :: thesis: verum