for T being TopStruct
for p being Point of T holds { A where A is Subset of T : p in Int A } is correct basis of p by Lm4, Lm5;