let R1 be domRing; :: thesis: for S being Subset of R1 st S is positive_cone holds
( {(S ^+),{(0. R1)},(S ^-)} is a_partition of the carrier of R1 & S ^+ is add-closed & S ^+ is mult-closed )
let S be Subset of R1; :: thesis: ( S is positive_cone implies ( {(S ^+),{(0. R1)},(S ^-)} is a_partition of the carrier of R1 & S ^+ is add-closed & S ^+ is mult-closed ) )
assume AS: S is positive_cone ; :: thesis: ( {(S ^+),{(0. R1)},(S ^-)} is a_partition of the carrier of R1 & S ^+ is add-closed & S ^+ is mult-closed )
then reconsider R = R1 as ordered domRing by REALALG1:def 17;
reconsider P = S as Ordering of R by AS;
set M = {(S ^+),{(0. R1)},(S ^-)};
H: ( P \/ (- P) = the carrier of R & P /\ (- P) = {(0. R)} ) by REALALG1:def 15;

now :: thesis: for o being object st o in the carrier of R holds
o in union {(S ^+),{(0. R1)},(S ^-)}

let o be object ; :: thesis: ( o in the carrier of R implies b₁ in union {(S ^+),{(0. R1)},(S ^-)} )
assume o in the carrier of R ; :: thesis: b₁ in union {(S ^+),{(0. R1)},(S ^-)}

per cases then ( o = 0. R or ( o <> 0. R & o in P ) or ( o <> 0. R & o in - P ) ) by H, XBOOLE_0:def 3;

suppose o = 0. R ; :: thesis: b₁ in union {(S ^+),{(0. R1)},(S ^-)}

then ( o in {(0. R)} & {(0. R)} in {(S ^+),{(0. R1)},(S ^-)} ) by TARSKI:def 1, ENUMSET1:def 1;
hence o in union {(S ^+),{(0. R1)},(S ^-)} by TARSKI:def 4; :: thesis: verum

end;

suppose ( o <> 0. R & o in P ) ; :: thesis: b₁ in union {(S ^+),{(0. R1)},(S ^-)}

then ( not o in {(0. R)} & o in P ) by TARSKI:def 1;
then ( o in P ^+ & P ^+ in {(S ^+),{(0. R1)},(S ^-)} ) by XBOOLE_0:def 5, ENUMSET1:def 1;
hence o in union {(S ^+),{(0. R1)},(S ^-)} by TARSKI:def 4; :: thesis: verum

end;

suppose ( o <> 0. R & o in - P ) ; :: thesis: b₁ in union {(S ^+),{(0. R1)},(S ^-)}

then ( not o in {(0. R)} & o in - P ) by TARSKI:def 1;
then ( o in P ^- & P ^- in {(S ^+),{(0. R1)},(S ^-)} ) by XBOOLE_0:def 5, ENUMSET1:def 1;
hence o in union {(S ^+),{(0. R1)},(S ^-)} by TARSKI:def 4; :: thesis: verum

end;

end;

end;

then the carrier of R c= union {(S ^+),{(0. R1)},(S ^-)} ;
then A: union {(S ^+),{(0. R1)},(S ^-)} = the carrier of R ;

now :: thesis: for A being Subset of the carrier of R st A in {(S ^+),{(0. R1)},(S ^-)} holds
( A <> {} & ( for B being Subset of the carrier of R holds
( not B in {(S ^+),{(0. R1)},(S ^-)} or A = B or A misses B ) ) )

let A be Subset of the carrier of R; :: thesis: ( A in {(S ^+),{(0. R1)},(S ^-)} implies ( A <> {} & ( for B being Subset of the carrier of R holds
( not B in {(S ^+),{(0. R1)},(S ^-)} or A = B or A misses B ) ) ) )
assume B: A in {(S ^+),{(0. R1)},(S ^-)} ; :: thesis: ( A <> {} & ( for B being Subset of the carrier of R holds
( not B in {(S ^+),{(0. R1)},(S ^-)} or A = B or A misses B ) ) )
thus A <> {} :: thesis: for B being Subset of the carrier of R holds
( not B in {(S ^+),{(0. R1)},(S ^-)} or A = B or A misses B )

proof

per cases ( A = {(0. R)} or A = P ^+ or A = P ^- ) by B, ENUMSET1:def 1;

suppose A = {(0. R)} ; :: thesis: A <> {}

hence A <> {} ; :: thesis: verum

end;

suppose A = P ^+ ; :: thesis: A <> {}

hence A <> {} ; :: thesis: verum

end;

suppose A = P ^- ; :: thesis: A <> {}

hence A <> {} ; :: thesis: verum

end;

end;

end;

thus for B being Subset of the carrier of R holds
( not B in {(S ^+),{(0. R1)},(S ^-)} or A = B or A misses B ) :: thesis: verum

proof

let B be Subset of the carrier of R; :: thesis: ( not B in {(S ^+),{(0. R1)},(S ^-)} or A = B or A misses B )
assume C: B in {(S ^+),{(0. R1)},(S ^-)} ; :: thesis: ( A = B or A misses B )
assume D: A <> B ; :: thesis: A misses B
set x = the Element of A /\ B;

per cases ( A = {(0. R)} or A = P ^+ or A = P ^- ) by B, ENUMSET1:def 1;

suppose E: A = {(0. R)} ; :: thesis: A misses B

per cases then ( B = P ^+ or B = P ^- ) by C, D, ENUMSET1:def 1;

suppose F: B = P ^+ ; :: thesis: A misses B

now :: thesis: not A /\ B <> {}

assume A /\ B <> {} ; :: thesis: contradiction
then ( the Element of A /\ B in {(0. R)} & the Element of A /\ B in B ) by E, XBOOLE_0:def 4;
hence contradiction by F, XBOOLE_0:def 5; :: thesis: verum

end;

hence A misses B ; :: thesis: verum

end;

suppose F: B = P ^- ; :: thesis: A misses B

now :: thesis: not A /\ B <> {}

assume A /\ B <> {} ; :: thesis: contradiction
then ( the Element of A /\ B in {(0. R)} & the Element of A /\ B in B ) by E, XBOOLE_0:def 4;
hence contradiction by F, XBOOLE_0:def 5; :: thesis: verum

end;

hence A misses B ; :: thesis: verum

end;

end;

end;

suppose E: A = P ^+ ; :: thesis: A misses B

per cases then ( B = {(0. R)} or B = P ^- ) by C, D, ENUMSET1:def 1;

suppose F: B = {(0. R)} ; :: thesis: A misses B

now :: thesis: not A /\ B <> {}

assume A /\ B <> {} ; :: thesis: contradiction
then ( the Element of A /\ B in {(0. R)} & the Element of A /\ B in A ) by F, XBOOLE_0:def 4;
hence contradiction by E, XBOOLE_0:def 5; :: thesis: verum

end;

hence A misses B ; :: thesis: verum

end;

suppose B = P ^- ; :: thesis: A misses B

hence A misses B by E; :: thesis: verum

end;

end;

end;

suppose E: A = P ^- ; :: thesis: A misses B

per cases then ( B = {(0. R)} or B = P ^+ ) by C, D, ENUMSET1:def 1;

suppose F: B = {(0. R)} ; :: thesis: A misses B

now :: thesis: not A /\ B <> {}

assume A /\ B <> {} ; :: thesis: contradiction
then ( the Element of A /\ B in {(0. R)} & the Element of A /\ B in A ) by F, XBOOLE_0:def 4;
hence contradiction by E, XBOOLE_0:def 5; :: thesis: verum

end;

hence A misses B ; :: thesis: verum

end;

suppose B = P ^+ ; :: thesis: A misses B

hence A misses B by E; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence {(S ^+),{(0. R1)},(S ^-)} is a_partition of the carrier of R1 by A, EQREL_1:def 4; :: thesis: ( S ^+ is add-closed & S ^+ is mult-closed )
for a, b being Element of R st a in P ^+ & b in P ^+ holds
a + b in P ^+ by IDEAL_1:def 1;
hence ( S ^+ is add-closed & S ^+ is mult-closed ) ; :: thesis: verum