That seems to be a little mistake. Actually, there is no variable d and the formula does not ask for an implication inf->d. It seems that when producing a comprehensive solution, we have abbreviated the states satisfying EF c by d. Assuming this, we have

[|inf|] = {s0;...;s6}
[|!inf|] = {s7}
[|d|] = [|EF c|] = {s0;s1;s2;s3;s4;s5;s6} = [|inf|]
[|inf -> EF c|] = [|!inf | EF c|] = {s7} ∪ {s0;...;s6} = {s0;...;s7}