let a, v be object ; :: thesis: for V, A being set st v in V & a in A holds

ND_ex_1 (v,a) in NDSS (V,A)

let V, A be set ; :: thesis: ( v in V & a in A implies ND_ex_1 (v,a) in NDSS (V,A) )

assume that

A1: v in V and

A2: a in A ; :: thesis: ND_ex_1 (v,a) in NDSS (V,A)

reconsider V1 = V, A1 = A as non empty set by A1, A2;

reconsider v = v as Element of V1 by A1;

reconsider a = a as Element of A1 by A2;

v .--> a in NDSS (V,A) ;

hence ND_ex_1 (v,a) in NDSS (V,A) ; :: thesis: verum

ND_ex_1 (v,a) in NDSS (V,A)

let V, A be set ; :: thesis: ( v in V & a in A implies ND_ex_1 (v,a) in NDSS (V,A) )

assume that

A1: v in V and

A2: a in A ; :: thesis: ND_ex_1 (v,a) in NDSS (V,A)

reconsider V1 = V, A1 = A as non empty set by A1, A2;

reconsider v = v as Element of V1 by A1;

reconsider a = a as Element of A1 by A2;

v .--> a in NDSS (V,A) ;

hence ND_ex_1 (v,a) in NDSS (V,A) ; :: thesis: verum