theorem Th18: :: YELLOW13:18

for T being TopStruct
for p being Point of T holds bool the carrier of T is basis of p