l in the topology of S ;
then reconsider L = l as Subset of S ;
A1: L is open by PRE_TOPC:def 2;
f is open by Def4;
then f .: L is open by A1, T_0TOPSP:def 2;
hence f .: l is Block of S by PRE_TOPC:def 2; :: thesis: verum