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

proof

let y be set ; :: 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 consider x being Element of L such that
A1: x = y and
x is_a_root_of p ;
thus y in the carrier of L by A1; :: 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 consider y being Element of L such that
A2: x = y and
A3: y is_a_root_of p ;
thus x is_a_root_of p by A2, A3; :: thesis: verum

end;

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