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 )
thus ( x c= meet Y implies for y being Element of Y holds x c= y ) by SETFAM_1:def 1; :: thesis: ( ( for y being Element of Y holds x c= y ) implies x c= meet Y )
assume A1: for y being Element of Y holds x c= y ; :: thesis: x c= meet Y
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in meet Y )
assume A2: z in x ; :: thesis: z in meet Y

now :: thesis: for u being set st u in Y holds
z in u

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 A1;
hence z in u by A2; :: thesis: verum

end;

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