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 ;

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 ) )

hence
Im (W,x) is open Subset of Y
by TOPS_1:25; :: thesis: verum( ( 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 ) )

( Q is open & Q c= A & y in Q ) implies y in A ) ; :: thesis: verum

end;( 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 )

thus
( 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

end;( 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

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

( Q is open & Q c= A & y in Q ) implies y in A ) ; :: thesis: verum