theorem lemeval2: :: FIELD_9:26

for F being Field
for a being non zero Element of F
for b, c being Element of F st Roots <%c,b,a%> <> {} holds
(b ^2) - ((4 '*' a) * c) is square