let T, S be non empty set ; :: thesis: for f being Function of T,S
for B being Subset-Family of S
for P being Subset of S st f .: (f " B) is Cover of P holds
B is Cover of P
let f be Function of T,S; :: thesis: for B being Subset-Family of S
for P being Subset of S st f .: (f " B) is Cover of P holds
B is Cover of P
let B be Subset-Family of S; :: thesis: for P being Subset of S st f .: (f " B) is Cover of P holds
B is Cover of P
let P be Subset of S; :: thesis: ( f .: (f " B) is Cover of P implies B is Cover of P )
assume f .: (f " B) is Cover of P ; :: thesis: B is Cover of P
then A1: P c= union (f .: (f " B)) by SETFAM_1:def 12;
P c= union B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in union B )
assume x in P ; :: thesis: x in union B
then consider Y being set such that
A2: ( x in Y & Y in f .: (f " B) ) by A1, TARSKI:def 4;
ex Z being set st
( x in Z & Z in B )

proof

reconsider Y = Y as Subset of S by A2;
consider Y1 being Subset of T such that
A3: ( Y1 in f " B & Y = f .: Y1 ) by A2, Def2a;
consider Y2 being Subset of S such that
A4: ( Y2 in B & Y1 = f " Y2 ) by A3, Def10;
A5: f .: (f " Y2) c= Y2 by FUNCT_1:145;
reconsider Y2 = Y2 as set ;
take Y2 ; :: thesis: ( x in Y2 & Y2 in B )
thus ( x in Y2 & Y2 in B ) by A2, A3, A4, A5; :: thesis: verum

end;

hence x in union B by TARSKI:def 4; :: thesis: verum

end;

hence B is Cover of P by SETFAM_1:def 12; :: thesis: verum