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:14; :: thesis: verum