let E be set ; :: thesis: for sE being Subset-Family of holds
( sE is covering iff union sE = E )
let sE be Subset-Family of ; :: thesis: ( sE is covering iff union sE = E )
union (union (bool (bool E))) = union (bool E) by ZFMISC_1:99
.= E by ZFMISC_1:99 ;
hence ( sE is covering iff union sE = E ) by Def6; :: thesis: verum