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

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

then ex z9 being Complex st
( z = z9 & Rea z = Re z9 ) by Def12;
hence Rea z is real ; :: thesis: verum

end;

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

then ex f being Function of 4,REAL st
( z = f & Rea z = f . 0 ) by Def12;
hence Rea z is real ; :: thesis: verum

end;

end;