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

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

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

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

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 ;