let F, G be set ; :: thesis: ( F <> {} & G <> {} implies (meet F) /\ (meet G) = meet (INTERSECTION F,G) )
assume A1: ( F <> {} & G <> {} ) ; :: thesis: (meet F) /\ (meet G) = meet (INTERSECTION F,G)
then consider y being set such that
A2: y in F by XBOOLE_0:def 1;
consider z being set such that
A3: z in G by A1, XBOOLE_0:def 1;
A4: y /\ z in INTERSECTION F,G by A2, A3, SETFAM_1:def 5;
A5: (meet F) /\ (meet G) c= meet (INTERSECTION F,G)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (meet F) /\ (meet G) or x in meet (INTERSECTION F,G) )
assume x in (meet F) /\ (meet G) ; :: thesis: x in meet (INTERSECTION F,G)
then A6: ( x in meet F & x in meet G ) by XBOOLE_0:def 4;
for Z being set st Z in INTERSECTION F,G holds
x in Z

proof

let Z be set ; :: thesis: ( Z in INTERSECTION F,G implies x in Z )
assume Z in INTERSECTION F,G ; :: thesis: x in Z
then consider Z1, Z2 being set such that
A7: ( Z1 in F & Z2 in G & Z = Z1 /\ Z2 ) by SETFAM_1:def 5;
( x in Z1 & x in Z2 ) by A6, A7, SETFAM_1:def 1;
hence x in Z by A7, XBOOLE_0:def 4; :: thesis: verum

end;

hence x in meet (INTERSECTION F,G) by A4, SETFAM_1:def 1; :: thesis: verum

end;

meet (INTERSECTION F,G) c= (meet F) /\ (meet G)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (INTERSECTION F,G) or x in (meet F) /\ (meet G) )
assume A8: x in meet (INTERSECTION F,G) ; :: thesis: x in (meet F) /\ (meet G)
for Z being set st Z in F holds
x in Z

proof

let Z be set ; :: thesis: ( Z in F implies x in Z )
assume Z in F ; :: thesis: x in Z
then Z /\ z in INTERSECTION F,G by A3, SETFAM_1:def 5;
then x in Z /\ z by A8, SETFAM_1:def 1;
hence x in Z by XBOOLE_0:def 4; :: thesis: verum

end;

then A9: x in meet F by A1, SETFAM_1:def 1;
for Z being set st Z in G holds
x in Z

proof

let Z be set ; :: thesis: ( Z in G implies x in Z )
assume Z in G ; :: thesis: x in Z
then y /\ Z in INTERSECTION F,G by A2, SETFAM_1:def 5;
then x in y /\ Z by A8, SETFAM_1:def 1;
hence x in Z by XBOOLE_0:def 4; :: thesis: verum

end;

then x in meet G by A1, SETFAM_1:def 1;
hence x in (meet F) /\ (meet G) by A9, XBOOLE_0:def 4; :: thesis: verum

end;

hence (meet F) /\ (meet G) = meet (INTERSECTION F,G) by A5, XBOOLE_0:def 10; :: thesis: verum