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