let X, Y, x be set ; :: thesis: for S being Subset-Family of Y
for f being Function of X,Y st x in meet ((" f) .: S) holds
f . x in meet S
let S be Subset-Family of Y; :: thesis: for f being Function of X,Y st x in meet ((" f) .: S) holds
f . x in meet S
let f be Function of X,Y; :: thesis: ( x in meet ((" f) .: S) implies f . x in meet S )
assume A1: x in meet ((" f) .: S) ; :: thesis: f . x in meet S

A2: now :: thesis: for SS being set st SS in S holds
f . x in SS

let SS be set ; :: thesis: ( SS in S implies f . x in SS )
assume A3: SS in S ; :: thesis: f . x in SS
then (" f) . SS in (" f) .: S by FUNCT_2:35;
then A4: x in (" f) . SS by A1, SETFAM_1:def 1;
(" f) . SS = f " SS by A3, Def2;
hence f . x in SS by A4, FUNCT_1:def 7; :: thesis: verum

end;

not (" f) .: S is empty by A1, SETFAM_1:def 1;
then not S is empty ;
hence f . x in meet S by A2, SETFAM_1:def 1; :: thesis: verum