l in the topology of S ;
then reconsider L = l as Subset of S ;
A1: L is open by PRE_TOPC:def 5;
A2: f is bijective by Def4;
then rng f = the carrier of S by FUNCT_2:def 3;
then f " = f " by A2, TOPS_2:def 4;
then A3: (f " ) .: L = f " L by A2, FUNCT_1:155;
f " is open by Def4;
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