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 A1: ( (Prj2 (s,H)) . p in V & 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
A2: [s,p] in W and
A3: W is open and
A4: H .: W c= V by ;
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 ;
consider e being set such that
A7: [s,p] in e and
A8: e in A by ;
consider X1 being Subset of S, Y1 being Subset of T such that
A9: e = [:X1,Y1:] and
X1 is open and
A10: Y1 is open by A6, A8;
take Y1 ; :: thesis: ( p in Y1 & Y1 is open & (Prj2 (s,H)) .: Y1 c= V )
thus p in Y1 by ; :: thesis: ( Y1 is open & (Prj2 (s,H)) .: Y1 c= V )
thus Y1 is open by A10; :: thesis: (Prj2 (s,H)) .: Y1 c= V
let x be object ; :: 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
A11: c in Y1 and
A12: x = (Prj2 (s,H)) . c by FUNCT_2:65;
s in X1 by ;
then [s,c] in [:X1,Y1:] by ;
then [s,c] in W by ;
then A13: H . [s,c] in H .: W by FUNCT_2:35;
(Prj2 (s,H)) . c = H . (s,c) by Def3
.= H . [s,c] ;
hence x in V by A4, A12, A13; :: thesis: verum
end;
hence Prj2 (s,H) is continuous by JGRAPH_2:10; :: thesis: verum