for p being Point of T
for V being Subset of Y st (Prj2 s,H) . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & (Prj2 s,H) .: W c= V )
proof
let p be
Point of
T;
:: thesis: for V being Subset of Y st (Prj2 s,H) . p in V & V is open holds
ex W being Subset of T st
( p in W & W is open & (Prj2 s,H) .: W c= V )let V be
Subset of
Y;
:: thesis: ( (Prj2 s,H) . p in V & V is open implies ex W being Subset of T st
( p in W & W is open & (Prj2 s,H) .: W c= V ) )
assume that A1:
(Prj2 s,H) . p in V
and A2:
V is
open
;
:: thesis: ex W being Subset of T st
( p in W & W is open & (Prj2 s,H) .: W c= V )
(Prj2 s,H) . p = H . s,
p
by Def3;
then consider W being
Subset of
[:S,T:] such that A3:
[s,p] in W
and A4:
W is
open
and A5:
H .: W c= V
by A1, A2, JGRAPH_2:20;
consider A being
Subset-Family of
[:S,T:] such that A6:
W = union A
and A7:
for
e being
set st
e in A holds
ex
X1 being
Subset of
S ex
Y1 being
Subset of
T st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
by A4, BORSUK_1:45;
consider e being
set such that A8:
[s,p] in e
and A9:
e in A
by A3, A6, TARSKI:def 4;
consider X1 being
Subset of
S,
Y1 being
Subset of
T such that A10:
e = [:X1,Y1:]
and
X1 is
open
and A11:
Y1 is
open
by A7, A9;
take
Y1
;
:: thesis: ( p in Y1 & Y1 is open & (Prj2 s,H) .: Y1 c= V )
thus
p in Y1
by A8, A10, ZFMISC_1:106;
:: thesis: ( Y1 is open & (Prj2 s,H) .: Y1 c= V )
thus
Y1 is
open
by A11;
:: thesis: (Prj2 s,H) .: Y1 c= V
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (Prj2 s,H) .: Y1 or x in V )
assume
x in (Prj2 s,H) .: Y1
;
:: thesis: x in V
then consider c being
Point of
T such that A12:
c in Y1
and A13:
x = (Prj2 s,H) . c
by FUNCT_2:116;
A14:
(Prj2 s,H) . c =
H . s,
c
by Def3
.=
H . [s,c]
;
s in X1
by A8, A10, ZFMISC_1:106;
then
[s,c] in [:X1,Y1:]
by A12, ZFMISC_1:106;
then
[s,c] in W
by A6, A9, A10, TARSKI:def 4;
then
H . [s,c] in H .: W
by FUNCT_2:43;
hence
x in V
by A5, A13, A14;
:: thesis: verum
end;
hence
Prj2 s,H is continuous
by JGRAPH_2:20; :: thesis: verum