:: deftheorem defines the_proper_Tree_of CGAMES_1:def 13 :
for g being ConwayGame holds the_proper_Tree_of g = (the_Tree_of g) \ {g};