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
then not (" f) .: S is empty by SETFAM_1:def 1;
then A2: not S is empty by RELAT_1:149;

now

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

end;

hence f . x in meet S by A2, SETFAM_1:def 1; :: thesis: verum