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, XBOOLE_1:1; :: thesis: verum