let SFX, SFY be set ; ( SFX meets SFY implies (meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY)) )
set y = the Element of SFX /\ SFY;
assume A1:
SFX /\ SFY <> {}
; XBOOLE_0:def 7 (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)
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))
hence
(meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY))
by A6; verum