let X be set ; :: thesis: for S being Subset-Family of X
for XX being Subset of S holds
( union XX = X iff XX is Cover of X )
let S be Subset-Family of X; :: thesis: for XX being Subset of S holds
( union XX = X iff XX is Cover of X )
let XX be Subset of S; :: thesis: ( union XX = X iff XX is Cover of X )
XX is Subset-Family of X by XBOOLE_1:1;
hence ( union XX = X iff XX is Cover of X ) by SETFAM_1:45; :: thesis: verum