theorem Th20: :: PENCIL_1:20

for S being identifying_close_blocks TopStruct
for l being Block of S
for L being Subset of S st L = l holds
L is closed_under_lines by Def7;