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 b1 in P \/ (- P) )
assume o in the carrier of INT.Ring ; :: thesis: b1 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: b1 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: b1 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