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

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