let R be preordered Ring; :: thesis: for P being Preordering of R holds
( 0. R in P & 1. R in P )
let O be Preordering of R; :: thesis: ( 0. R in O & 1. R in O )
( 0. R in QS R & 1. R in QS R ) ;
hence ( 0. R in O & 1. R in O ) by ord2, TARSKI:def 3; :: thesis: verum