for g being ConwayGame
for s being set st g in s & ( for g1 being ConwayGame st g1 in s holds
the_Options_of g1 c= s ) holds
the_Tree_of g c= s