let S be non void TopStruct ; :: thesis: [#] S is closed_under_lines
thus [#] S is closed_under_lines :: thesis: verum
proof
let K be Block of S; :: according to PENCIL_1:def 2 :: thesis: ( 2 c= card (K /\ ([#] S)) implies K c= [#] S )
assume 2 c= card (K /\ ([#] S)) ; :: thesis: K c= [#] S
K in the topology of S ;
hence K c= [#] S ; :: thesis: verum
end;