now :: thesis: for o being object st o in { a where a is Element of S : a is_a_root_of p,S } holds
o in the carrier of S

let o be object ; :: thesis: ( o in { a where a is Element of S : a is_a_root_of p,S } implies o in the carrier of S )
assume o in { a where a is Element of S : a is_a_root_of p,S } ; :: thesis: o in the carrier of S
then consider a being Element of S such that
A1: ( o = a & a is_a_root_of p,S ) ;
thus o in the carrier of S by A1; :: thesis: verum

end;

hence { a where a is Element of S : a is_a_root_of p,S } is Subset of S by TARSKI:def 3; :: thesis: verum