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

hence
{ a where a is Element of S : a is_a_root_of p,S } is Subset of S
by TARSKI:def 3; :: thesis: verumo 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;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