let T be non empty TopSpace; :: thesis: for F, G being Subset-Family of T st F is open & G is open holds
INTERSECTION F,G is open
let F, G be Subset-Family of T; :: thesis: ( F is open & G is open implies INTERSECTION F,G is open )
assume that
A1: F is open and
A2: G is open ; :: thesis: INTERSECTION F,G is open
for A being Subset of T st A in INTERSECTION F,G holds
A is open

proof

let A be Subset of T; :: thesis: ( A in INTERSECTION F,G implies A is open )
assume A in INTERSECTION F,G ; :: thesis: A is open
then consider X, Y being set such that
A3: ( X in F & Y in G & A = X /\ Y ) by SETFAM_1:def 5;
reconsider X = X, Y = Y as Subset of T by A3;
( X is open & Y is open ) by A1, A2, A3, TOPS_2:def 1;
hence A is open by A3, TOPS_1:38; :: thesis: verum

end;

hence INTERSECTION F,G is open by TOPS_2:def 1; :: thesis: verum