for F, G being set st F <> {} & G <> {} holds
(meet F) /\ (meet G) = meet (INTERSECTION (F,G))