let Y be non empty set ; :: thesis: for x being set holds
( x c= meet Y iff for y being Element of Y holds x c= y )
let x be set ; :: thesis: ( x c= meet Y iff for y being Element of Y holds x c= y )

hereby :: thesis: ( ( for y being Element of Y holds x c= y ) implies x c= meet Y )

assume A1: x c= meet Y ; :: thesis: for y being Element of Y holds x c= y
let y be Element of Y; :: thesis: x c= y
for z being set st z in x holds
z in y by A1, SETFAM_1:def 1;
hence x c= y by TARSKI:def 3; :: thesis: verum

end;

assume A2: for y being Element of Y holds x c= y ; :: thesis: x c= meet Y
for z being set st z in x holds
z in meet Y

proof

let z be set ; :: thesis: ( z in x implies z in meet Y )
assume A3: z in x ; :: thesis: z in meet Y

now

let u be set ; :: thesis: ( u in Y implies z in u )
assume u in Y ; :: thesis: z in u
then x c= u by A2;
hence z in u by A3; :: thesis: verum

end;

hence z in meet Y by SETFAM_1:def 1; :: thesis: verum

end;

hence x c= meet Y by TARSKI:def 3; :: thesis: verum