thus not nonatomicsND (V,A) is empty by Th2; :: thesis: nonatomicsND (V,A) is functional
let v be object ; :: according to FUNCT_1:def 13 :: thesis: ( not v in nonatomicsND (V,A) or v is set )
thus ( not v in nonatomicsND (V,A) or v is set ) by Th1; :: thesis: verum