Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.
According to this sample solution the property does not hold, but my solution shows it holds.
So what could be the mistake in my solution?
You continued in s5 with the diamond operator, but that one has been removed by the rule before. Instead, it should have been a box operator there. And then, the property must also be shown in the other successor states of s5, but it does not hold in state s0: