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)

(meet SFX) /\ (meet SFY) c= 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

A9:
the Element of SFX /\ SFY /\ the Element of SFX /\ SFY in INTERSECTION (SFX,SFY)
by A3, A4, Def5;
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

for Z being set st Z in SFX holds

x in Z

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

end;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

then A8:
x in meet SFY
by A2, Def1;
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;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

for Z being set st Z in SFX holds

x in Z

proof

then
x in meet SFX
by A5, Def1;
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;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

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

(meet SFX) /\ (meet SFY) c= meet (INTERSECTION (SFX,SFY))

proof

hence
(meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY))
by A6; :: thesis: verum
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

end;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

hence
x in meet (INTERSECTION (SFX,SFY))
by A9, Def1; :: thesis: verum
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;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