set NH = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X));
defpred S₁[ set ] means ex a being set st
( a in X . s & S = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) );
consider x being object such that
A1: x in X . s by XBOOLE_0:def 1;
S₁[((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [x,s])] by A1;
hence not OSFreeGen (s,X) is empty by Def25; :: thesis: verum