let x be set ; :: thesis: for f being Function st f <> {} holds
( x in meet f iff for y being set st y in dom f holds
x in f . y )
let f be Function; :: thesis: ( f <> {} implies ( x in meet f iff for y being set st y in dom f holds
x in f . y ) )
assume A1: f <> {} ; :: thesis: ( x in meet f iff for y being set st y in dom f holds
x in f . y )
thus ( x in meet f implies for y being set st y in dom f holds
x in f . y ) :: thesis: ( ( for y being set st y in dom f holds
x in f . y ) implies x in meet f )

proof

assume A2: x in meet f ; :: thesis: for y being set st y in dom f holds
x in f . y
let y be set ; :: thesis: ( y in dom f implies x in f . y )
assume y in dom f ; :: thesis: x in f . y
then f . y in rng f by FUNCT_1:def 3;
then meet f c= f . y by SETFAM_1:3;
hence x in f . y by A2; :: thesis: verum

end;

assume A3: for y being set st y in dom f holds
x in f . y ; :: thesis: x in meet f

now

let z be set ; :: thesis: ( z in rng f implies x in z )
assume z in rng f ; :: thesis: x in z
then ex y being set st
( y in dom f & z = f . y ) by FUNCT_1:def 3;
hence x in z by A3; :: thesis: verum

end;

hence x in meet f by A1, SETFAM_1:def 1; :: thesis: verum