let R be preordered domRing; :: thesis: for P being Preordering of R
for a being b₁ -ordered Element of R holds (abs (P,a)) ^2 = a ^2
let P be Preordering of R; :: thesis: for a being P -ordered Element of R holds (abs (P,a)) ^2 = a ^2
let a be P -ordered Element of R; :: thesis: (abs (P,a)) ^2 = a ^2
a in P \/ (- P) by defppp;

per cases then ( a in P or a in - P ) by XBOOLE_0:def 3;

suppose a in P ; :: thesis: (abs (P,a)) ^2 = a ^2

then 0. R <= P,a ;
hence (abs (P,a)) ^2 = a ^2 by av2; :: thesis: verum

end;

suppose a in - P ; :: thesis: (abs (P,a)) ^2 = a ^2

then - a in - (- P) ;
then a <= P, 0. R ;
hence (abs (P,a)) ^2 = (- a) ^2 by av3
.= a ^2 by VECTSP_1:10 ;
:: thesis: verum

end;

end;