let S be Subset of F_Real; :: thesis: ( S = { x where x is Element of REAL : 0 <= x } implies S is positive_cone )
assume AS: S = { x where x is Element of REAL : 0 <= x } ; :: thesis: S is positive_cone
set R = F_Real ;
A: S + S c= S

proof

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

end;

B: S * S c= S

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in S * S or o in S )
assume o in S * S ; :: thesis: o in S
then consider a, b being Element of F_Real such that
A: ( o = a * b & a in S & b in S ) ;
consider x being Element of F_Real such that
B: ( x = a & 0 <= x ) by A, AS;
consider y being Element of F_Real such that
C: ( y = b & 0 <= y ) by A, AS;
thus o in S by A, B, C, AS; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in S /\ (- S) implies o in {(0. F_Real)} )
assume K0: o in S /\ (- S) ; :: thesis: o in {(0. F_Real)}
then K1: ( o in S & o in - S ) by XBOOLE_0:def 4;
reconsider x = o as Element of F_Real by K0;
consider y1 being Element of F_Real such that
K2: ( y1 = o & 0 <= y1 ) by AS, K1;
consider y2 being Element of F_Real such that
K3: ( - y2 = o & y2 in S ) by K1;
consider y being Element of F_Real such that
K4: ( y2 = y & 0 <= y ) by AS, K3;
y1 = 0. F_Real by K4, K2, K3;
hence o in {(0. F_Real)} by K2, TARSKI:def 1; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in {(0. F_Real)} implies o in S /\ (- S) )
assume K0: o in {(0. F_Real)} ; :: thesis: o in S /\ (- S)
then K1: o = 0. F_Real by TARSKI:def 1;
reconsider x = o as Element of F_Real by K0;
K2: ( 0 <= x & 0 <= - x ) by K1;
K3: x in S by AS, K0;
x in { (- s) where s is Element of F_Real : s in S } by K2, K3, K1;
hence o in S /\ (- S) by K3, XBOOLE_0:def 4; :: thesis: verum

end;

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

let o be object ; :: thesis: ( o in the carrier of F_Real implies b₁ in S \/ (- S) )
assume o in the carrier of F_Real ; :: thesis: b₁ in S \/ (- S)
then reconsider x = o as Element of F_Real ;

per cases ( 0 <= x or 0 <= - x ) ;

suppose 0 <= x ; :: thesis: b₁ in S \/ (- S)

then x in S by AS;
hence o in S \/ (- S) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose 0 <= - x ; :: thesis: b₁ in S \/ (- S)

then - x in S by AS;
then - (- x) in - S ;
hence o in S \/ (- S) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

for o being object st o in S \/ (- S) holds
o in the carrier of F_Real ;
hence S is positive_cone by A, B, C, K, F, TARSKI:2; :: thesis: verum