let F, G be set ; :: thesis: ( F <> {} & G <> {} implies (meet F) /\ (meet G) = meet (INTERSECTION (F,G)) )
assume that
A1: F <> {} and
A2: G <> {} ; :: thesis: (meet F) /\ (meet G) = meet (INTERSECTION (F,G))
consider y being object such that
A3: y in F by ;
reconsider y = y as set by TARSKI:1;
consider z being object such that
A4: z in G by ;
reconsider z = z as set by TARSKI:1;
A5: meet (INTERSECTION (F,G)) c= (meet F) /\ (meet G)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (INTERSECTION (F,G)) or x in (meet F) /\ (meet G) )
assume A6: x in meet (INTERSECTION (F,G)) ; :: thesis: x in (meet F) /\ (meet G)
for Z being set st Z in G holds
x in Z
proof
let Z be set ; :: thesis: ( Z in G implies x in Z )
assume Z in G ; :: thesis: x in Z
then y /\ Z in INTERSECTION (F,G) by ;
then x in y /\ Z by ;
hence x in Z by XBOOLE_0:def 4; :: thesis: verum
end;
then A7: x in meet G by ;
for Z being set st Z in F holds
x in Z
proof
let Z be set ; :: thesis: ( Z in F implies x in Z )
assume Z in F ; :: thesis: x in Z
then Z /\ z in INTERSECTION (F,G) by ;
then x in Z /\ z by ;
hence x in Z by XBOOLE_0:def 4; :: thesis: verum
end;
then x in meet F by ;
hence x in (meet F) /\ (meet G) by ; :: thesis: verum
end;
A8: y /\ z in INTERSECTION (F,G) by ;
(meet F) /\ (meet G) c= meet (INTERSECTION (F,G))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (meet F) /\ (meet G) or x in meet (INTERSECTION (F,G)) )
assume x in (meet F) /\ (meet G) ; :: thesis: x in meet (INTERSECTION (F,G))
then A9: ( x in meet F & x in meet G ) by XBOOLE_0:def 4;
for Z being set st Z in INTERSECTION (F,G) holds
x in Z
proof
let Z be set ; :: thesis: ( Z in INTERSECTION (F,G) implies x in Z )
assume Z in INTERSECTION (F,G) ; :: thesis: x in Z
then consider Z1, Z2 being set such that
A10: ( Z1 in F & Z2 in G ) and
A11: Z = Z1 /\ Z2 by SETFAM_1:def 5;
( x in Z1 & x in Z2 ) by ;
hence x in Z by ; :: thesis: verum
end;
hence x in meet (INTERSECTION (F,G)) by ; :: thesis: verum
end;
hence (meet F) /\ (meet G) = meet (INTERSECTION (F,G)) by A5; :: thesis: verum