let x be set ; :: according to FUNCT_1:def 13 :: thesis: ( not x in D * or x is set )
thus ( not x in D * or x is set ) by Def11; :: thesis: verum