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

now :: thesis: for y being set holds
( ( y in A implies ex Y1 being Subset of Y st
( Y1 is open & Y1 c= A & y in Y1 ) ) & ( ex Q being Subset of Y st
( Q is open & Q c= A & y in Q ) implies y in A ) )

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

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

assume y in A ; :: thesis: ex Y1 being Subset of Y st
( Y1 is open & Y1 c= A & y in Y1 )
then consider z being object such that
A1: [z,y] in W and
A2: z in {x} by RELAT_1:def 13;
consider AA being Subset-Family of [:X,Y:] such that
A3: W = union AA and
A4: for e being set st e in AA holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
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 X, Y1 being Subset of Y 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:87;
thus Y1 c= A :: thesis: y in Y1

proof

let z be object ; :: 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:87;
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:87; :: thesis: verum

end;

thus ( ex Q being Subset of Y 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 Y by TOPS_1:25; :: thesis: verum