let S be Subset of R; :: thesis: ( S is add-closed & S is mult-closed & S is negative-disjoint & S is spanning implies S is positive_cone )
assume AS: ( S is add-closed & S is mult-closed & S is negative-disjoint & S is spanning ) ; :: thesis: S is positive_cone
B: S + S c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S + S or x in S )
assume x in S + S ; :: thesis: x in S
then x in { (a + b) where a, b is Element of R : ( a in S & b in S ) } by IDEAL_1:def 19;
then consider a, b being Element of R such that
A1: ( x = a + b & a in S & b in S ) ;
thus x in S by AS, A1; :: thesis: verum

end;

S * S c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S * S or x in S )
assume x in S * S ; :: thesis: x in S
then consider a, b being Element of R such that
A1: ( x = a * b & a in S & b in S ) ;
thus x in S by A1, AS; :: thesis: verum

end;

hence S is positive_cone by AS, B; :: thesis: verum