theorem :: TOPALG_3:11

for T being TopSpace ex F being Subset-Family of T st
( F = { the carrier of T} & F is Cover of T & F is open )