reconsider sE = {E} as Subset-Family of E by ZFMISC_1:68;
take sE ; :: thesis: ( not sE is empty & sE is finite & sE is covering )
thus ( not sE is empty & sE is finite ) ; :: thesis: sE is covering
union sE = E by ZFMISC_1:25;
hence sE is covering by Th4; :: thesis: verum