theorem :: HEYTING1:2

for A being set
for B being Element of Fin (DISJOINT_PAIRS A) st B = {} holds
mi B = {} by NORMFORM:40, XBOOLE_1:3;