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 set 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 Def26; :: thesis: verum