set M = /\ (P,R);
now :: thesis: for x, y being Element of R st x in /\ (P,R) & y in /\ (P,R) holds
x + y in /\ (P,R)
let x, y be Element of R; :: thesis: ( x in /\ (P,R) & y in /\ (P,R) implies x + y in /\ (P,R) )
assume AS: ( x in /\ (P,R) & y in /\ (P,R) ) ; :: thesis: x + y in /\ (P,R)
then consider a being Element of R such that
A: ( x = a & ( for O being Ordering of R st P c= O holds
a in O ) ) ;
consider b being Element of R such that
B: ( y = b & ( for O being Ordering of R st P c= O holds
b in O ) ) by AS;
now :: thesis: for O being Ordering of R st P c= O holds
a + b in O
let O be Ordering of R; :: thesis: ( P c= O implies a + b in O )
assume P c= O ; :: thesis: a + b in O
then ( a in O & b in O ) by A, B;
then C: a + b in O + O ;
O + O c= O by REALALG1:def 14;
hence a + b in O by C; :: thesis: verum
end;
hence x + y in /\ (P,R) by A, B; :: thesis: verum
end;
hence /\ (P,R) is add-closed ; :: thesis: ( /\ (P,R) is mult-closed & /\ (P,R) is with_squares )
now :: thesis: for x, y being Element of R st x in /\ (P,R) & y in /\ (P,R) holds
x * y in /\ (P,R)
let x, y be Element of R; :: thesis: ( x in /\ (P,R) & y in /\ (P,R) implies x * y in /\ (P,R) )
assume AS: ( x in /\ (P,R) & y in /\ (P,R) ) ; :: thesis: x * y in /\ (P,R)
then consider a being Element of R such that
A: ( x = a & ( for O being Ordering of R st P c= O holds
a in O ) ) ;
consider b being Element of R such that
B: ( y = b & ( for O being Ordering of R st P c= O holds
b in O ) ) by AS;
now :: thesis: for O being Ordering of R st P c= O holds
a * b in O
let O be Ordering of R; :: thesis: ( P c= O implies a * b in O )
assume P c= O ; :: thesis: a * b in O
then ( a in O & b in O ) by A, B;
then C: a * b in O * O ;
O * O c= O by REALALG1:def 14;
hence a * b in O by C; :: thesis: verum
end;
hence x * y in /\ (P,R) by A, B; :: thesis: verum
end;
hence /\ (P,R) is mult-closed ; :: thesis: /\ (P,R) is with_squares
X0: SQ R c= P by REALALG1:def 14;
now :: thesis: for o being object st o in SQ R holds
o in /\ (P,R)
let o be object ; :: thesis: ( o in SQ R implies o in /\ (P,R) )
assume X2: o in SQ R ; :: thesis: o in /\ (P,R)
then consider a being Element of R such that
X1: ( o = a & a is square ) ;
for O being Ordering of R st P c= O holds
a in O by X0, X1, X2;
hence o in /\ (P,R) by X1; :: thesis: verum
end;
then SQ R c= /\ (P,R) ;
hence /\ (P,R) is with_squares ; :: thesis: verum