theorem :: NORMFORM:30

for X being set
for a being Element of DISJOINT_PAIRS X
for V, W being set st V c= a `1 & W c= a `2 holds
[V,W] is Element of DISJOINT_PAIRS X