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

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