let SFX, SFY be set ; :: thesis: ( SFX meets SFY implies (meet SFX) /\ (meet SFY) = meet (INTERSECTION SFX,SFY) )
consider y being Element of SFX /\ SFY;
assume A1: SFX /\ SFY <> {} ; :: according to XBOOLE_0:def 7 :: thesis: (meet SFX) /\ (meet SFY) = meet (INTERSECTION SFX,SFY)
then A2: SFY <> {} ;
A3: y in SFX by A1, XBOOLE_0:def 4;
A4: y in SFY by A1, XBOOLE_0:def 4;
A5: SFX <> {} by A1;
A6: meet (INTERSECTION SFX,SFY) c= (meet SFX) /\ (meet SFY)

proof

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

proof

let Z be set ; :: thesis: ( Z in SFY implies x in Z )
assume Z in SFY ; :: thesis: x in Z
then y /\ Z in INTERSECTION SFX,SFY by A3, Def5;
then x in y /\ Z by A7, Def1;
hence x in Z by XBOOLE_0:def 4; :: thesis: verum

end;

then A8: x in meet SFY by A2, Def1;
for Z being set st Z in SFX holds
x in Z

proof

let Z be set ; :: thesis: ( Z in SFX implies x in Z )
assume Z in SFX ; :: thesis: x in Z
then Z /\ y in INTERSECTION SFX,SFY by A4, Def5;
then x in Z /\ y by A7, Def1;
hence x in Z by XBOOLE_0:def 4; :: thesis: verum

end;

then x in meet SFX by A5, Def1;
hence x in (meet SFX) /\ (meet SFY) by A8, XBOOLE_0:def 4; :: thesis: verum

end;

A9: y /\ y in INTERSECTION SFX,SFY by A3, A4, Def5;
(meet SFX) /\ (meet SFY) c= meet (INTERSECTION SFX,SFY)

proof

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

proof

let Z be set ; :: thesis: ( Z in INTERSECTION SFX,SFY implies x in Z )
assume Z in INTERSECTION SFX,SFY ; :: thesis: x in Z
then consider Z1, Z2 being set such that
A11: ( Z1 in SFX & Z2 in SFY ) and
A12: Z = Z1 /\ Z2 by Def5;
( x in Z1 & x in Z2 ) by A10, A11, Def1;
hence x in Z by A12, XBOOLE_0:def 4; :: thesis: verum

end;

hence x in meet (INTERSECTION SFX,SFY) by A9, Def1; :: thesis: verum

end;

hence (meet SFX) /\ (meet SFY) = meet (INTERSECTION SFX,SFY) by A6, XBOOLE_0:def 10; :: thesis: verum