theorem :: SETFAM_1:45

for X being set
for F being Subset-Family of X holds
( F is Cover of X iff union F = X ) by Def11;