let T, S be TopSpace; :: thesis: for f being Function of T,S holds
( f is open iff ex B being Basis of T st
for V being Subset of T st V in B holds
f .: V is open )
let f be Function of T,S; :: thesis: ( f is open iff ex B being Basis of T st
for V being Subset of T st V in B holds
f .: V is open )

hereby :: thesis: ( ex B being Basis of T st
for V being Subset of T st V in B holds
f .: V is open implies f is open )

assume A1: f is open ; :: thesis: ex B being Basis of T st
for V being Subset of T st V in B holds
f .: V is open
reconsider B = the Basis of T as Basis of T ;
take B = B; :: thesis: for V being Subset of T st V in B holds
f .: V is open
let V be Subset of T; :: thesis: ( V in B implies f .: V is open )
assume V in B ; :: thesis: f .: V is open
hence f .: V is open by A1, TOPS_2:def 1, T_0TOPSP:def 2; :: thesis: verum

end;

given B being Basis of T such that A2: for V being Subset of T st V in B holds
f .: V is open ; :: thesis: f is open

now :: thesis: for A being Subset of T st A is open holds
f .: A is open

let A be Subset of T; :: thesis: ( A is open implies f .: A is open )
set Y = { G where G is Subset of T : ( G in B & G c= A ) } ;
{ G where G is Subset of T : ( G in B & G c= A ) } c= bool the carrier of T

proof

let g be object ; :: according to TARSKI:def 3 :: thesis: ( not g in { G where G is Subset of T : ( G in B & G c= A ) } or g in bool the carrier of T )
assume g in { G where G is Subset of T : ( G in B & G c= A ) } ; :: thesis: g in bool the carrier of T
then ex G being Subset of T st
( g = G & G in B & G c= A ) ;
hence g in bool the carrier of T ; :: thesis: verum

end;

then reconsider Y = { G where G is Subset of T : ( G in B & G c= A ) } as Subset-Family of T ;
set Z = { (f .: G) where G is Subset of T : G in Y } ;
{ (f .: G) where G is Subset of T : G in Y } c= bool the carrier of S

proof

let h be object ; :: according to TARSKI:def 3 :: thesis: ( not h in { (f .: G) where G is Subset of T : G in Y } or h in bool the carrier of S )
assume h in { (f .: G) where G is Subset of T : G in Y } ; :: thesis: h in bool the carrier of S
then ex G being Subset of T st
( h = f .: G & G in Y ) ;
hence h in bool the carrier of S ; :: thesis: verum

end;

then reconsider Z = { (f .: G) where G is Subset of T : G in Y } as Subset-Family of S ;
A7: for P being Subset of S st P in Z holds
P is open

proof

let P be Subset of S; :: thesis: ( P in Z implies P is open )
assume P in Z ; :: thesis: P is open
then consider G1 being Subset of T such that
A5: ( P = f .: G1 & G1 in Y ) ;
ex G2 being Subset of T st
( G1 = G2 & G2 in B & G2 c= A ) by A5;
hence P is open by A2, A5; :: thesis: verum

end;

assume A is open ; :: thesis: f .: A is open
then A = union Y by YELLOW_8:9;
then f .: A = union Z by RELSET_2:14;
hence f .: A is open by A7, TOPS_2:19, TOPS_2:def 1; :: thesis: verum

end;

hence f is open by T_0TOPSP:def 2; :: thesis: verum