let S be Subset of R; :: thesis: ( S is positive_cone implies ( S is add-closed & S is mult-closed & S is negative-disjoint & S is spanning ) )
assume AS: S is positive_cone ; :: thesis: ( S is add-closed & S is mult-closed & S is negative-disjoint & S is spanning )
thus S is add-closed :: thesis: ( S is mult-closed & S is negative-disjoint & S is spanning )
proof
let x, y be Element of R; :: according to IDEAL_1:def 1 :: thesis: ( not x in S or not y in S or x + y in S )
assume ( x in S & y in S ) ; :: thesis: x + y in S
then x + y in { (a + b) where a, b is Element of R : ( a in S & b in S ) } ;
then x + y in S + S by IDEAL_1:def 19;
hence x + y in S by AS; :: thesis: verum
end;
thus S is mult-closed :: thesis: ( S is negative-disjoint & S is spanning )
proof
let x, y be Element of R; :: according to REALALG1:def 5 :: thesis: ( x in S & y in S implies x * y in S )
assume ( x in S & y in S ) ; :: thesis: x * y in S
then x * y in S * S ;
hence x * y in S by AS; :: thesis: verum
end;
thus ( S is negative-disjoint & S is spanning ) by AS; :: thesis: verum