for z being Quaternion st z is real holds
( Rea z = z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by Lm18;