A1: ( f " is open & f is bijective ) by Def4;
then A2: ( f is one-to-one & f is onto ) ;
l in the topology of S ;
then reconsider L = l as Subset of S ;
rng f = the carrier of S by A2, FUNCT_2:def 3;
then f " = f " by A2, TOPS_2:def 4;
then A3: (f " ) .: L = f " L by A2, FUNCT_1:155;
L is open by PRE_TOPC:def 5;
then (f " ) .: L is open by A1, T_0TOPSP:def 2;
hence f " l is Block of S by A3, PRE_TOPC:def 5; :: thesis: verum