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