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 )

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

hence
Prj1 (t,H) is continuous
by JGRAPH_2:10; :: thesis: verum
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 A1: ( (Prj1 (t,H)) . p in V & 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

A2: [p,t] in W and

A3: W is open and

A4: H .: W c= V by A1, JGRAPH_2:10;

consider A being Subset-Family of [:S,T:] such that

A5: W = union A and

A6: 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 A3, BORSUK_1:5;

consider e being set such that

A7: [p,t] in e and

A8: e in A by A2, A5, TARSKI:def 4;

consider X1 being Subset of S, Y1 being Subset of T such that

A9: e = [:X1,Y1:] and

A10: X1 is open and

Y1 is open by A6, A8;

take X1 ; :: thesis: ( p in X1 & X1 is open & (Prj1 (t,H)) .: X1 c= V )

thus p in X1 by A7, A9, ZFMISC_1:87; :: thesis: ( X1 is open & (Prj1 (t,H)) .: X1 c= V )

thus X1 is open by A10; :: thesis: (Prj1 (t,H)) .: X1 c= V

let x be object ; :: 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

A11: c in X1 and

A12: x = (Prj1 (t,H)) . c by FUNCT_2:65;

t in Y1 by A7, A9, ZFMISC_1:87;

then [c,t] in [:X1,Y1:] by A11, ZFMISC_1:87;

then [c,t] in W by A5, A8, A9, TARSKI:def 4;

then A13: H . [c,t] in H .: W by FUNCT_2:35;

(Prj1 (t,H)) . c = H . (c,t) by Def2

.= H . [c,t] ;

hence x in V by A4, A12, A13; :: thesis: verum

end;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 A1: ( (Prj1 (t,H)) . p in V & 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

A2: [p,t] in W and

A3: W is open and

A4: H .: W c= V by A1, JGRAPH_2:10;

consider A being Subset-Family of [:S,T:] such that

A5: W = union A and

A6: 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 A3, BORSUK_1:5;

consider e being set such that

A7: [p,t] in e and

A8: e in A by A2, A5, TARSKI:def 4;

consider X1 being Subset of S, Y1 being Subset of T such that

A9: e = [:X1,Y1:] and

A10: X1 is open and

Y1 is open by A6, A8;

take X1 ; :: thesis: ( p in X1 & X1 is open & (Prj1 (t,H)) .: X1 c= V )

thus p in X1 by A7, A9, ZFMISC_1:87; :: thesis: ( X1 is open & (Prj1 (t,H)) .: X1 c= V )

thus X1 is open by A10; :: thesis: (Prj1 (t,H)) .: X1 c= V

let x be object ; :: 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

A11: c in X1 and

A12: x = (Prj1 (t,H)) . c by FUNCT_2:65;

t in Y1 by A7, A9, ZFMISC_1:87;

then [c,t] in [:X1,Y1:] by A11, ZFMISC_1:87;

then [c,t] in W by A5, A8, A9, TARSKI:def 4;

then A13: H . [c,t] in H .: W by FUNCT_2:35;

(Prj1 (t,H)) . c = H . (c,t) by Def2

.= H . [c,t] ;

hence x in V by A4, A12, A13; :: thesis: verum