consider x being object such that
A1: x in X . s by XBOOLE_0:def 1;
ex a being set st
( a in X . s & root-tree [x,s] = root-tree [a,s] ) by A1;
hence not FreeGen (s,X) is empty by Def15; :: thesis: verum