theorem Th3: :: FINANCE2:17

for mym, myp being Element of REAL st mym = 1 & myp = - 1 holds
(Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) = RAT