theorem :: TOPMETR:1

for T being TopStruct
for F being Subset-Family of T holds
( F is Cover of T iff the carrier of T c= union F ) by SETFAM_1:def 11;