reconsider Rz1 = Re z1, Iz1 = Im z1 as Rational ;
reconsider Rz2 = Re z2, Iz2 = Im z2 as Rational ;
( Re (z1 - z2) = Rz1 - Rz2 & Im (z1 - z2) = Iz1 - Iz2 ) by COMPLEX1:19;
hence z1 - z2 is g_rational by RAT_1:def 2; :: thesis: verum