theorem Th48: :: NOMIN_1:48

for a1, v, v1 being object
for V, A being set st {v,v1} c= V & a1 in A holds
ND_ex_2 (v,v1,a1) in NDSS (V,(A \/ (NDSS (V,A))))