let X be non empty TopSpace; :: thesis: for x being Point of X
for A, B being Subset of X holds
( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff A /\ B is a_neighborhood of x )
let x be Point of X; :: thesis: for A, B being Subset of X holds
( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff A /\ B is a_neighborhood of x )
let A, B be Subset of X; :: thesis: ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff A /\ B is a_neighborhood of x )
( A is a_neighborhood of x & B is a_neighborhood of x iff ( x in Int A & x in Int B ) ) by Def1;
then ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff x in (Int A) /\ (Int B) ) by XBOOLE_0:def 4;
then ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff x in Int (A /\ B) ) by TOPS_1:17;
hence ( ( A is a_neighborhood of x & B is a_neighborhood of x ) iff A /\ B is a_neighborhood of x ) by Def1; :: thesis: verum