theorem XX: :: RING_5:1

for n being even Nat
for x being Element of F_Real holds x |^ n >= 0. F_Real