take F_Real ; :: thesis: F_Real is infinite
thus F_Real is infinite ; :: thesis: verum