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

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