per cases ( z in COMPLEX or not z in COMPLEX ) ;

suppose z in COMPLEX ; :: thesis: Rea z is real

then consider z' being complex number such that
z = z' and
A1: Rea z = Re z' by Def13;
thus Rea z is real by A1; :: thesis: verum

end;

suppose not z in COMPLEX ; :: thesis: Rea z is real

then consider f being Function of 4,REAL such that
z = f and
A2: Rea z = f . 0 by Def13;
thus Rea z is real by A2; :: thesis: verum

end;

end;