set C = { x where x is Element of R : x is irreducible } ;
now :: thesis: for y being object st y in { x where x is Element of R : x is irreducible } holds
y in the carrier of R
let y be object ; :: thesis: ( y in { x where x is Element of R : x is irreducible } implies y in the carrier of R )
assume y in { x where x is Element of R : x is irreducible } ; :: thesis: y in the carrier of R
then ex a being Element of R st
( a = y & a is irreducible ) ;
hence y in the carrier of R ; :: thesis: verum
end;
then { x where x is Element of R : x is irreducible } c= the carrier of R ;
hence { x where x is Element of R : x is irreducible } is Subset of R ; :: thesis: verum