let S be TopStruct ; :: thesis: for l being Block of S
for L being Subset of S st L = l holds
L is strong
let l be Block of S; :: thesis: for L being Subset of S st L = l holds
L is strong
let L be Subset of S; :: thesis: ( L = l implies L is strong )
assume A1: L = l ; :: thesis: L is strong
thus L is strong :: thesis: verum
proof
let x, y be Point of S; :: according to PENCIL_1:def 3 :: thesis: ( x in L & y in L implies x,y are_collinear )
assume ( x in L & y in L ) ; :: thesis: x,y are_collinear
then {x,y} c= l by A1, ZFMISC_1:32;
hence x,y are_collinear ; :: thesis: verum
end;