z *' in COMPLEX ;
hence z *' is Element of by Def1; :: thesis: verum