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); :: thesis: ( ( for x being set holds
( x in A iff ex a being set st
( a in X . s & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) ) ) & ( for x being set holds
( x in B iff ex a being set st
( a in X . s & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) ) ) implies A = B )
assume that
A7: for x being set holds
( x in A iff ex a being set st
( a in X . s & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) ) and
A8: for x being set holds
( x in B iff ex a being set st
( a in X . s & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) ) ; :: thesis: A = B
thus A c= B :: according to XBOOLE_0:def 10 :: thesis: B c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume x in A ; :: thesis: x in B
then ex a being set st
( a in X . s & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) by A7;
hence x in B by A8; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in A )
assume x in B ; :: thesis: x in A
then ex a being set st
( a in X . s & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) by A8;
hence x in A by A7; :: thesis: verum