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 <> {} )
assume F is Cover of T ; :: thesis: F <> {}
then A1: union F = the carrier of T by SETFAM_1:60;
consider x being Element of union F;
ex A being set st
( x in A & A in F ) by A1, TARSKI:def 4;
hence F <> {} ; :: thesis: verum