take 0. F_Real ; :: thesis: 0. F_Real is F_Rat -membered
thus 0. F_Real is F_Rat -membered ; :: thesis: verum