let S be locally_directed OrderSortedSign; :: thesis: for X being V16() ManySortedSet of S
for R being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds t in OSClass R,t
let X be V16() ManySortedSet of S; :: thesis: for R being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds t in OSClass R,t
let R be OSCongruence of ParsedTermsOSA X; :: thesis: for t being Element of TS (DTConOSA X) holds t in OSClass R,t
let t be Element of TS (DTConOSA X); :: thesis: t in OSClass R,t
set PTA = ParsedTermsOSA X;
reconsider x = t as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort t) by Def12;
OSClass R,t = OSClass R,x by Def28
.= Class (CompClass R,(CComp (LeastSort t))),x ;
hence t in OSClass R,t by EQREL_1:28, OSALG_4:6; :: thesis: verum