let f be Function; :: thesis: ( f <> {} implies for x being object holds
( x in meet f iff for y being object st y in dom f holds
x in f . y ) )
assume A1: f <> {} ; :: thesis: for x being object holds
( x in meet f iff for y being object st y in dom f holds
x in f . y )
let x be object ; :: thesis: ( x in meet f iff for y being object st y in dom f holds
x in f . y )
thus ( x in meet f implies for y being object st y in dom f holds
x in f . y ) :: thesis: ( ( for y being object 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 object st y in dom f holds
x in f . y
let y be object ; :: 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 object st y in dom f holds
x in f . y ; :: thesis: x in meet f

now :: thesis: for z being set st z in rng f holds
x in z

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 object 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