let R be non degenerated Ring; :: thesis: for S being Subset of R st {S,{(0. R)},(- S)} is a_partition of the carrier of R & S is add-closed & S is mult-closed holds
S \/ {(0. R)} is positive_cone
let S be Subset of R; :: thesis: ( {S,{(0. R)},(- S)} is a_partition of the carrier of R & S is add-closed & S is mult-closed implies S \/ {(0. R)} is positive_cone )
assume AS: ( {S,{(0. R)},(- S)} is a_partition of the carrier of R & S is add-closed & S is mult-closed ) ; :: thesis: S \/ {(0. R)} is positive_cone
set T = S \/ {(0. R)};

J: now :: thesis: not S = - S

assume S = - S ; :: thesis: contradiction
then J1: {S,{(0. R)}} = {S,(- S),{(0. R)}} by ENUMSET1:30
.= {S,{(0. R)},(- S)} by ENUMSET1:57 ;
J2: ( S in {S,{(0. R)}} & {(0. R)} in {S,{(0. R)}} ) by TARSKI:def 2;
union {S,{(0. R)}} = the carrier of R by AS, J1, EQREL_1:def 4;
then J3: S \/ {(0. R)} = the carrier of R by ZFMISC_1:75;
( not 1. R in {(0. R)} & not - (1. R) in {(0. R)} ) by TARSKI:def 1;
then ( 1. R in S & - (1. R) in S ) by J3, XBOOLE_0:def 3;
then (1. R) + (- (1. R)) in S by AS;
then ( 0. R in S & 0. R in {(0. R)} ) by RLVECT_1:5, TARSKI:def 1;
then 0. R in S /\ {(0. R)} ;
then not S misses {(0. R)} ;
then S = {(0. R)} by AS, J1, J2, EQREL_1:def 4;
then {S,{(0. R)}} = {{(0. R)}} by ENUMSET1:29;
then union {{(0. R)}} = the carrier of R by AS, J1, EQREL_1:def 4;
hence contradiction by ZFMISC_1:25; :: thesis: verum

end;

I1: now :: thesis: not S = {(0. R)}

assume AS1: S = {(0. R)} ; :: thesis: contradiction
then - S = {(0. R)} by lempart0;
then {S,{(0. R)},(- S)} = {{(0. R)}} by AS1, ENUMSET1:36;
then union {{(0. R)}} = the carrier of R by AS, EQREL_1:def 4;
hence contradiction by ZFMISC_1:25; :: thesis: verum

end;

( S in {S,{(0. R)},(- S)} & {(0. R)} in {S,{(0. R)},(- S)} ) by ENUMSET1:def 1;
then S misses {(0. R)} by I1, AS, EQREL_1:def 4;
then K0: S \ {(0. R)} = S by XBOOLE_1:83;

I2: now :: thesis: not - S = {(0. R)}

assume AS2: - S = {(0. R)} ; :: thesis: contradiction
then - (- S) = - {(0. R)} ;
then S = {(0. R)} by lempart0;
then {S,{(0. R)},(- S)} = {{(0. R)}} by AS2, ENUMSET1:36;
then union {{(0. R)}} = the carrier of R by AS, EQREL_1:def 4;
hence contradiction by ZFMISC_1:25; :: thesis: verum

end;

( - S in {S,{(0. R)},(- S)} & {(0. R)} in {S,{(0. R)},(- S)} ) by ENUMSET1:def 1;
then - S misses {(0. R)} by I2, AS, EQREL_1:def 4;
then K1: (- S) \ {(0. R)} = - S by XBOOLE_1:83;
H1: (S \/ {(0. R)}) ^+ = S by K0, XBOOLE_1:40;
H2: (S \/ {(0. R)}) ^- = ((- S) \/ (- {(0. R)})) \ {(0. R)} by REALALG1:16
.= ((- S) \/ {(0. R)}) \ {(0. R)} by lempart0
.= - S by K1, XBOOLE_1:40 ;
0. R in {(0. R)} by TARSKI:def 1;
then A: 0. R in S \/ {(0. R)} by XBOOLE_0:def 3;
((S \/ {(0. R)}) ^+) /\ ((S \/ {(0. R)}) ^-) = {}

proof

( S in {S,{(0. R)},(- S)} & - S in {S,{(0. R)},(- S)} ) by ENUMSET1:def 1;
then S misses - S by J, AS, EQREL_1:def 4;
hence ((S \/ {(0. R)}) ^+) /\ ((S \/ {(0. R)}) ^-) = {} by H2, K0, XBOOLE_1:40; :: thesis: verum

end;

hence S \/ {(0. R)} is positive_cone by H1, H2, AS, A, bla; :: thesis: verum