reconsider mym = 1 as Element of REAL by Ko1;
consider myp being Element of REAL such that
A10: myp = - mym ;
A0: (Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) = RAT by A10, Th3;
A1: Union (GoCross_Union mym) is Event of Borel_Sets by PROB_1:17;
Union (GoCross_Union myp) is Event of Borel_Sets by PROB_1:17;
hence RAT is Event of Borel_Sets by A1, PROB_1:21, A0; :: thesis: verum