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
the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:] by BORSUK_1:def 5;
then reconsider W = W as Relation of the carrier of X,the carrier of Y ;
reconsider A = W .: {x} as Subset of Y ;

now

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 set such that
A1: ( [z,y] in W & z in {x} ) by RELAT_1:def 13;
consider AA being Subset-Family of [:X,Y:] such that
A2: W = union AA and
A3: 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:45;
z = x by A1, TARSKI:def 1;
then consider e being set such that
A4: ( [x,y] in e & e in AA ) by A1, A2, TARSKI:def 4;
consider X1 being Subset of X, Y1 being Subset of Y such that
A5: ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A3, A4;
A6: x in X1 by A4, A5, ZFMISC_1:106;
take Y1 = Y1; :: thesis: ( Y1 is open & Y1 c= A & y in Y1 )
thus Y1 is open by A5; :: thesis: ( Y1 c= A & y in Y1 )
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 A5, A6, ZFMISC_1:106;
then ( [x,z] in W & x in {x} ) by A2, A4, TARSKI:def 1, TARSKI:def 4;
hence z in A by RELAT_1:def 13; :: thesis: verum

end;

thus y in Y1 by A4, A5, ZFMISC_1:106; :: 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:57; :: thesis: verum