now :: thesis: for x being object st x in { x where x is Element of R : for O being Ordering of R st P c= O holds
x in O } holds
x in the carrier of R

let x be object ; :: thesis: ( x in { x where x is Element of R : for O being Ordering of R st P c= O holds
x in O } implies x in the carrier of R )
assume x in { x where x is Element of R : for O being Ordering of R st P c= O holds
x in O } ; :: thesis: x in the carrier of R
then ex x1 being Element of R st
( x1 = x & ( for O being Ordering of R st P c= O holds
x1 in O ) ) ;
hence x in the carrier of R ; :: thesis: verum

end;

hence { x where x is Element of R : for O being Ordering of R st P c= O holds
x in O } is Subset of R by TARSKI:def 3; :: thesis: verum