let T be TopSpace; :: thesis: for F being Subset-Family of T holds Int F is open
let F be Subset-Family of T; :: thesis: Int F is open
now :: thesis: for A being Subset of T st A in Int F holds
A is open
let A be Subset of T; :: thesis: ( A in Int F implies A is open )
assume A in Int F ; :: thesis: A is open
then ex B being Subset of T st
( A = Int B & B in F ) by Def1;
hence A is open ; :: thesis: verum
end;
hence Int F is open by TOPS_2:def 1; :: thesis: verum