set LS = LeastSort t;
set PTA = ParsedTermsOSA X;
reconsider x1 = t as Element of the Sorts of (ParsedTermsOSA X) . (LeastSort t) by Def12;
take OSClass (R,x1) ; :: thesis: for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds
OSClass (R,x1) = OSClass (R,x)
let s be Element of S; :: thesis: for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds
OSClass (R,x1) = OSClass (R,x)
let x be Element of the Sorts of (ParsedTermsOSA X) . s; :: thesis: ( t = x implies OSClass (R,x1) = OSClass (R,x) )
assume A1: t = x ; :: thesis: OSClass (R,x1) = OSClass (R,x)
LeastSort t <= s by A1, Def12;
hence OSClass (R,x1) = OSClass (R,x) by A1, OSALG_4:13; :: thesis: verum