{ x where x is Element of L : x is_a_root_of p } c= the carrier of L

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of L : x is_a_root_of p } or y in the carrier of L )
assume y in { x where x is Element of L : x is_a_root_of p } ; :: thesis: y in the carrier of L
then ex x being Element of L st
( x = y & x is_a_root_of p ) ;
hence y in the carrier of L ; :: thesis: verum

end;

then reconsider X = { x where x is Element of L : x is_a_root_of p } as Subset of L ;
take X ; :: thesis: for x being Element of L holds
( x in X iff x is_a_root_of p )
let x be Element of L; :: thesis: ( x in X iff x is_a_root_of p )
thus ( x in X implies x is_a_root_of p ) :: thesis: ( x is_a_root_of p implies x in X )

proof

assume x in X ; :: thesis: x is_a_root_of p
then ex y being Element of L st
( x = y & y is_a_root_of p ) ;
hence x is_a_root_of p ; :: thesis: verum

end;

assume x is_a_root_of p ; :: thesis: x in X
hence x in X ; :: thesis: verum