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