set R = F_Rat ;
let P be Preordering of F_Rat; :: thesis: P is spanning
A: ( 0. F_Rat = 0 & 1. F_Rat = 1 ) by GAUSSINT:def 14;
E: ( P + P c= P & P * P c= P ) by REALALG1:def 14;
H: (- P) * P c= - P by v2;

now :: thesis: for o being object st o in the carrier of F_Rat holds
o in P \/ (- P)

let o be object ; :: thesis: ( o in the carrier of F_Rat implies b₁ in P \/ (- P) )
assume o in the carrier of F_Rat ; :: thesis: b₁ in P \/ (- P)
then reconsider p = o as Rational ;
set m = numerator p;
set n = denominator p;
reconsider a = denominator p, b = numerator p as Element of F_Rat by INT_1:def 2, NUMBERS:14, GAUSSINT:def 14;
G: a <> 0. F_Rat by GAUSSINT:def 14;
F: p = (numerator p) * ((denominator p) ") by RAT_1:15
.= b * (a ") by G, GAUSSINT:15 ;

per cases ( numerator p = 0 or 0 < numerator p or numerator p < 0 ) ;

suppose numerator p = 0 ; :: thesis: b₁ in P \/ (- P)

then p = 0 by RAT_1:14;
then o in P by A, REALALG1:25;
hence o in P \/ (- P) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose 0 < numerator p ; :: thesis: b₁ in P \/ (- P)

then reconsider m1 = numerator p as Element of NAT by INT_1:3;
C: ( (denominator p) '*' (1. F_Rat) = denominator p & m1 '*' (1. F_Rat) = m1 ) by Lm9;
then D: ( a in P & b in P ) by spa;
not a is zero by GAUSSINT:def 14;
then a " in P by C, spa, REALALG1:27;
then b * (a ") in P * P by D;
hence o in P \/ (- P) by E, F, XBOOLE_0:def 3; :: thesis: verum

end;

suppose numerator p < 0 ; :: thesis: b₁ in P \/ (- P)

then reconsider m1 = - (numerator p) as Element of NAT by INT_1:3;
E: ( (denominator p) '*' (1. F_Rat) = denominator p & m1 '*' (1. F_Rat) = m1 ) by Lm9;
then ( a in P & - b in P ) by spa;
then D: ( a in P & - (- b) in - P ) ;
not a is zero by GAUSSINT:def 14;
then a " in P by E, spa, REALALG1:27;
then b * (a ") in (- P) * P by D;
hence o in P \/ (- P) by F, H, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then the carrier of F_Rat = P \/ (- P) by TARSKI:def 3;
hence P is spanning ; :: thesis: verum