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