let n be Element of REAL ; :: thesis: n is complex
n in REAL ;
hence n is complex by Lm6; :: thesis: verum