set M = { x where x is Element of L : x is_a_common_root_of p,q } ;

now :: thesis: for u being object st u in { x where x is Element of L : x is_a_common_root_of p,q } holds
u in the carrier of L

let u be object ; :: thesis: ( u in { x where x is Element of L : x is_a_common_root_of p,q } implies u in the carrier of L )
assume u in { x where x is Element of L : x is_a_common_root_of p,q } ; :: thesis: u in the carrier of L
then ex x being Element of L st
( u = x & x is_a_common_root_of p,q ) ;
hence u in the carrier of L ; :: thesis: verum

end;

hence { x where x is Element of L : x is_a_common_root_of p,q } is Subset of L by TARSKI:def 3; :: thesis: verum