theorem Th47: :: RING_3:48

F_Real is Subfield of F_Complex by Lm2, EC_PF_1:2;