let X be non empty TopSpace; :: thesis: for x being Point of X
for A, B being Subset of X st A is a_neighborhood of x & B is a_neighborhood of x holds
A \/ B is a_neighborhood of x

let x be Point of X; :: thesis: for A, B being Subset of X st A is a_neighborhood of x & B is a_neighborhood of x holds
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 implies A \/ B is a_neighborhood of x )
reconsider A1 = A, B1 = B as Subset of X ;
( A1 is a_neighborhood of x & B1 is a_neighborhood of x implies A1 \/ B1 is a_neighborhood of x )
proof
assume that
A1: x in Int A1 and
x in Int B1 ; :: according to CONNSP_2:def 1 :: thesis: A1 \/ B1 is a_neighborhood of x
A2: (Int A1) \/ (Int B1) c= Int (A1 \/ B1) by TOPS_1:20;
x in (Int A1) \/ (Int B1) by ;
hence A1 \/ B1 is a_neighborhood of x by ; :: thesis: verum
end;
hence ( A is a_neighborhood of x & B is a_neighborhood of x implies A \/ B is a_neighborhood of x ) ; :: thesis: verum