let R be preordered Ring; :: thesis: for P being Preordering of R
for a being Element of R holds a ^2 in P
let P be Preordering of R; :: thesis: for a being Element of R holds a ^2 in P
let a be Element of R; :: thesis: a ^2 in P
a ^2 is square ;
then A: a ^2 in SQ R ;
SQ R c= P by defppc;
hence a ^2 in P by A; :: thesis: verum