let F, G, H be ext-real-membered set ; :: thesis: F -- (G /\ H) c= (F -- G) /\ (F -- H)
F -- (G /\ H) = F ++ ((-- G) /\ (-- H)) by Th6;
hence F -- (G /\ H) c= (F -- G) /\ (F -- H) by Th42; :: thesis: verum