let T be non empty 1-sorted ; :: thesis: for F being Subset-Family of T st F is Cover of T holds
F <> {}
let F be Subset-Family of T; :: thesis: ( F is Cover of T implies F <> {} )
set x = the Element of union F;
assume F is Cover of T ; :: thesis: F <> {}
then union F = the carrier of T by SETFAM_1:45;
then ex A being set st
( the Element of union F in A & A in F ) by TARSKI:def 4;
hence F <> {} ; :: thesis: verum