for F, G, H being ext-real-membered set holds (F /\ G) /// H c= (F /// H) /\ (G /// H) by Th83;