let V, A be set ; :: thesis: for D being NonatomicND of V,A st not D in A holds
D in (ND (V,A)) \ A
let D be NonatomicND of V,A; :: thesis: ( not D in A implies D in (ND (V,A)) \ A )
D in ND (V,A) by Th41;
hence ( not D in A implies D in (ND (V,A)) \ A ) by XBOOLE_0:def 5; :: thesis: verum