let R be non degenerated Ring; :: thesis: for S being Subset of R st 0. R in S & ( (S ^+) /\ (S ^-) = {} or S ^+ <> S ^- ) & {(S ^+),{(0. R)},(S ^-)} is a_partition of the carrier of R & S ^+ is add-closed & S ^+ is mult-closed holds
S is positive_cone
let S be Subset of R; :: thesis: ( 0. R in S & ( (S ^+) /\ (S ^-) = {} or S ^+ <> S ^- ) & {(S ^+),{(0. R)},(S ^-)} is a_partition of the carrier of R & S ^+ is add-closed & S ^+ is mult-closed implies S is positive_cone )
assume H: ( 0. R in S & ( (S ^+) /\ (S ^-) = {} or S ^+ <> S ^- ) ) ; :: thesis: ( not {(S ^+),{(0. R)},(S ^-)} is a_partition of the carrier of R or not S ^+ is add-closed or not S ^+ is mult-closed or S 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 is positive_cone
A1: S + S c= S

proof

now :: thesis: for o being object st o in S + S holds
o in S

let o be object ; :: thesis: ( o in S + S implies b₁ in S )
assume o in S + S ; :: thesis: b₁ in S
then consider a, b being Element of R such that
B: ( o = a + b & a in S & b in S ) ;

per cases ( a = 0. R or b = 0. R or ( a <> 0. R & b <> 0. R ) ) ;

suppose ( a = 0. R or b = 0. R ) ; :: thesis: b₁ in S

hence o in S by B; :: thesis: verum

end;

suppose ( a <> 0. R & b <> 0. R ) ; :: thesis: b₁ in S

then ( not a in {(0. R)} & not b in {(0. R)} ) by TARSKI:def 1;
then ( a in S ^+ & b in S ^+ ) by B, XBOOLE_0:def 5;
then o in S ^+ by B, AS;
hence o in S by XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence S + S c= S ; :: thesis: verum

end;

A2: S * S c= S

proof

now :: thesis: for o being object st o in S * S holds
o in S

let o be object ; :: thesis: ( o in S * S implies b₁ in S )
assume o in S * S ; :: thesis: b₁ in S
then consider a, b being Element of R such that
B: ( o = a * b & a in S & b in S ) ;

per cases ( a = 0. R or b = 0. R or ( a <> 0. R & b <> 0. R ) ) ;

suppose ( a = 0. R or b = 0. R ) ; :: thesis: b₁ in S

hence o in S by B; :: thesis: verum

end;

suppose ( a <> 0. R & b <> 0. R ) ; :: thesis: b₁ in S

then ( not a in {(0. R)} & not b in {(0. R)} ) by TARSKI:def 1;
then ( a in S ^+ & b in S ^+ ) by B, XBOOLE_0:def 5;
then o in S ^+ by B, AS;
hence o in S by XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence S * S c= S ; :: thesis: verum

end;

A3: S /\ (- S) = {(0. R)}

proof

B: now :: thesis: for o being object st o in {(0. R)} holds
o in S /\ (- S)

let o be object ; :: thesis: ( o in {(0. R)} implies o in S /\ (- S) )
assume o in {(0. R)} ; :: thesis: o in S /\ (- S)
then ( o = 0. R & 0. R = - (0. R) ) by TARSKI:def 1;
then ( o in S & o in - S ) by H;
hence o in S /\ (- S) ; :: thesis: verum

end;

now :: thesis: for o being object st o in S /\ (- S) holds
o in {(0. R)}

let o be object ; :: thesis: ( o in S /\ (- S) implies o in {(0. R)} )
assume o in S /\ (- S) ; :: thesis: o in {(0. R)}
then C: ( o in S & o in - S ) by XBOOLE_0:def 4;

now :: thesis: not o <> 0. R

assume o <> 0. R ; :: thesis: contradiction
then not o in {(0. R)} by TARSKI:def 1;
then ( o in S ^+ & o in S ^- ) by C, XBOOLE_0:def 5;
then F: o in (S ^+) /\ (S ^-) ;
then D: not S ^+ misses S ^- ;

per cases ( (S ^+) /\ (S ^-) = {} or S ^+ <> S ^- ) by H;

suppose (S ^+) /\ (S ^-) = {} ; :: thesis: contradiction

hence contradiction by F; :: thesis: verum

end;

suppose E: S ^+ <> S ^- ; :: thesis: contradiction

( S ^+ in {(S ^+),{(0. R)},(S ^-)} & S ^- in {(S ^+),{(0. R)},(S ^-)} ) by ENUMSET1:def 1;
hence contradiction by AS, D, E, EQREL_1:def 4; :: thesis: verum

end;

end;

end;

hence o in {(0. R)} by TARSKI:def 1; :: thesis: verum

end;

hence S /\ (- S) = {(0. R)} by B, TARSKI:2; :: thesis: verum

end;

S \/ (- S) = the carrier of R

proof

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

let o be object ; :: thesis: ( o in the carrier of R implies b₁ in S \/ (- S) )
assume B: o in the carrier of R ; :: thesis: b₁ in S \/ (- S)
union {(S ^+),{(0. R)},(S ^-)} = the carrier of R by AS, EQREL_1:def 4;
then consider u being set such that
C: ( o in u & u in {(S ^+),{(0. R)},(S ^-)} ) by B, TARSKI:def 4;

per cases ( u = S ^+ or u = {(0. R)} or u = S ^- ) by C, ENUMSET1:def 1;

suppose u = S ^+ ; :: thesis: b₁ in S \/ (- S)

then o in S by C, XBOOLE_0:def 5;
hence o in S \/ (- S) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose u = {(0. R)} ; :: thesis: b₁ in S \/ (- S)

then o in S by C, H, TARSKI:def 1;
hence o in S \/ (- S) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose u = S ^- ; :: thesis: b₁ in S \/ (- S)

then o in - S by C, XBOOLE_0:def 5;
hence o in S \/ (- S) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

then the carrier of R c= S \/ (- S) ;
hence S \/ (- S) = the carrier of R ; :: thesis: verum

end;

hence S is positive_cone by A1, A2, A3; :: thesis: verum