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