let X1, X2 be Subset of L; :: thesis: ( ( for x being Element of L holds
( x in X1 iff x is_a_root_of p ) ) & ( for x being Element of L holds
( x in X2 iff x is_a_root_of p ) ) implies X1 = X2 )
assume that
A1: for x being Element of L holds
( x in X1 iff x is_a_root_of p ) and
A2: for x being Element of L holds
( x in X2 iff x is_a_root_of p ) ; :: thesis: X1 = X2
thus X1 c= X2 by A1, A2; :: according to XBOOLE_0:def 10 :: thesis: X2 c= X1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X2 or x in X1 )
assume A3: x in X2 ; :: thesis: x in X1
then reconsider y = x as Element of L ;
y is_a_root_of p by A2, A3;
hence x in X1 by A1; :: thesis: verum