let S be identifying_close_blocks TopStruct ; :: thesis: for l being Block of S
for L being Subset of S st L = l holds
L is closed_under_lines
let l be Block of S; :: thesis: for L being Subset of S st L = l holds
L is closed_under_lines
let L be Subset of S; :: thesis: ( L = l implies L is closed_under_lines )
assume A1: L = l ; :: thesis: L is closed_under_lines
thus L is closed_under_lines :: thesis: verum

proof

let K be Block of S; :: according to PENCIL_1:def 2 :: thesis: ( 2 c= card (K /\ L) implies K c= L )
assume 2 c= card (K /\ L) ; :: thesis: K c= L
hence K c= L by A1, Def7; :: thesis: verum

end;