let L be Field; :: thesis: for a being Element of L
for b being non zero Element of L holds Roots <%a,b%> = {(- (a / b))}
let a be Element of L; :: thesis: for b being non zero Element of L holds Roots <%a,b%> = {(- (a / b))}
let b be non zero Element of L; :: thesis: Roots <%a,b%> = {(- (a / b))}
set p = <%a,b%>;
thus Roots <%a,b%> c= {(- (a / b))} :: according to XBOOLE_0:def 10 :: thesis: {(- (a / b))} c= Roots <%a,b%>

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Roots <%a,b%> or x in {(- (a / b))} )
assume A1: x in Roots <%a,b%> ; :: thesis: x in {(- (a / b))}
then reconsider x = x as Element of L ;
x is_a_root_of <%a,b%> by A1, POLYNOM5:def 10;
then x = - (a / b) by Th9;
hence x in {(- (a / b))} by TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(- (a / b))} or x in Roots <%a,b%> )
assume x in {(- (a / b))} ; :: thesis: x in Roots <%a,b%>
then A2: x = - (a / b) by TARSKI:def 1;
- (a / b) is_a_root_of <%a,b%> by Th9;
hence x in Roots <%a,b%> by A2, POLYNOM5:def 10; :: thesis: verum