let X, Y be non empty TopSpace; :: thesis: for W being open Subset of
for x being Point of holds Im W,x is open Subset of
let W be open Subset of ; :: thesis: for x being Point of holds Im W,x is open Subset of
let x be Point of ; :: thesis: Im W,x is open Subset of
reconsider W = W as Relation of , by BORSUK_1:def 5;
reconsider A = W .: {x} as Subset of ;

now

let y be set ; :: thesis: ( ( y in A implies ex Y1 being Subset of st
( Y1 is open & Y1 c= A & y in Y1 ) ) & ( ex Q being Subset of st
( Q is open & Q c= A & y in Q ) implies y in A ) )

hereby :: thesis: ( ex Q being Subset of st
( Q is open & Q c= A & y in Q ) implies y in A )

assume y in A ; :: thesis: ex Y1 being Subset of st
( Y1 is open & Y1 c= A & y in Y1 )
then consider z being set such that
A1: [z,y] in W and
A2: z in {x} by RELAT_1:def 13;
consider AA being Subset-Family of such that
A3: W = union AA and
A4: for e being set st e in AA holds
ex X1 being Subset of ex Y1 being Subset of st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:45;
z = x by A2, TARSKI:def 1;
then consider e being set such that
A5: [x,y] in e and
A6: e in AA by A1, A3, TARSKI:def 4;
consider X1 being Subset of , Y1 being Subset of such that
A7: e = [:X1,Y1:] and
X1 is open and
A8: Y1 is open by A4, A6;
take Y1 = Y1; :: thesis: ( Y1 is open & Y1 c= A & y in Y1 )
thus Y1 is open by A8; :: thesis: ( Y1 c= A & y in Y1 )
A9: x in X1 by A5, A7, ZFMISC_1:106;
thus Y1 c= A :: thesis: y in Y1

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in Y1 or z in A )
assume z in Y1 ; :: thesis: z in A
then [x,z] in e by A7, A9, ZFMISC_1:106;
then A10: [x,z] in W by A3, A6, TARSKI:def 4;
x in {x} by TARSKI:def 1;
hence z in A by A10, RELAT_1:def 13; :: thesis: verum

end;

thus y in Y1 by A5, A7, ZFMISC_1:106; :: thesis: verum

end;

thus ( ex Q being Subset of st
( Q is open & Q c= A & y in Q ) implies y in A ) ; :: thesis: verum

end;

hence Im W,x is open Subset of by TOPS_1:57; :: thesis: verum