theorem :: YELLOW_9:27

for T being TopSpace
for K being Basis of T holds
( K is open & K is prebasis of T ) ;