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 A1, XBOOLE_0:def 3;
hence A1 \/ B1 is a_neighborhood of x by A2, Def1; :: 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