let P be Subset of R; :: thesis: ( P is positive_cone implies P is prepositive_cone )
assume AS: P is positive_cone ; :: thesis: P is prepositive_cone
SQ R c= P
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in SQ R or o in P )
assume o in SQ R ; :: thesis: o in P
then consider a being Element of R such that
A: ( o = a & a is square ) ;
consider b being Element of R such that
B: a = b ^2 by A;
per cases ( b in P or b in - P ) by AS, XBOOLE_0:def 3;
suppose b in P ; :: thesis: o in P
then b * b in { (x * y) where x, y is Element of R : ( x in P & y in P ) } ;
hence o in P by A, B, AS; :: thesis: verum
end;
suppose b in - P ; :: thesis: o in P
then consider b1 being Element of R such that
D: ( - b1 = b & b1 in P ) ;
E: b1 * b1 in { (x * y) where x, y is Element of R : ( x in P & y in P ) } by D;
b1 * b1 = b * b by D, VECTSP_1:10;
hence o in P by E, B, A, AS; :: thesis: verum
end;
end;
end;
hence P is prepositive_cone by AS; :: thesis: verum