theorem Th1: :: TOPGEN_3:1

for X being set
for B being Subset-Family of X holds
( B is covering iff for x being set st x in X holds
ex U being Subset of X st
( U in B & x in U ) )