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 A1, XBOOLE_0:def 1;

reconsider y = y as set by TARSKI:1;

consider z being object such that

A4: z in G by A2, XBOOLE_0:def 1;

reconsider z = z as set by TARSKI:1;

A5: meet (INTERSECTION (F,G)) c= (meet F) /\ (meet G)

(meet F) /\ (meet G) c= 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 A1, XBOOLE_0:def 1;

reconsider y = y as set by TARSKI:1;

consider z being object such that

A4: z in G by A2, XBOOLE_0:def 1;

reconsider z = z as set by TARSKI:1;

A5: meet (INTERSECTION (F,G)) c= (meet F) /\ (meet G)

proof

A8:
y /\ z in INTERSECTION (F,G)
by A3, A4, SETFAM_1:def 5;
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

for Z being set st Z in F holds

x in Z

hence x in (meet F) /\ (meet G) by A7, XBOOLE_0:def 4; :: thesis: verum

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

then A7:
x in meet G
by A2, SETFAM_1:def 1;
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 A3, SETFAM_1:def 5;

then x in y /\ Z by A6, SETFAM_1:def 1;

hence x in Z by XBOOLE_0:def 4; :: thesis: verum

end;assume Z in G ; :: thesis: x in Z

then y /\ Z in INTERSECTION (F,G) by A3, SETFAM_1:def 5;

then x in y /\ Z by A6, SETFAM_1:def 1;

hence x in Z by XBOOLE_0:def 4; :: thesis: verum

for Z being set st Z in F holds

x in Z

proof

then
x in meet F
by A1, SETFAM_1:def 1;
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 A4, SETFAM_1:def 5;

then x in Z /\ z by A6, SETFAM_1:def 1;

hence x in Z by XBOOLE_0:def 4; :: thesis: verum

end;assume Z in F ; :: thesis: x in Z

then Z /\ z in INTERSECTION (F,G) by A4, SETFAM_1:def 5;

then x in Z /\ z by A6, SETFAM_1:def 1;

hence x in Z by XBOOLE_0:def 4; :: thesis: verum

hence x in (meet F) /\ (meet G) by A7, XBOOLE_0:def 4; :: thesis: verum

(meet F) /\ (meet G) c= meet (INTERSECTION (F,G))

proof

hence
(meet F) /\ (meet G) = meet (INTERSECTION (F,G))
by A5; :: thesis: verum
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

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

hence
x in meet (INTERSECTION (F,G))
by A8, SETFAM_1:def 1; :: thesis: verum
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 A9, A10, SETFAM_1:def 1;

hence x in Z by A11, XBOOLE_0:def 4; :: thesis: verum

end;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 A9, A10, SETFAM_1:def 1;

hence x in Z by A11, XBOOLE_0:def 4; :: thesis: verum