let E be set ; :: thesis: for sE being Subset-Family of E holds
( sE is covering iff union sE = E )
let sE be Subset-Family of E; :: 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