let n be Element of REAL ; :: thesis: n is complex
n in REAL ;
hence n is complex by Def2, Lm4; :: thesis: verum