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 )

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

hence
( A is a_neighborhood of x & B is a_neighborhood of x implies A \/ B is a_neighborhood of x )
; :: thesis: verum
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;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