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

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

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

end;

end;