theorem :: SETFAM_1:9

for X, Y being set st X <> {} & Y <> {} holds
meet (X \/ Y) = (meet X) /\ (meet Y)