let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X
for x being Point of
for x1 being Point of
for x2 being Point of st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2
let X1, X2 be non empty SubSpace of X; :: thesis: for x being Point of
for x1 being Point of
for x2 being Point of st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2
let x be Point of ; :: thesis: for x1 being Point of
for x2 being Point of st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2
let x1 be Point of ; :: thesis: for x2 being Point of st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2
let x2 be Point of ; :: thesis: ( x1 = x & x2 = x implies for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2 )
assume A1: ( x1 = x & x2 = x ) ; :: thesis: for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2
let A1 be a_neighborhood of x1; :: thesis: for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2
let A2 be a_neighborhood of x2; :: thesis: ex A being a_neighborhood of x st A c= A1 \/ A2
consider V being Subset of such that
A2: ( V is open & x in V ) and
A3: V c= A1 \/ A2 by A1, Th20;
reconsider W = V as a_neighborhood of x by A2, CONNSP_2:5;
take W ; :: thesis: W c= A1 \/ A2
thus W c= A1 \/ A2 by A3; :: thesis: verum