let T be TopSpace; :: thesis:
let F be Subset-Family of T; :: thesis:
assume A1: F is Cover of T ; :: thesis:

per cases ;

suppose A2: F is empty ; :: thesis:

take F ; :: thesis:
thus ( F c= F & F is Cover of T & card F c= card ([#] T) ) by A1, A2; :: thesis:

end;

suppose A3: not F is empty ; :: thesis:

defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & $1 in D2 );
A4: for x being object st x in [#] T holds
ex y being object st
( y in F & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in [#] T ; :: thesis:
then x in union F by A1, SETFAM_1:45;
then ex y being set st
( x in y & y in F ) by TARSKI:def 4;
hence ex y being object st
( y in F & S₁[x,y] ) ; :: thesis:

end;

consider g being Function of ([#] T),F such that
A5: for x being object st x in [#] T holds
S₁[x,g . x] from FUNCT_2:sch 1(A4);
reconsider R = rng g as Subset-Family of T by XBOOLE_1:1;
take R ; :: thesis:
A6: dom g = [#] T by A3, FUNCT_2:def 1;
[#] T c= union R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in [#] T ; :: thesis:
then S₁[x,g . x] by A5;
then ( x in g . x & g . x in R ) by A6, FUNCT_1:def 3, A7;
hence x in union R by TARSKI:def 4; :: thesis:

end;

hence ( R c= F & R is Cover of T & card R c= card ([#] T) ) by A6, CARD_1:12, SETFAM_1:def 11; :: thesis:

end;

end;