theorem Th4: :: LIOUVIL2:3

F_Real is Subring of F_Complex by RING_3:43, RING_3:48;