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 ;
A4: the Element of SFX /\ SFY in SFY by ;
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 ;
then x in the Element of SFX /\ SFY /\ Z by ;
hence x in Z by XBOOLE_0:def 4; :: thesis: verum
end;
then A8: x in meet SFY by ;
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 ;
then x in Z /\ the Element of SFX /\ SFY by ;
hence x in Z by XBOOLE_0:def 4; :: thesis: verum
end;
then x in meet SFX by ;
hence x in (meet SFX) /\ (meet SFY) by ; :: 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 ;
hence x in Z by ; :: thesis: verum
end;
hence x in meet (INTERSECTION (SFX,SFY)) by ; :: thesis: verum
end;
hence (meet SFX) /\ (meet SFY) = meet (INTERSECTION (SFX,SFY)) by A6; :: thesis: verum