let x be object ; :: thesis: for V, A being set st x in (ND (V,A)) \ A holds

x is NonatomicND of V,A

let V, A be set ; :: thesis: ( x in (ND (V,A)) \ A implies x is NonatomicND of V,A )

assume A1: x in (ND (V,A)) \ A ; :: thesis: x is NonatomicND of V,A

then x in ND (V,A) ;

then A2: ex w being TypeSCNominativeData of V,A st x = w ;

not x in A by A1, XBOOLE_0:def 5;

hence x is NonatomicND of V,A by A2, Def6; :: thesis: verum

x is NonatomicND of V,A

let V, A be set ; :: thesis: ( x in (ND (V,A)) \ A implies x is NonatomicND of V,A )

assume A1: x in (ND (V,A)) \ A ; :: thesis: x is NonatomicND of V,A

then x in ND (V,A) ;

then A2: ex w being TypeSCNominativeData of V,A st x = w ;

not x in A by A1, XBOOLE_0:def 5;

hence x is NonatomicND of V,A by A2, Def6; :: thesis: verum