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