let x be number ; :: thesis: ( x is real implies x is complex )
assume x is real ; :: thesis: x is complex
then x in REAL by Def1;
hence x in COMPLEX by NUMBERS:def 2, XBOOLE_0:def 3; :: according to XCMPLX_0:def 2 :: thesis: verum