A1: f is open by Def4;
l in the topology of S ;
then reconsider L = l as Subset of S ;
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 PRE_TOPC:def 5; :: thesis: verum