set R = INT.Ring ;
let P be Preordering of INT.Ring; :: thesis: P is spanning

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

let o be object ; :: thesis: ( o in the carrier of INT.Ring implies b₁ in P \/ (- P) )
assume o in the carrier of INT.Ring ; :: thesis: b₁ in P \/ (- P)
then consider n being Nat such that
B: ( o = n or o = - n ) by INT_1:2;
A: n '*' (1. INT.Ring) = n by Lm8;
C: - (n '*' (1. INT.Ring)) = - n by Lm8;

per cases ( o = n or o = - n ) by B;

suppose o = n ; :: thesis: b₁ in P \/ (- P)

then o in P by A, spa;
hence o in P \/ (- P) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose K: o = - n ; :: thesis: b₁ in P \/ (- P)

n in P by A, spa;
then - n in - P by C;
hence o in P \/ (- P) by K, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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