let X, Y be set ; :: thesis: for S being cap-closed Subset-Family of X
for f being Function of X,Y st f is one-to-one holds
f .: S is cap-closed Subset-Family of Y
let S be cap-closed Subset-Family of X; :: thesis: for f being Function of X,Y st f is one-to-one holds
f .: S is cap-closed Subset-Family of Y
let f be Function of X,Y; :: thesis: ( f is one-to-one implies f .: S is cap-closed Subset-Family of Y )
assume A1: f is one-to-one ; :: thesis: f .: S is cap-closed Subset-Family of Y

now :: thesis: for s1, s2 being set st s1 in f .: S & s2 in f .: S holds
s1 /\ s2 in f .: S

let s1, s2 be set ; :: thesis: ( s1 in f .: S & s2 in f .: S implies s1 /\ s2 in f .: S )
assume A2: ( s1 in f .: S & s2 in f .: S ) ; :: thesis: s1 /\ s2 in f .: S
consider c1 being Subset of X such that
A3: c1 in S and
A4: s1 = f .: c1 by A2, FUNCT_2:def 10;
consider c2 being Subset of X such that
A5: c2 in S and
A6: s2 = f .: c2 by A2, FUNCT_2:def 10;
reconsider f12 = f .: (c1 /\ c2) as Subset of Y ;
c1 /\ c2 in S by A3, A5, FINSUB_1:def 2;
then f12 in f .: S by FUNCT_2:def 10;
hence s1 /\ s2 in f .: S by A1, A4, A6, FUNCT_1:62; :: thesis: verum

end;

hence f .: S is cap-closed Subset-Family of Y by FINSUB_1:def 2; :: thesis: verum