let S be locally_directed OrderSortedSign; :: thesis: for X being non-empty 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 non-empty 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 Def27
.= Class ((CompClass (R,(CComp (LeastSort t)))),x) ;
hence t in OSClass (R,t) by EQREL_1:20, OSALG_4:5; :: thesis: verum