set SO = the Sorts of (FreeOSA X);
set NH = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X));
let A, B be Subset of ( the Sorts of (FreeOSA X) . s); ( ( for x being object holds
( x in A iff ex a being object st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) & ( for x being object holds
( x in B iff ex a being object st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) implies A = B )
assume that
A8:
for x being object holds
( x in A iff ex a being object st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) )
and
A9:
for x being object holds
( x in B iff ex a being object st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) )
; A = B
thus
A c= B
XBOOLE_0:def 10 B c= A
let x be object ; TARSKI:def 3 ( not x in B or x in A )
assume
x in B
; x in A
then
ex a being object st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) )
by A9;
hence
x in A
by A8; verum