let a, a1, v, v1 be object ; :: thesis: for V, A being set st {v,v1} c= V & {a,a1} c= A holds
ND_ex_3 (v,v1,a,a1) in NDSS (V,A)
let V, A be set ; :: thesis: ( {v,v1} c= V & {a,a1} c= A implies ND_ex_3 (v,v1,a,a1) in NDSS (V,A) )
assume that
A1: {v,v1} c= V and
A2: {a,a1} c= A ; :: thesis: ND_ex_3 (v,v1,a,a1) in NDSS (V,A)

per cases ( v = v1 or v <> v1 ) ;

suppose v = v1 ; :: thesis: ND_ex_3 (v,v1,a,a1) in NDSS (V,A)

then A3: ND_ex_3 (v,v1,a,a1) = ND_ex_1 (v1,a1) by FUNCT_4:81;
( v1 in V & a1 in A ) by A1, A2, ZFMISC_1:32;
hence ND_ex_3 (v,v1,a,a1) in NDSS (V,A) by A3, Th45; :: thesis: verum

end;

suppose v <> v1 ; :: thesis: ND_ex_3 (v,v1,a,a1) in NDSS (V,A)

then {v} misses {v1} by ZFMISC_1:11;
then A4: ND_ex_1 (v,a) tolerates ND_ex_1 (v1,a1) by FUNCOP_1:87;
( v in V & v1 in V & a in A & a1 in A ) by A1, A2, ZFMISC_1:32;
then A5: ( ND_ex_1 (v,a) in NDSS (V,A) & ND_ex_1 (v1,a1) in NDSS (V,A) ) by Th45;
ND_ex_3 (v,v1,a,a1) = (ND_ex_1 (v,a)) \/ (ND_ex_1 (v1,a1)) by A4, FUNCT_4:30;
hence ND_ex_3 (v,v1,a,a1) in NDSS (V,A) by A4, A5, Th8; :: thesis: verum

end;

end;