take F_Real ; :: thesis: F_Real is 0 -characteristic
thus F_Real is 0 -characteristic ; :: thesis: verum