let F, G, H be ext-real-membered set ; :: thesis: F /// (G /\ H) c= (F /// G) /\ (F /// H)
(G /\ H) "" c= (G "") /\ (H "") by Th24;
then A1: F ** ((G /\ H) "") c= F ** ((G "") /\ (H "")) by Th81;
F ** ((G "") /\ (H "")) c= (F ** (G "")) /\ (F ** (H "")) by Th83;
hence F /// (G /\ H) c= (F /// G) /\ (F /// H) by A1; :: thesis: verum