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

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