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:81
.= E by ZFMISC_1:81 ;
hence ( sE is covering iff union sE = E ) ; :: thesis: verum