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)

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 )
;

end;

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;( 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

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;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