let SFX, SFY be set ; :: thesis: ( SFX meets SFY implies (meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY)) )
set y = the 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: the Element of SFX /\ SFY in SFX by A1, XBOOLE_0:def 4;
A4: the Element of SFX /\ SFY 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 object ; :: 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 the Element of SFX /\ SFY /\ Z in INTERSECTION (SFX,SFY) by A3, Def5;
then x in the Element of SFX /\ SFY /\ 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 /\ the Element of SFX /\ SFY in INTERSECTION (SFX,SFY) by A4, Def5;
then x in Z /\ the Element of SFX /\ SFY 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: the Element of SFX /\ SFY /\ the Element of SFX /\ SFY in INTERSECTION (SFX,SFY) by A3, A4, Def5;
(meet SFX) /\ (meet SFY) c= meet (INTERSECTION (SFX,SFY))

proof

let x be object ; :: 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; :: thesis: verum