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

suppose z in REAL ; :: thesis: Re z is real

hence Re z is real by Def2; :: thesis: verum

end;

suppose not z in REAL ; :: thesis: Re z is real

then consider f being Function of 2,REAL such that
z = f and
A1: Re z = f . 0 by Def2;
0 in 2 by CARD_1:88, TARSKI:def 2;
then f . 0 in REAL by FUNCT_2:7;
hence Re z is real by A1; :: thesis: verum

end;

end;