let z be quaternion number ; :: thesis: ( z is real implies Rea z = z )
assume z is real ; :: thesis: Rea z = z
then z in REAL by XREAL_0:def 1;
hence Rea z = z by Lm19; :: thesis: verum